[FOM] inconsistency of P

[Harvey Friedman]

I am reasonably aware of Nelson on this, but my main point is that  
mathematicians (including Nelson, by the way) seem to regularly use -  
and teach - facts which logically imply the consistency of at least  
significant fragments of PA, including PRA, or single quantifier PA.  
At least, the former Nelson - and what about Nelson's current math  
teaching?

Even this claim of mine above requires serious justification, and  
needs the new SRM = strict reverse mathematics, to fully justify.

On the other hand, it appears that a very large amount of mathematics  
is "innocent" and does not imply the consistency of, say, PRA, or  
single quantifier PA.

This leads to the program of coming up with very comprehensive  
conservative extensions of, say, RCA0 (and weaker!) that have lots of  
abstract objects - even uncountable objects - and support flexible  
reasoning involving such.

Harvey Friedman

> On Oct 2, 2011, at 8:42 PM, Timothy Y. Chow wrote:
>
> 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.
>