How true are theorems proved by Coq?

Question

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.

Answer 1

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.

Answer 2

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.

Answer 3

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. doi:10.1093/oso/9780198501275.003.0013, (also freely available as BRICS Report Series, 4(18) (1997) doi:10.7146/brics.v4i18.18945) (Wayback Machine of author's gzipped ps file)

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.

Answer 4

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.

Answer 5

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?

Answer 6

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.

Answer 7

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.

Answer 8

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.