Thanks for the very detailed comments, as usual!

I find this statement too vague, what does simulation mean? Does it mean that T can prove in exp(g(n)) symbols that "R() == x" where x = R()? On what do you base the claim that you need exp(g(n)) symbols? I assume the intent is to bound the number of steps in the execution of R?

Yes, that's the intent. R checks exp(g(n)) proofs, and checking each proof is less than exponential, so it all gets folded up into the exponential.

For this to work, the Godel number of R needs to be a computable function of n.

Are you sure? It seems to me that R is just something that gets used in the proof, only f(n) and g(n) need to depend on n... In any case, R depends on T, not just n. Of course the size and runtime of R need to be bounded by functions of n, and they are.

Why do you require g(n) to be much larger than n? How much larger does it need to be? Why not take g(n)>n, or even g(n)=n?

Because there are also things like going from "R won't find proofs" to "R won't print anything", which may have constant or linear costs, but not more.

Don't you need soundness for that instead of consistency?

For that statement, yes. But it's not really used in the proof, so I removed it =) Thanks!

For the next statement I only need consistency, because I build a contradiction between two proofs in T (the proof that gets found by R, and the proof by simulation of what R ends up doing).