The Coq mailing list

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

Hello José,

José Manuel Rodriguez Caballero 
<josephcmac AT gmail.com>
 writes:

> Indeed, in my above-mentioned reference to Voevodsky's conjecture that
> PA is inconsistent, he explained the problem with Gentzen's argument:
> https://video.ias.edu/voevodsky-80th

Well, I am not the right person to talk about that but as far as I
understand Voevodsky retracted the claims made in that talk; maybe it is
good to give more publicity to the retraction so people is not misled.

It is my understanding that his views were influenced by Edward Nelson
which were quite radical AFAICT. IIRC, at some point Nelson wrote a
"theorem prover" and claimed to have found a proof of "PA ⊢ ⊥", but it
seems it was not correct.

Consistency of PA is a well-established fact and all that you need to
assume is the termination of the finitary Hydra game.

Think of it other way: if you had to bet all your current and future
state to either 1) "a proof of PA ⊢ ⊥" will be found or 2) "a proof of PA ⊢ ⊥"
won't be found, which one you would choose?

I would be happy to take the bet if you wanna support 1.

Also note that it is not the same to assume the existence of Nat than
the existence of Nat + induction, this may be relevant in some contexts.

Best,
E.