Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

Less tongue in cheek, is it known what the relative consistency is for theorems proved with an automatic theorem prover? Of course this depends somewhat on what assumptions one makes with respect to predicativity and so on. But for concreteness take one of the popular packages with its standard installation.

Perhaps this is a can of worms, or a piece of string of indeterminate length, but the recent surge of interest in Voevodsky's univalent foundations raises questions about the consistency strength of the system HoTT he (and others) propose.

share|improve this question
    
As far as I have been taught, Coq proofs are pretty much the best proofs you can get: they just require intuitionistic logic in the strong sense (not the Russian one). Of course, I don't know what the "popular packages" are and whether one of them smuggles in some ZFC... –  darij grinberg Mar 25 '11 at 15:01
    
David: I thought you would be more interested in the Pollack quote. According to Pollack what you consider "underlying formal system" has "informally specified " coercions that may be used in proofs. An interesting question is "where is the full formal system of Coq described/proved" (I couldn't find such, found articles covering parts of the code...) –  joro Jun 15 '11 at 7:53

4 Answers 4

up vote 18 down vote accepted

For systems like Coq that are based on type theory, this question is trickier to answer than you might expect.

First of all, what does it take to "know" the consistency strength of some system? Classically, the most thoroughly studied logical systems are based on first-order logic, using either the language of elementary arithmetic or the language of set theory. So if you are able to say, "System X is equiconsistent with ZF" (or with PA, or PRA, or ZFC + infinitely many inaccessibles, etc.), then most people will feel that they "know" the consistency strength of X, because you have calibrated it against a familiar hierarchy of systems.

Coq, however, is based on something called the Calculus of Inductive Constructions (CIC). Without going into a detailed explanation of what this is, let me just mention that the core of CIC doesn't have any axioms, but typically people add axioms as needed. For example, if you want classical logic, then you can add the law of the excluded middle as an axiom. To get more power you can add more axioms (though you have to be careful because certain combinations of axioms are known to be inconsistent). But trying to line up the various systems you can get this way against more familiar set-theoretic or arithmetic systems is a tricky business. Typically, we cannot expect an exact calibration, but we can interpret various fragments of set theory in type theory and vice versa, showing that the consistency of CIC plus certain axioms is sandwiched between two different systems on the set-theoretic side. If you want to delve into the details, I'd recommend the paper Sets in Coq, Coq in Sets by Bruno Barras as a starting point.

share|improve this answer
    
Hmm, so even in Coq (and presumably among formal systems generally), we have a poset of consistency strength, rather than a more linear arrangement like set theory. I thought set theory might be in general incomparable in strength to formal systems (and Coq specifically), but I didn't consider the case that there was branching at such a low level. –  David Roberts Mar 25 '11 at 23:32

There are several things to say : first, an automatic theorem prover not only says a naked "This is true" -- it says "It is true and here is a proof : ...".

The fact that a proof exists is already something which lends confidence to the result, because that means it can be independently checked. And by that, I mean that an automatic proof checker can go on the proof and look for errors. Or humans can check each step (though that will be very very boring comparing to human-written proofs).

I must insist that if the check is by a program, then it should be made off a different code base than the prover -- because there's a risk that if a bug made the proof faulty, that same bug will make the checker faulty in a similar way.

From those considerations, I think automatic proofs can be as convincing as human proofs. Definitely not as satisfying, but convincing.

I trust the books and the articles I read because I check them for basic consistency, and I know others did too. Why wouldn't I trust results which have been checked likewise?

share|improve this answer
1  
Snark - Stefan is right in his interpretation. I'm not looking for how much faith we put in proofs generated by formal systems, but the relative consistency strength of the results produced. But it is a good point that we don't just get a result but a proof of it as well. –  David Roberts Mar 25 '11 at 23:25

Some proof checkers/automatic provers like Mizar use pretty strong theories: Set Theory (ZFC or something like that) together with the assumption that there is an inaccessible cardinal, if I remember correctly.

@Snark: I think the OP is not so much concerned with the possibility that the automatic prover has bugs, but that the underlying axiom system is actually faulty, i.e., inconsistent.

share|improve this answer
3  
It's even worse: the Tarski–Grothendieck set theory used by Mizar is equivalent to ZFC + there exists a proper class of inaccessible cardinals. –  Emil Jeřábek Mar 25 '11 at 14:11
    
Ah, that's interesting. I was under the obviously faulty assumption that automatic theorem provers shied away from theories that strong (which are not that strong in the grand scheme of things, but stronger than Coq for example) –  David Roberts Mar 25 '11 at 23:27
5  
@David: Philosophically, automated proof checkers are motivated more by the problem of human error creeping into the process of verifying proofs than by skepticism about the "truth" of strong axioms. Conversely, if you are skeptical about sets, or truth, or infinity, or impredicativity, or whatever, then you'll naturally be interested in logical systems that avoid such things, but that doesn't necessarily mean that you'll insist on machine verification of everything. –  Timothy Chow Apr 1 '11 at 18:29
3  
Mechanization also makes understanding informal patterns of proof very important. Eg, probability theorists often avoid stating which probability space they are working in, so that they can freely introduce new random variables in a proof. This pattern can be formalized by interpreting these arguments in a topos of presheaves over probability spaces and extensions. There's no consistency strength angle, but the "morality of proofs" of probability theory (and other areas) is still important. Without that structure, mechanization attempts will invariably drown in extraneous detail. –  Neel Krishnaswami Jun 15 '11 at 11:19

Here are some publications related to your question:

Robert Pollack. How to believe a machine-checked proof. In G. Sambin and J. Smith, editors, Twenty Five Years of Constructive Type Theory. Oxford Univ. Press, 1998.

Pollack-inconsistency, Freek Wiedijk Freek demonstrates the most popular proof assistants are Pollack inconsistent.

In an internet post Pollack discusses Coq coercions:

The problem is that Coq coercions are informally specified and behave somewhat unpredictably. A formal theory of coercions, such as Luo's Coercive subtyping (with proof theory and semantics) would eliminate this question of the meaning of statements using coercions. However, the proof theory of coercions is complicated.

share|improve this answer
    
Hi Joro - thanks for the references. I read the second of these not long ago, but after I posted this question. However, I was looking more for the consistency strength of the underlying formal system in Coq, rather than the notion of whether we believe Coq to have proved what we thought it proved. –  David Roberts Jun 15 '11 at 7:23
    
David: I thought you would be more interested in the Pollack quote. According to Pollack what you consider "underlying formal system" has "informally specified " coercions that may be used in proofs. –  joro Jun 15 '11 at 7:40

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.