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...