[FOM] 180:Provable Functions of PA
friedman at math.ohio-state.edu
Wed Jun 25 05:25:01 EDT 2003
Reply to Tait 10:40AM 6/22/03.
I have been asked to explain why something is true.
>On Saturday, June 21, 2003, at 10:02 AM, William Tait wrote:
>>On Sunday, June 15, 2003, at 11:42 PM, Harvey Friedman wrote:
>>>THEOREM 2. The PA provable Delta_0 functions are exactly the
>>>Delta_0 functions that are bounded by a <epsilon_0 recursive
>>I can't prove this. Certainly a Delta_0 function bounded by a
>>PA-provably recursive function is provably recursive; but I don't
>>see that it need be Delta_0.
>Just in case I'm being suspected of melt-down: of course, I meant
>that I don't see that it need be provably Delta_0. Bill
Let f be a Delta_0 function bounded by the <epsilon_0 recursive
function g. Let the e-th Turing machine compute g.
Let A(x,y) be Delta_0 defining f. PA may not prove
(forall x)(therexists unique y)(A(x,y).
Let A'(x,y) be
A(x,y) or (y is the number of steps that it takes for the e-th Turing
machine to halt, and for all z < y, we have notA(x,z)).
Then A'(x,y) is Delta_0, and PA proves
(forall x)(therexists unique y)(A'(x,y))
and A'(x,y) also defines f. So f is PA provable Delta_0.
More information about the FOM