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