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).
While writing up decision theory results, I had to work out bounded versions of Gödel's second incompleteness theorem and Löb's theorem. Posting the tentative proofs here to let people find any major errors before adding formality. Any comments are welcome!
Bounded Gödel's theorem
Informal meaning: if a theory T has a short proof that any proof of T's inconsistency must be long, then T is inconsistent.
Formal statement: there exists a total computable function f such that for any effectively generated theory T that includes Peano arithmetic, and for any integer n, if T proves in n symbols that "T can't prove a falsehood in f(n) symbols", then T is inconsistent.
Proof
If the theory T takes more than n symbols to describe, the condition of the theorem can't hold, so let's assume T is smaller than that.
Let's take g(n)>>n and f(n)>>exp(g(n)). For any integer n, let's define a program R that enumerates all proofs in the theory T up to length g(n), looking for either a proof that R prints something (in which case R immediately halts without printing anything), or a proof that R doesn't print anything (in which case R prints something and halts). If no proof is found, R halts without printing anything.
Assume that the theory T is consistent. Note that if the program R finds some proof, then it makes the proved statement false. Also note that the theory T can completely simulate the execution of the program R in exp(g(n)) symbols. Therefore if the program R finds any proof, the resulting contradiction in the theory T can be "exposed" using exp(g(n)) symbols. Since f(n)>>exp(g(n)), and the theory T proves in n symbols that "T can't prove a falsehood in f(n) symbols", we see that T proves in slightly more than n symbols that the program R won't find any proofs. Therefore the theory T proves in slightly more than n symbols that the program R won't print anything. Since g(n)>>n, the program R will find that proof and print something, making the theory T inconsistent. QED.
(The main idea of the proof is taken from Ron Maimon, originally due to Rosser, and adapted to the bounded case.)
Bounded Löb's theorem
Informal meaning: if having a bounded-size proof of statement S would imply the truth of S, and that fact has a short proof, then S is provable.
Formal statement: there exists a total computable function f such that for any effectively generated theory T that includes Peano arithmetic, any statement S in that theory, and any integer n, if T proves in n symbols that "if T proves S in f(n) symbols, then S is true", then T proves S.
Proof
Taking the contrapositive, the theory T proves in n symbols that "if the statement S is false, then T doesn't prove S in f(n) symbols". Therefore the theory T+¬S proves in n symbols that "T+¬S doesn't prove a falsehood in f(n) symbols" (I'm glossing over the tiny changes to n and f(n) here). Taking the function f from the bounded Gödel's theorem, we obtain that the theory T+¬S is inconsistent. That means T proves S. QED.
(The main idea of the proof is taken from Scott Aaronson, originally due to Kripke or Kreisel.)
As a sanity check, the regular versions of the theorems seem to be easy corollaries of the bounded versions. But of course there could still be errors...