Some comments
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.
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?
there exists a total computable function f such that .... For any integer n, let's define a program R ...
For this to work, the Godel number of R needs to be a computable function of n.
Let's take g(n)>>n
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?
Assume that the theory T is consistent. Note that if the program R finds some proof, then it makes the proved statement false, therefore R won't find any proofs.
Don't you need soundness for that instead of consistency?
I am now trying to formalize the proof, to aid my own understanding.
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 functio
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...