[FOM] 180:Provable Functions of PA

[William Tait]

On Wednesday, June 25, 2003, at 04:25  AM, Harvey Friedman wrote:

> 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

Thanks, Harvey; I should have seen that. Maybe not melt-down, but its 
getting hotter.

> Let f be a Delta_0 function bounded by the <epsilon_0 recursive 
> function g. Let the e-th Turing machine compute g.

More explicitly, since <epsilon_0-recursive is equivalent to PA 
provable Sigma_1, let  (all x)(exists z) B(x, g(x), z), where PA proves 
(all x)(exists unique y)(exists z) B(x,y,z) and B is Delta_0.

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

  A'(x,y) is A(X,y) or {B(x, (y)_0, (y)_1) and for all z<y not-A(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.

I'll come to you with all my problems!

Bill Tait