The Coq mailing list

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

Dear Emilio,

  Thank you very much by the information that Voevodsky retracted its conjecture that PA is inconsistent (it would be wonderful to find a video or a manuscript of him in order to know the context). Nevertheless, as far as I know, he didn't retracted his second claim:  "CIC is not cleaned defined, because it is an initial model of a theory which itself requires natural numbers to be specified".

Concerning you claim that "consistency of PA is a well-established fact", according to your two arguments I only can deduce that "consistency of PA is a well-established belief". First, "the termination of the finitary Hydra game" is not true for certain initial segment of PA (this is precisely the theorem that I'm trying to mechanize in Coq right now). You can prove "the termination of the finitary Hydra game" in ZFC as well as in CiC, but that is more, not less. Second, the argument "if you had to bet all your current and future state to either..." can be used to "prove" any conjecture, for example the 3x+1 conjecture.

With respect to you question

"About 'proving in Coq' assumptions from CiC in a fancy way, well, that's

what logic is, isn't it?"

My answer is that in foundation of mathematics you go from weak assumptions to strong assumptions. To do it the other way around is Begging the Question. For example, Riemann "proved" Prime Number Theorem, but he just assumed Riemann Hypothesis.

CiC is wonderful for many branches of mathematics, but there are some foundational problems when it is applied as an autonomous foundation of mathematics.

Best Regards,

José M.

2018-05-02 12:03 GMT+02:00 R. Pollack <rpollack0 AT gmail.com>:

Emilio says:

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.

​Nelson was not as nutty as this might suggest.  He took the view that natural number induction is not predicative, because one quantifies over all natural numbers.  In his classic monograph "Predicative Arithmetic" he discusses formal systems​ that are predicative in his sense. IIRC such systems do not prove totality of exponentiation, so Godel's Theorem may be unprovable.

--Randy