[FOM] 180:Provable Functions of PA

[William Tait]

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. (I also don't have a counterexample.) Do you 
want to give a hint, Harvey?

Regards,

Bill Tait