[FOM] 180:Provable Functions of PA
William Tait
wwtx at earthlink.net
Thu Jun 26 09:54:54 EDT 2003
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
More information about the FOM
mailing list