Is there a quicker argument from the HBL derivability conditions to the equivalence of fixed points of $\neg\Box$ to $\mathsf{Con}$?

Question

I'm just about to send off the final, final corrected PDF of the second edition of my Gödel book, and the following (neurotic?!?) question occurs to me.

In discussing matters around and about the Second Incompleteness Theorem, I use (of course) the three HBL derivability conditions governing the provability predicate for $T$

C1. If $T \vdash \varphi$, then $T \vdash \Box\varphi$,

C2. $T \vdash \Box\mathsf{(\varphi \to \psi)} \to (\Box\varphi \to \Box\psi)$,

C3. $T \vdash \Box\varphi \to \Box\Box\varphi$,

I give the following argument for the theorem that if $\gamma$ is fixed point for $\neg\Box$ in $T$ it is provably equivalent to $\neg\Box\bot$. [If you use "Gödel sentence", as some do, to mean a fixed point of $\neg\Box$, then this shows that, at least relative to a choice of provability predicate, Gödel sentences are provably equivalent.]

1. $T \vdash \gamma \equiv \neg\Box\gamma$
2. $T \vdash \gamma \to (\Box\gamma \to \bot)\quad\quad\text{From 1, by logic}$
3. $T \vdash \Box(\gamma \to (\Box\gamma \to \bot))\quad\quad\text{From 2 by C1}$
4. $T \vdash \Box\gamma \to \Box(\Box\gamma \to \bot))\quad\quad\text{From 3, by C2}$
5. $T \vdash \Box\gamma \to (\Box\Box\gamma \to \Box\bot)\quad\quad \text{From 4, by C2}$
6. $T \vdash \Box\gamma \to \Box\Box\gamma\quad\quad \text{From C3}$
7. $T \vdash \Box\gamma \to \Box\bot\quad\quad \text{From 5 and 6}$
8. $T \vdash \bot \to \gamma\quad\quad\text{Logic}$
9. $T \vdash \Box(\bot \to \gamma)\quad\quad \text{From 8, by C1}$
10. $T \vdash \Box\bot \to \Box\gamma \quad\quad \text{From 9, by C2}$
11. $T \vdash \Box\gamma \equiv \Box\bot \quad\quad \text{From 7 and 10}$
12. $T \vdash \gamma \equiv \neg\Box\bot \quad\quad \text{From 1 and 11}$

Question/problem: This is the proof that was in the first edition, and no one complained -- but is this the shortest proof? Or have I gone round the houses in an inelegant way?

Answer 1

It's pretty elegant from my computer-science viewpoint:

Viewed through the Curry-Howard correspondence, the HBL conditions correspond to basic typed metaprogramming, where $\Box \tau$ is the type of closed fragments of program text of type $\tau$. If for readability we write $\Box \tau$ as $[\tau]$ and the arrow associates to the right, the conditions are

C1. If $M$ is a closed term of type $\tau$, then $\ulcorner M\urcorner$ is a term of type $[\tau]$.

C2. For every $\alpha$ and $\beta$ there's a term $\mathtt{App}_{\alpha,\beta}$ of type $[\alpha\to\beta]\to[\alpha]\to[\beta]$.

C3. For every $\alpha$ there's a term $\mathtt{Lift}_{[\alpha]}$ of type $[\alpha]\to\bigl[[\alpha]\bigr]$.

Conditions C1 and C2 allow us to form quasiquotations: $$ \ulcorner \cdots \llcorner M \lrcorner \cdots \urcorner \qquad\text{means}\qquad \mathtt{App}\;\ulcorner \lambda x. \cdots x \cdots \urcorner\; \ulcorner M \urcorner$$

In your proof given $\gamma \equiv \Box\gamma\to\bot$, you're assuming a term $\mathtt{p}: \gamma\to[\gamma]\to\bot$. You also have, from logic, $\mathtt{Explode}:\bot\to\alpha$ for all $\alpha$.

Your proof now corresponds to constructing, (with some $\beta\eta$-redexes from the quasiquote translation already reduced):

$$\lambda x.\ulcorner \mathtt p\;\llcorner x\lrcorner\;\llcorner \mathtt{Lift}\;x\lrcorner\urcorner ~:~ [\gamma]\to[\bot] $$ $$ \lambda x:\ulcorner \mathtt{Explode}\;\llcorner x \lrcorner\urcorner ~:~ [\bot]\to[\gamma] $$

It is difficult to see how that could be done shorter. Essentially all of what you do appears to be necessary set-up for being able to use $\mathtt{p}$ for anything, given that $\mathtt{Lift}$ only works when you already have one $\Box$.

I toyed a bit with starting from $\delta\equiv\Box\neg\delta$ instead, but that seems to lead nowhere.

---

By the way, I can't resist pointing out that the usually fairly impenetrable standard modal proof of Löb's theorem becomes very simple and beautiful through this correspondence. The premise of the theorem is that we know a term $\mathtt{eval}$ of type $[\tau]\to\tau$ (where the name "eval" is suggestive but not quite trustworthy because all we really know is that $\mathtt{eval}$ will produce some value of type $\tau$, not necessarily one related to the input to $\mathtt{eval}$).

Löb's theorem (and the standard proof) then simply observes that the type $\tau$ is inhabited by a program that goes:

1. Produce a copy of my own source code, by the fixpoint property.
2. Apply $\mathtt{eval}$ to that source code and output its result.