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.

When I get some time I'll sit down and read these more carefully. However, before that time comes I wanted to congratulate you on tackling these things!

<3

EDIT 1: Remarks on Bounded Goedel's theorem

1) It is unclear (to me, who has not studied such things in several years) where the proof uses the fact that T includes PA. Maybe it is necessary for the construction of R?

Other than that, I rewrote the proof as explicitly as I could (supplying some missing details and the like) and found no issues.

We should be able to make the bounds smaller... Let a be small (in comparison to n), and let P be the proof of length n that "T can't prove a falsehood in f(n) symbols" is true.

Then define R as above, except it searches through all proofs beginning with P, of length n+a. Then T can completely simulate the execution of R in slightly over (n+a)exp(a) symbols. Then the same reasoning would establish that we only need to take f(n) >> (n+a)exp(a) in order for the reasoning to work.

Not sure how large a should be. It might be a constant, but more likely it grows logarithmically with n (as it probably has to include the definition of n itself). Which would mean f(n) >> n^2.

If this argument works, we might be able to get even better bounds restrictions - maybe we restrict R to look at proofs starting with P, which then include the definition of n somewhere after. Or maybe R just looks at a single proof - the actual proof that R printing anything is impossible? That would reduce to f(n) >> n.

This comment was stupid. The symbol papermachine refered to was T ⊢_n P or maybe [n]P.

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.

Could you elaborate on this? What is the slightly-more-than-n-symbols-long proof?

Bounded Löb's theorem seems to provide an easier way to do what you did in AI Cooperation in Practice. Or are they essentially the same thing?

I like (apart from the use of T and S to denote very different things). EDIT: and R!

One question: any idea how long it would take T to prove S under this reasoning?

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.