The Coq mailing list

[Andrej Bauer <andrej.bauer AT andrej.com>]

Dear José,

your post contains a number of inaccurate statements. Let me just
focus on this one:

> Coq cannot prove the consistency of PA: no one can do it (Coq is not 
> supernatural, to say it in a funny way).

You seem to think that one can never prove the consistency of PA.
Already Gentzen showed the consistency of PA by using induction up to
ordinal ∊₀. Set theory ZFC can prove consistency of PA. CiC can prove
consistency of PA. The question is not whether consistency of PA can
be proved in some theory T, but how do we know that T itself is
consistent? So, there is a proof of consistency of PA in CiC. But to
prove consistency of CiC itself requires a still stronger theory. This
is all very well known and is not mysterious at all.

I recommend a textbook on proof theory that will counteract the
popular misrepresentations of Gödel's work that are all too easy to
find. Wolfram Pohlers published a textbook in 2008 which is also quite
detailed about inductive definitions. I do not know whether it covers
CiC, though, but it surely covers lots of related systems.


With kind regards,

Andrej