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

6 Answers 6

up vote 25 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
    
@DavidRoberts The consistency strength hierarchy in set theory (and even arithmetic) is not linear: one can construct sentences whose consistency strengths are incomparable. Meanwhile, there is a rough linear nature for many large cardinal axioms, and some people go further and insist that the large cardinal consistency strength hierarchy is definitely linear. But one should note that we have no proof of this and there are many pairs of large cardinal concepts whose exact consistency strength relation is not known. Note also that we have essentially no methods for proving non-linearity. –  Joel David Hamkins May 29 at 12:42

The folklore result is that there is a "simple" model of the underlying theory of Coq in $\mathrm{ZFC}+\omega$-many inaccessibles.

A good intro to this model is "The not-so-simple proof-irrelevant model of CC" by Miquel and Werner.

Benjamin Werner also sketched a consistency proof for the more general system with universes: On the strength of proof-irrelevant type theories. I feel that the community is begging for a clean formal construction of this model. I believe that this is what Bruno Barras is doing (as mentioned by Tim Chow in his answer).

The lower bound is more elusive still. I'm only aware of 2 results for lower bounds:

Werner again builds an interpretation of ZFC in CIC + some set-theoretically plausible axioms. Sets in Types, Types in Sets.

Miquel (again) builds an interpretation of Zermelo Set Theory in $\mathrm{F}_{\omega^2}$, the non-dependent fragment of $\mathrm{CoC}$ with universes. The article is a must read: $\lambda Z$: Zermelo’s Set Theory as a PTS with 4 Sorts.

If memory serves, in his PhD, he shows the more general result that $\mathrm{CoC}$ with universes is equi-consistent with Zermelo theory with $\omega$-many (Zermelo) universes. Sadly the dissertation is in French.

I'm far from certain that $\mathrm{CIC}$ with universes is more powerful than $\mathrm{CoC}$ with universes if no additional axioms are added. This intuitively is because inductive data-types can be built at the "2nd level" using the usual encoding trick, and AFAIK, have the same strength as "built-in" inductive data-types (but are significantly less convenient to use).

As you can see, there is significant work to be done to put these questions to rest.

share|improve this answer
1  
It might be better to personalize the state of affairs, as in "Sadly, the dissertation is in a language I don't know (French)." Gerhard "Appearance Matters (To The French)" Paseman, 2015.05.29 –  Gerhard Paseman May 29 at 17:45
    
Well, to be fair, I do know the language, but every time I try to sell people on this excellent work, the fact that it is in French is a no-go. The sad state of affairs is that English is a de facto standard language for scientific communication, just like Latin was 300 years ago. –  cody May 29 at 20:24
1  
@cody one should point out McLarty's paper claiming HoTT with the univalence axiom is consistent with finite-order arithmetic (arxiv.org/abs/1412.6714), though I'm not sure the issues raised by Awodey have been fully resolved. –  David Roberts May 29 at 23:36
    
@DavidRoberts: of course, McLarty's claim is for univalence in Martin-Löf type theory, which is much weaker than $\mathrm{CoC}$ (with some axiom along the lines $0\neq 1$). –  cody May 30 at 15:26
    
Point taken. Perhaps one should replace "I" with "many" in the above suggestion. Also, most sales pitches I know don't use the word "Sadly" . Gerhard "Your Closing Pitch Needs Work" Paseman, 2015.05.31 –  Gerhard Paseman May 31 at 22:53

There is a comment in Wikipedia that Martin-Löf type theory with arbitrarily many finite level universes has proof-theoretic ordinal the Feferman-Schütte ordinal $\Gamma_0$. There is no obvious reference given, unfortunately, past general proof theory/ordinal analysis texts.

share|improve this answer
2  
There is on the same page a remark a few line below that Martin-lof type theory with indexed W-type has a larger proof theoretic ordinal (the Bachmann-Howard ordinal). Coq has those $W$-type, together with an infinite hierarchy of universe, so it is even probably Higher... –  Simon Henry May 29 at 9:35
2  
@DavidRoberts: I am not sure the precise reference, but I know this is something that Peter Hancock and Anton Setzer have studied deeply. Here are some slides by Peter Hancock, which end with the claim in question: cs.swan.ac.uk/~csetzer/russell08/slides/hancock.pdf –  Noam Zeilberger May 29 at 13:38
    
@SimonHenry I didn't see that! –  David Roberts May 29 at 23:18
1  
Anton Setzer (cs.swan.ac.uk/~csetzer) has apparently a few papers dealing with the proof theoretic strength of Martin-lof type theory with various additional hypothesis. I haven't been through all of them (and they are not all accessible from his webpage) but it seems that the precise statement can be found in his work. –  Simon Henry May 30 at 12:07
    
Of course, Coq also has an impredicative base universe $\mathrm{Prop}$ which makes its proof theoretic ordinal unimaginably higher than $\Gamma_0$. Note that $\Gamma_0$ is lower than the ordinal for $\mathrm{PA}_2$ already... –  cody May 30 at 15:23

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

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
6  
@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
4  
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

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

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.