The Coq mailing list

[José Manuel Rodriguez Caballero <josephcmac AT gmail.com>]

Emilio said
So now the question is, can you construct a losing strategy for the
Hydra game?

There is such a losing strategy, but you need to take a certain initial segment of non-standard model of first-order Peano arithmetic, this is how Kirby and Paris proved the unprovability of Goodstein theorem in PA (page 291 of Accessible Independence Results for Peano Arithmetic). 

Russell said
I'm about as confident that there is no infinitely long descending chain of ordinal notations in Cantor normal form as I am that there is no infinitely long descending chain of natural numbers.

If you take Nelson's Internal Set Theory in place of ZFC, then you can prove in a trivial way that there exists an "infinitely long" descending chain of ordinal notations in Cantor normal form, where "infinitely long" here means "larger than any standard natural number", i.e. larger than any n : nat. Of course that sequence will be Dedekind-finite, but from a practical point of view, it will be infinite.

To believe that the statement 0 = 1 is false is not the same a to believe in the consistency of PA.  Indeed, the relevant arithmetic R# is consistent and you can prove there that the statement 0 = 1 cannot be deduced. If there is an inconsistency of PA, it will be because of its first-order classical logic and it will be related to the induction principle. 

Many people think that the higher-order logic of Coq is its main advantage, but from the point of view of model theory it is uncomfortable to work with non-standard first-order arithmetic in Coq. Practically, you need to create another software inside Coq in order to do it and from a foundational perspective you need to assume the consistency of Coq in order to prove results which, in some cases, are metamathematically true without assuming any consistency.