[Date Index] [Thread Index] [FOM Postings] [FOM Home]

*To*: fom@math.psu.edu*Subject*: FOM: n(3)*From*: friedman@math.ohio-state.edu (Harvey Friedman)*Date*: Mon, 12 Oct 1998 16:57:41 -0400 (EDT)*Sender*: owner-fom@math.psu.edu

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.

[Date Prev] [Date Next] [Thread Prev] [Thread Next]

[Date Index] [Thread Index] [FOM Postings] [FOM Home]