# [FOM] inconsistency of P

Arnon Avron aa at tau.ac.il
Mon Oct 3 03:13:13 EDT 2011

```Can Nelson understand what is Pi^0_0 statement? How?
Can he  understand what is a formula? How?
Can he  understand what is a proof? How?

I cannot understand how he can use all these
concepts and yet claim to doubt the consistency of P.
(how does he understand the notion of consistency
at the first place?)

Arnon Avron

Quoting "Timothy Y. Chow" <tchow at alum.mit.edu>:

> 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
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>

----- End forwarded message -----
```