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