“this” should be a reference to the Gödel code of the current proof
the OP would like to have what is essentially an application of the diagonal lemma to the whole proof instead of a proposition
“zip”/”unzip” is simply taking the Gödel numbering, and doesn’t hide any extra complexity
In this case the problem here is making precise what one hopes for in step 2. (I don’t really see how one would do it), and then to prove that one can make it work.
part of my point is that the standard proof of löb does essentially apply the main idea of the diagonal lemma to the whole proof instead of to a proposition. when you look at the standard proof of löb from the right angle, it looks very similar to the standard standard proof of the diagonal lemma (namely, they both look like lawvere’s fixpoint theorem, as does the Y combinator).
löb lets you define a proof by reference to its own gödel-code, just like how the diagonal lemma lets you define a proposition by reference to its own gödel-code. (the former just happens to recurse into the latter at one point along the way, as an implementation detail.)
(“but wait, if the mechanisms are so similar, then why doesn’t the diagonal lemma have to recurse into the diagonal lemma at one point along the way, as an implementation detail?” it almost does! and this almost sinks the ship! the diagonal lemma requires an extra hacky insight, that works only in the special case of the diagonal lemma, and that is required to get off the ground. i discuss this in footnote 2 of my original comment, iirc.)
another part of my point is that the hard part of zip/unzip isn’t the part where you take the gödel-numbering, it’s the part where you make the gödel-numbering of the proof you’re currently naming available to the proof that you haven’t finished defining yet. that’s the tricky part of löb’s theorem. if we ignore that part, it’s no surprise that we find the remainder is simpler: we skipped the hard part!
(another thing that might help: when you’re proving an implication □ C → C, the gödel-number that you’re given doesn’t code for the proof of the implication you’re currently writing; that would be ill-typed. you asked for a □ C, not a □ (□ C → C). so the gödel-number you’re given isn’t a code for the thing you’re currently writing, it’s a code for löb’s theorem applied to the thing you’re currently writing.
it is for this reason that the proof you’re fed might not be exactly the proof you were hoping for. you started out your implication being like “step 1: this proof is a proof of C”, but then the proof that you’re fed starts out saying “step 1: apply löb’s theorem to the following implication”, and only at step 2 is it like “this proof is a proof of C”.
you might have really wanted the proof you’re fed to start with “step 1: this proof is a proof of C”. and you might say “well, inline the application of löb’s theorem there, so that the code i’m fed codes for a proof that actually starts that way”. this is like trying to get the fixpoint of f in the λ-calculus by way of f (f (f (...: you can do that for as many steps as you like, but you have to end at (Y f) at some point, on pain of infinite terms (which are contradictory in the mathematical setting).
alternatively, you might accept that the proof you’re fed codes for a proof that starts by saying “apply löb’s theorem to the following implication: …”; this corresponds to being fed the term (Y f) and producing the term f (Y f).
in neither case does it seem to me like there’s an idea for some alternative method of producing the self-reference, so as to sidestep the Y-combinator-esque machinery that makes up the bulk of the proof of löb’s theorem (and that is the source of the recursive call into the diagonal lemma).)
I was interpreting things somewhat differently:
“this” should be a reference to the Gödel code of the current proof
the OP would like to have what is essentially an application of the diagonal lemma to the whole proof instead of a proposition
“zip”/”unzip” is simply taking the Gödel numbering, and doesn’t hide any extra complexity
In this case the problem here is making precise what one hopes for in step 2. (I don’t really see how one would do it), and then to prove that one can make it work.
part of my point is that the standard proof of löb does essentially apply the main idea of the diagonal lemma to the whole proof instead of to a proposition. when you look at the standard proof of löb from the right angle, it looks very similar to the standard standard proof of the diagonal lemma (namely, they both look like lawvere’s fixpoint theorem, as does the Y combinator).
löb lets you define a proof by reference to its own gödel-code, just like how the diagonal lemma lets you define a proposition by reference to its own gödel-code. (the former just happens to recurse into the latter at one point along the way, as an implementation detail.)
(“but wait, if the mechanisms are so similar, then why doesn’t the diagonal lemma have to recurse into the diagonal lemma at one point along the way, as an implementation detail?” it almost does! and this almost sinks the ship! the diagonal lemma requires an extra hacky insight, that works only in the special case of the diagonal lemma, and that is required to get off the ground. i discuss this in footnote 2 of my original comment, iirc.)
another part of my point is that the hard part of zip/unzip isn’t the part where you take the gödel-numbering, it’s the part where you make the gödel-numbering of the proof you’re currently naming available to the proof that you haven’t finished defining yet. that’s the tricky part of löb’s theorem. if we ignore that part, it’s no surprise that we find the remainder is simpler: we skipped the hard part!
(another thing that might help: when you’re proving an implication □ C → C, the gödel-number that you’re given doesn’t code for the proof of the implication you’re currently writing; that would be ill-typed. you asked for a □ C, not a □ (□ C → C). so the gödel-number you’re given isn’t a code for the thing you’re currently writing, it’s a code for löb’s theorem applied to the thing you’re currently writing.
it is for this reason that the proof you’re fed might not be exactly the proof you were hoping for. you started out your implication being like “step 1: this proof is a proof of C”, but then the proof that you’re fed starts out saying “step 1: apply löb’s theorem to the following implication”, and only at step 2 is it like “this proof is a proof of C”.
you might have really wanted the proof you’re fed to start with “step 1: this proof is a proof of C”. and you might say “well, inline the application of löb’s theorem there, so that the code i’m fed codes for a proof that actually starts that way”. this is like trying to get the fixpoint of f in the λ-calculus by way of
f (f (f (...: you can do that for as many steps as you like, but you have to end at(Y f)at some point, on pain of infinite terms (which are contradictory in the mathematical setting).alternatively, you might accept that the proof you’re fed codes for a proof that starts by saying “apply löb’s theorem to the following implication: …”; this corresponds to being fed the term
(Y f)and producing the termf (Y f).in neither case does it seem to me like there’s an idea for some alternative method of producing the self-reference, so as to sidestep the Y-combinator-esque machinery that makes up the bulk of the proof of löb’s theorem (and that is the source of the recursive call into the diagonal lemma).)