The Coq mailing list

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

Dear José,

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

> 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).

If my memory serves me correctly you should be able to find a mail
discussion in FOM around the date of the talk.

> 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".

I am not an expert on the meta-theory of CIC and indeed I heard that it
may have some rough edges, but AFAIK there should not be a serious
problem there.

> 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.

Well, I say it is a well established fact as I can build a _physical_
machine that will actually normalize any proof let's say, in System-T,
provided you give me a finite, but _unbounded_ number of pieces, thus
breaking the "assumption cycle" by constructing an actual device.

I guess the device could be a steam-punk like machine [with gears and
steam pipes and whatnot] but usually computers are more practical; but
indeed, this only holds if I can assume an unbounded amount of memory,
well, in the case of PA I believe given the input term I can predict the
maximum amount of memory I would use.

As I wrote on the other mail, rejecting the unbounded nature of our
theoretical computing devices it is a valid and fair point, but usually
off-topic in the context of traditional cut-elimination proofs.

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

I'll have to disagree here, as indeed in my very humble view you cannot
do much better than having a realizability model in terms of
philosophical justification; basically you are reducing truth to a
computation that can be carried out by a physical machine, and thus
outside the realm of mathematics themselves.

I am not sure what kind of problem you do find with that, other than of
course the unavoidable physical limits of reality.

E.