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.
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).
Some comments
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?
For this to work, the Godel number of R needs to be a computable function of 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?
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!
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.
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.
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.
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).