The Coq mailing list

[Emilio Jesús Gallego Arias <e AT x80.org>]

Marco Servetto 
<marco.servetto AT gmail.com>
 writes:

> I think this conversation is very interesting for us (especially since
> many students read this mailing-list) , may be is not so much about
> coq but about what it means to "prove" something.

Indeed my only motivation to reply was indeed to warn students reading
the mailing list that claims such as "the consistency of PA is an open
question" are just uninformed statements by non-experts.

By the way, Coq proves the consistency of PA almost in a trivial way if
you admit a deep embedding of the axioms + some trickery, or you use
System-T.

> I would dare to ask a question to this list:
> -is there any proof in any (not proved incoherent yet) system showing that
> "it must exist a coherent systems complex enough to support Godel theorem"?
> sometimes I wonder if they are just going to be bound to be
> incoherent, and the proof "true=false" is often just so gigantic that
> escape human comprehension.

I am not sure what do you mean here, but indeed IIUC the answer is given
by the incompleteness theorem itself, and is no. A proof of

"PA ⊢ true = false" cannot exist unless you are willing to contradict
for example, as pointed out separately that the Hydra game has a winning
strategy. This is well established fact and there is little to discuss.

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

Systems proving the consistency of PA tend to use other means of
justification, such as computation, or games.

E.