58
$\begingroup$

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.

$\endgroup$
8
  • $\begingroup$ 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... $\endgroup$ Mar 25, 2011 at 15:01
  • $\begingroup$ 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...) $\endgroup$
    – joro
    Jun 15, 2011 at 7:53
  • $\begingroup$ @joro I recently watched a talk about MetaCoq, which is trying to verify Coq, and apparently there's a whole lot that's not even documented, let alone the full formal system being described anyway. $\endgroup$
    – David Roberts
    Oct 31, 2021 at 8:41
  • $\begingroup$ @DavidRoberts Thanks. Many years ago on the Coq mailing list I saw proof based on paradox of the form A = not A which raised error of the form "multiverse inconsistency" $\endgroup$
    – joro
    Oct 31, 2021 at 8:51
  • $\begingroup$ Yes, I vaguely recall that there have been outright (local) bugs. $\endgroup$
    – David Roberts
    Oct 31, 2021 at 9:13

8 Answers 8

45
$\begingroup$

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.

$\endgroup$
6
  • $\begingroup$ 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. $\endgroup$
    – David Roberts
    Mar 25, 2011 at 23:32
  • 10
    $\begingroup$ @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. $\endgroup$ May 29, 2015 at 12:42
  • 1
    $\begingroup$ When this topic came up recently on the Foundations of Mathematics mailing list, Freek Wiedijk mentioned another relevant paper: "On Relating Type Theories and Set Theories" by Peter Aczel, in Types for Proofs and Programs, Lecture Notes in Computer Science Volume 1657, 1999, pp 1-18. $\endgroup$ Oct 21, 2015 at 20:21
  • $\begingroup$ @Joel I was just wondering if there is anything new in the nonlinear consistency strength world... $\endgroup$
    – David Roberts
    Oct 30, 2021 at 22:52
  • 2
    $\begingroup$ @DavidRoberts I have a paper in preparation. See jdh.hamkins.org/…. There will be a revised version of this paper coming out probably in a few months. $\endgroup$ Nov 9, 2021 at 21:07
17
$\begingroup$

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.

$\endgroup$
7
  • 1
    $\begingroup$ 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 $\endgroup$ May 29, 2015 at 17:45
  • 8
    $\begingroup$ 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. $\endgroup$
    – cody
    May 29, 2015 at 20:24
  • 1
    $\begingroup$ @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. $\endgroup$
    – David Roberts
    May 29, 2015 at 23:36
  • 1
    $\begingroup$ 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 $\endgroup$ May 31, 2015 at 22:53
  • 2
    $\begingroup$ The first link - irif.fr/users/miquel/publis/types02.pdf - seems to be dead. Is it this paper: lix.polytechnique.fr/~werner/publis/cc.pdf ? $\endgroup$ Aug 15, 2017 at 16:18
11
$\begingroup$

Here are some publications related to your question:

In Pollack-inconsistency (published in Electronic Notes in Theoretical Computer Science), Freek Wiedijk 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.


Added later

The consistency and expressive power of Coq depend on time and bugs fixed vs bugs introduces.

Some versions of Coq fail to prove provable theorems, e.g. check How do I verify the Coq proof of Feit-Thompson?

The error you get is a real one, but is not in the proof of the odd order theorem. It is in Coq. Let me be more clear: a bug in the kernel of Coq

Inconsistency bugs appear more common, Preliminary compilation of critical bugs in stable releases of Coq. In around 2008 I reported inconsistency bug and to my surprise Coq devs called the proof of concept code exploit.

$\endgroup$
2
  • $\begingroup$ 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. $\endgroup$
    – David Roberts
    Jun 15, 2011 at 7:23
  • $\begingroup$ 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. $\endgroup$
    – joro
    Jun 15, 2011 at 7:40
8
$\begingroup$

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.

$\endgroup$
4
  • 3
    $\begingroup$ It's even worse: the Tarski–Grothendieck set theory used by Mizar is equivalent to ZFC + there exists a proper class of inaccessible cardinals. $\endgroup$ Mar 25, 2011 at 14:11
  • $\begingroup$ 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) $\endgroup$
    – David Roberts
    Mar 25, 2011 at 23:27
  • 11
    $\begingroup$ @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. $\endgroup$ Apr 1, 2011 at 18:29
  • 7
    $\begingroup$ 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. $\endgroup$ Jun 15, 2011 at 11:19
6
$\begingroup$

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?

$\endgroup$
1
  • 2
    $\begingroup$ 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. $\endgroup$
    – David Roberts
    Mar 25, 2011 at 23:25
6
$\begingroup$

I just learned about the part of the Coq FAQ titled What do I have to trust when I see a proof checked by Coq?. To quote from the Apr 24, 2018 revision:

You have to trust:

  • The theory behind Coq: The theory of Coq version 8.0 is generally admitted to be consistent wrt Zermelo-Fraenkel set theory + inaccessible cardinals. Proofs of consistency of subsystems of the theory of Coq can be found in the literature.
  • The Coq kernel implementation: You have to trust that the implementation of the Coq kernel mirrors the theory behind Coq. The kernel is intentionally small to limit the risk of conceptual or accidental implementation bugs.
  • The Objective Caml compiler: The Coq kernel is written using the Objective Caml language but it uses only the most standard features (no object, no label ...), so that it is highly improbable that an Objective Caml bug breaks the consistency of Coq without breaking all other kinds of features of Coq or of other software compiled with Objective Caml.
  • Your hardware: In theory, if your hardware does not work properly, it can accidentally be the case that False becomes provable. But it is more likely the case that the whole Coq system will be unusable. You can check your proof using different computers if you feel the need to.
  • Your axioms: Your axioms must be consistent with the theory behind Coq.

So I guess Coq theorems are true modulo the above.

$\endgroup$
1
  • $\begingroup$ It's a tiny bit more finicky than this though: github.com/coq/coq/issues/7695 this inconsistency is the result of interactions between modules and polymorphic universes: is this a defect of the theory behind Coq, or the implementation? $\endgroup$
    – cody
    Oct 18, 2020 at 5:39
3
$\begingroup$

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.

$\endgroup$
6
  • 2
    $\begingroup$ 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... $\endgroup$ May 29, 2015 at 9:35
  • 2
    $\begingroup$ @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 $\endgroup$ May 29, 2015 at 13:38
  • 1
    $\begingroup$ 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. $\endgroup$ May 30, 2015 at 12:07
  • 1
    $\begingroup$ 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... $\endgroup$
    – cody
    May 30, 2015 at 15:23
  • 1
    $\begingroup$ @SimonHenry from the perso.ens-lyon.fr/jeremy.ledent/internship_report.pdf, dated August last year, I see the strength of HoTT is an open problem. $\endgroup$
    – David Roberts
    Jun 2, 2015 at 7:16
1
$\begingroup$

Taken from the question How bad is Coq proving both $T$ and $\lnot T$?

Back in 2011 on the coq-club mailing list there was a thread: Is the Daniel Schepler's inconsistency real?. In the thread Georgi Guninski is me.

Inline in it there are two files (file 1) and (file 2), which are minor modifications of Daniel's code.

In 2023 all of the following can be proved based on the files.

  1. $T$
  2. $\lnot T$.
  3. Taking $T$ as axiom, we can prove $False$.
  4. Taking $\lnot T$ as axiom, we can prove $False$.

Proving $T$ and $\lnot T$ doesn't lead to proof of $False$, with a Coq error.

$\endgroup$
1
  • $\begingroup$ But as a pointer for future readers, consult the answer there, as well. $\endgroup$
    – David Roberts
    Aug 24, 2023 at 1:05

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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