[FOM] 180:Provable Functions of PA

[Harvey Friedman]

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 
>>>function.
>>
>>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.

Harvey Friedman