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...
I'm not sure if this post is obsolete, but it was linked to by a recent post, so I will provide feedback.
The translation to the formal version goes from "if a theory T has a short proof that any proof of T's inconsistency must be long, then T is inconsistent" to "if T proves in n symbols that 'T can't prove a falsehood in f(n) symbols", then T is inconsistent.'"
But inconsistency is not the same as proving a falsehood. Assuming that PA is consistent, the theory PA+~Con(PA) is consistent, since PA cannot prove its own consistency, but this consistent theory proves the false theorem ~ConPA.
Also, there exists no truth predicate Tru(n) within any consistent extension of PA--otherwise, we could formulate a liar paradox. Hence the notion of a "falsehood" is not expressible in our formal system.
In the proof, we define a program R which enumerates the theorems of the theory T that can be proved with g(n) symbols or less. Such a program must describe the formal system T to utilize its axioms and rules of inference. Assume that T is describable using t symbols. Then the program R requires log g(n) bits to describe the halting condition and t bits to describe T, so we can write the program R using around log g(n) + t bits.
This means that when R is searching for proofs about its behavior of length less than g(n), some of the g(n) symbols will have to describe R itself using log g(n) + t bits. This means that if R does not find a proof, it has only established that there is no proof in T that R halts or not of g(n) - (log g(n) + t) symbols. There may well exist a proof in T that R halts or not of g(n) symbols.
Now T is supposed to prove in n symbols that "T can't prove a falsehood in f(n) symbols," but n << g(n) and exp g(n) << f(n). This implies that log f(n) >> n, which means that n symbols do not suffice to describe a number of size f(n). Thus it is impossible to prove that "T can't prove a falsehood in f(n) symbols" using n, or slightly more than n, symbols.
By "proving a falsehood" I meant proving that 0=1. That's how people usually formalize something like Con(PA).