[FOM] a query about PRA

[Robert Black]

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.

Robert