# [FOM] 180:Provable Functions of PA

Harvey Friedman 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
>>>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

```