FOM: n(3)

[Harvey Friedman]

Shipman 2:44PM 10/12/98 writes:

>Example.  Let x be the length of Friedman's number n(3) when expressed
>in binary notation.  I expect "x is even" is a statement no one will
>ever know the truth value of, despite its obvious decidability.  It
>would be nice to have a formal system which somehow represented this
>fact directly by having neither "x is even" nor "x is odd" be formally
>derivable.  Of course here we are only requiring a system whose
>derivable sentences are a subset of the derivable sentences of PA; but
>one can go further and ask for a system in which a statement like "n(3)
>exists" is actually "false", where "false" is interpreted as "there is
>no feasible integer with the property defining n(3)".

Actually, it is trtivial that every n(k) is odd. But is n(3) divisible by
3? That might be much harder. Or is n(3) prime? Etcetera.

The result one wants is that, e.g., PA does not decide such questions by a
proof of length at most 2^2^100.