Is there a quicker argument from the HBL derivability conditions to the equivalence of fixed points of $\neg\Box$ to $\mathsf{Con}$?
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:
- Produce a copy of my own source code, by the fixpoint property.
- Apply $\mathtt{eval}$ to that source code and output its result.