I think this factoring hides the computational content of Löb’s theorem (or at least doesn’t make it obvious). Namely, that if you have f:□p→p, then Löb’s theorem is just the fixpoint of this function.
Here’s a one-line proof of Löb’s theorem, which is basically the same as the construction of the Y combinator (h/t Neel Krishnaswami’s blogpost from 2016):
löb(f):=let ψ:=(λψ:Ψ.f(ψ.fwd(‘‘ψ")) in ψ.bak(ψ)
where ‘‘ψ" is applying internal necessitation to ψ, and .fwd (.bak) is the forward (reps. backwards) direction of the point-surjection Ψ↔(□Ψ→p).
I think this factoring hides the computational content of Löb’s theorem (or at least doesn’t make it obvious). Namely, that if you have f:□p→p, then Löb’s theorem is just the fixpoint of this function.
Here’s a one-line proof of Löb’s theorem, which is basically the same as the construction of the Y combinator (h/t Neel Krishnaswami’s blogpost from 2016):
löb(f):=let ψ:=(λψ:Ψ.f(ψ.fwd(‘‘ψ")) in ψ.bak(ψ)where ‘‘ψ" is applying internal necessitation to ψ, and .fwd (.bak) is the forward (reps. backwards) direction of the point-surjection Ψ↔(□Ψ→p).