[FOM] a query about PRA
Mongre at gmx.de
Thu Mar 9 10:08:49 EST 2006
Let S be any formal system extending primitive recursive arithmetic.
As is well known, for any pi_1 sentence A, PRA+Con(S) proves that if
S proves A then A. In particular, if we take S to be PRA itself, then
PRA+Con(PRA) proves the reflection principle for PRA (i.e. proves
every instance of the schema).
My question is: does PRA know that it does all this? This is what my
old Latin master would have called a num question - expecting the
answer no. I expect the answer no because it doesn't seem to me that
the function leading from the Goedel number of A to the Goedel number
of a proof in PRA+Con(S) of 'if S proves A then A' is going to be
primitive recursive (basically, because the evaluation function isn't
primitive recursive). But I could easily be quite wrong.
More information about the FOM