[FOM] inconsistency of P

[Timothy Y. Chow]

Harvey Friedman wrote:

>As I indicated before on the FOM, there is a proof that any given  
>finite fragment of PA is consistent, using "every infinite sequence of  
>rationals in [0,1] has an infinite Cauchy 1/n subsequence".

Perhaps you haven't read any of Nelson's philosophical writings.  He 
doesn't believe in infinity, except "potential infinity," and regards 
even so-called "finitary" reasoning (let's say, PRA) as having hidden 
infinitary assumptions in it.  Thus it is suspect.

Here's another way to put it.  You [Friedman] have suggested before that 
mathematics is "essentially" Pi^0_1.  For example, if someone were to 
prove P != NP, then we'd immediately want a more quantitative version of 
it that gives us bounds, and we'd search for a Pi^0_1 strengthening.  For 
Nelson, math is essentially Pi^0_0.  Nelson will accept statements of the 
form "T is a theorem of X" as immediately meaningful because they're 
Pi^0_0.  (At least, he'll accept them if the proof has feasible length; my 
guess is that he'd do the old "wait 2^n when asked if 2^n exists" trick if 
you asked him about large finite numbers.)  But any infinitary statement T 
is at best a convenient fiction for helping us find Pi^0_0 statements, or 
is perhaps a shorthand for "T is provable in X."

It's not clear to me whether there is anything that Nelson would accept
as settling the consistency of first-order Peano arithmetic in the 
affirmative.  So when he says that "the consistency of P remains an open 
problem" I think he just means that nobody has yet found an explicit proof 
of a contradiction in P.

Tim