Cousin_it, do you have an argument that n1 … n6 < nmax? It seems like one way for the proof to fail is if no matter what nmax is, step 11 forces n1 > nmax.
Only a very rough one, I’m afraid. The number n1 is chosen to “contain” the blow-up from the short proof of 10 to the proof of 11, which grows with the computational complexities of n1,...,nmax, not their values. These computational complexities can be made way smaller than n1.
Ok, I was checking if there was an obvious flaw that you might have missed. Now I’m trying to actually understand your proof, and I’m getting stuck on the first step, where you invoke the Diagonal Lemma. Now a typical statement of the Diagonal Lemma is:
Diagonal Lemma: If T is a theory in which diag is representable, then for any formula B(x) with exactly one free variable x there is a formula G such that G ⇔ B(g(G)) is a theorem in T. (g(G) is the Gödel number of G. This was copied from page 2 of http://www.cs.cornell.edu/courses/cs4860/2009sp/lec-23.pdf)
If you look at page 3 of that PDF, it gives an explicit formula for G, which happens to contain an existential quantifier. Now my question is, how do I translate that G into a code string (the one named “box” in your proof)? Also, is this supposed to be obvious, or are you assuming some background knowledge beyond the standard expositions of the Diagonal Lemma and Löb’s Theorem?
You can build “box” by quining, I think. Like this:
var s = "...";
return implies(
proves(s, n1),
eval(outputs(1)));
Where s contains the source code of the entire snippet. I’d kinda assumed that quining and the diagonal lemma were the same thing, I guess that was wrong.
Quining is implied by the diagonal lemma, and but you can use the diagonal lemma like you’ve written. See this webpage on quines to understand the distinction. Wei Dai, it’s easy to convert between code strings and Gödel numbers, at least in theory. I don’t know about your particular example’s numbering, because that link isn’t working for me. You may want to find something specific to complexity theory, instead of math, which I suspect you (personally) would find more understandable. The quine page has a brief intro, which includes a proof of the fixed-point theorem.
In this case I think we have
B(x) = implies(proves(x, n1), eval(outputs(1)))
which is fine, but doesn’t bound the size of BOX. However, cousin_it specifies a way to keep BOX small using quining, so this proof seems legit to me. Its conclusion is just as unintuitive as Lob’s Theorem, but the steps all look all right.
Edit:
For an explicit way to compute fixed points, see the Y combinator.
The number n1 [...] grows with the computational complexities of n1,...,nmax
Why is this true? I am trying to understand. An obvious way to prove that eval(box) returns true is to go through the execution step by step. But when I write down what box is, it seems to call proves(box, n1) and eval(outputs(1)), which take much more than n1 steps.
Cousin_it, do you have an argument that n1 … n6 < nmax? It seems like one way for the proof to fail is if no matter what nmax is, step 11 forces n1 > nmax.
Only a very rough one, I’m afraid. The number n1 is chosen to “contain” the blow-up from the short proof of 10 to the proof of 11, which grows with the computational complexities of n1,...,nmax, not their values. These computational complexities can be made way smaller than n1.
Ok, I was checking if there was an obvious flaw that you might have missed. Now I’m trying to actually understand your proof, and I’m getting stuck on the first step, where you invoke the Diagonal Lemma. Now a typical statement of the Diagonal Lemma is:
Diagonal Lemma: If T is a theory in which diag is representable, then for any formula B(x) with exactly one free variable x there is a formula G such that G ⇔ B(g(G)) is a theorem in T. (g(G) is the Gödel number of G. This was copied from page 2 of http://www.cs.cornell.edu/courses/cs4860/2009sp/lec-23.pdf)
If you look at page 3 of that PDF, it gives an explicit formula for G, which happens to contain an existential quantifier. Now my question is, how do I translate that G into a code string (the one named “box” in your proof)? Also, is this supposed to be obvious, or are you assuming some background knowledge beyond the standard expositions of the Diagonal Lemma and Löb’s Theorem?
You can build “box” by quining, I think. Like this:
Where s contains the source code of the entire snippet. I’d kinda assumed that quining and the diagonal lemma were the same thing, I guess that was wrong.
Quining is implied by the diagonal lemma, and but you can use the diagonal lemma like you’ve written. See this webpage on quines to understand the distinction. Wei Dai, it’s easy to convert between code strings and Gödel numbers, at least in theory. I don’t know about your particular example’s numbering, because that link isn’t working for me. You may want to find something specific to complexity theory, instead of math, which I suspect you (personally) would find more understandable. The quine page has a brief intro, which includes a proof of the fixed-point theorem.
In this case I think we have B(x) = implies(proves(x, n1), eval(outputs(1))) which is fine, but doesn’t bound the size of BOX. However, cousin_it specifies a way to keep BOX small using quining, so this proof seems legit to me. Its conclusion is just as unintuitive as Lob’s Theorem, but the steps all look all right.
Edit: For an explicit way to compute fixed points, see the Y combinator.
You don’t need that to be a program for the proof to go through.
Why is this true? I am trying to understand. An obvious way to prove that eval(box) returns true is to go through the execution step by step. But when I write down what box is, it seems to call proves(box, n1) and eval(outputs(1)), which take much more than n1 steps.
n1 is chosen as to contain the size of the “box” statement, not its execution time.