The Coq mailing list

[roconnor AT theorem.ca]

On Wed, 28 Sep 2011, Cody Roux wrote:

> ----- 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,

I think you mean to say that Coq can interpret PA rather than Coq extends 
PA.

BTW, you can intepret *all* proofs in PA into Coq, even the ones using 
excluded midde, with a suitable double negation intepretation.  This is 
how I prove the consistency of PA in my work.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''