The Coq mailing list

[Cody Roux <cody.roux AT inria.fr>]

----- Mail original -----
> De: "Andrej Bauer" 
>Â <andrej.bauer AT andrej.com>
> À: "Benjamin Werner" 
>Â <benjamin.werner AT polytechnique.org>
> Cc: "Coq-Club Club" 
>Â <coq-club AT inria.fr>
> Envoyé: Mercredi 28 Septembre 2011 15:05:14
> Objet: Re: [Coq-Club] a question about CIC/Coq consistency
> > Coq is an extension of PA.
> 
> What does "extension" mean here?
> 
> With kind regards,
> 
> Andrej

I'm sure someone else will have answered by the time this is sent but I'll 
try to give a quick idea about measuring the relative strengths of logical 
theories: In this case we can take a statement about Peano Arithmetic, for 
example:

forall x y, exists z, x * z = y

And translate that into a Coq statement:


forall (x y : nat), exists z:nat, x * z = y

where the multiplication and equality are translated to the ones in the 
standard library. Now you can translate every statement of Peano Arithmetic 
into one of Coq, and ask yourself which statements provable in PA are 
provable in Coq.

It is in fact easy to show that all statements provable in PA -without the 
use of the excluded middle- have translations which are in fact provable in 
the Coq logic. The fragment of PA that does not admit the excluded middle is 
commonly called HA, Heyting Arithmetic. So there are some statements that are 
provable in PA and not in Coq (or HA). However it can be shown that if PA is 
contradictory, i.e. PA proves 0 =\= 1, then so does HA, and therefore Coq 
proves the translation of that statement "O <> S O" (which implies False).

As a side note, it is interesting to ask whether there are statements from HA 
such that their translations are provable in Coq, but that are themselves not 
provable in HA. The answer is yes! There are many such statements, one of the 
famous ones being the Goodstein Theorem, another being the Godel encoding of 
the consistency of Arithmetic.

In conclusion, Coq can prove all theorems of Peano Arithmetic that do not use 
excluded middle in their proofs, and has a strictly stronger consistency 
strength: consistency of Coq implies that of PA, but not vice-versa.

I'm not sure that the consistency strength of CIC or Coq are precisely known 
with respect to set theories but I believe that CIC with universes and 
predicative set is weaker than, but of similar strength to, ZF set theory (in 
particular it is stronger than ZF - axiom of replacement). Benjamin probably 
knows more about this than I do.


I hope I am not rehashing things you know very well,


All the best,


Cody