[FOM] Re: Ineffective proofs and weak systems

[Timothy Y. Chow]

Harvey Friedman <friedman at math.ohio-state.edu> wrote:
> If an AE sentence is provable in RCA0 then there is a primitive recursive
> way of going from A to E.
[...]
> If an AEA sentence is provable in RCA0 then there may not be an effective
> way of going from A to E.

Thanks for the remedial lesson.  I take it that analogous statements hold
for weaker systems, such as PFA?  That is, if an AE sentence is provable
in PFA then there is a polynomial way of going from A to E, but if an AEA
sentence is provable in PFA then there may not be an effective way of
going from A to E?

By the way, is PFA the same as Buss's S_2?

Tim