FOM: n(k), PA

[Joe Shipman]

Of course I knew that the n(k) are all odd--that is why I used "the
length of  n(3) in binary" rather than n(3) itself!   I also considered
n(3) divisible by 3, but wanted something which looked like it had a
50-50 chance of being true.

What you really want to do is show there is no proof settling the
question of length < 2^2^100 in ZF (modulo ZF's consistency), not in PA.

Can anyone give an example of a intrinsically interesting theorem (one
which might be conjectured by a non-logician) which is provable in PA
but not feasibly provable in PA?  (I don't want an example with an
arbitrary numerical parameter in it unless the parameter is at most 3).

-- Joe Shipman