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

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?

-
I have no complaints! (And I suspect the lack of complaints/negative feedback is a fair indicator of its quality.) I'm not in a position to know whether it's the shortest proof, but it seems rather apparent that it is not in any sense of the term inelegant! – amWhy Jan 20 '13 at 18:17

1 Answer

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\; M$$

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.
-
I should adopt this quasiquotation notation! – Zhen Lin Jan 21 '13 at 14:14
@HenningMaklholm "Pretty elegant" is good enough for me, thanks! :) Your comments are very interesting, and remind me that I really ought to get more up to speed on viewing things through Curry-Howard spectacles. If you were going to recommend one reasonably accessible book to look at for an illuminating treatment, what would you choose? – Peter Smith Jan 21 '13 at 16:30
(I should add that I know of the Morten Sørensen and Paweł Urzyczyn book, and have been meaning to read it for a while -- or is there a better place to start?) – Peter Smith Jan 21 '13 at 16:37
@PeterSmith: I haven't read the final version of the Sørensen-Uyzyczyn book, but I was in the graduate course the earliest (I think) draft of it was written for, and that was a really good course. I know nothing else I'd recommend over it. (I can't give any a reference that applies C-H specifically to metaprogramming, quasiquotes and the Hilbert-Bernays conditions -- I noticed by myself that they map to each other, but am probably not the first to do so. On the other hand, typed homogeneously staged metaprogramming is something of a specialty subject even within CS, so perhaps...). – Henning Makholm Jan 21 '13 at 18:57
Thanks for the confirmatory recommendation! – Peter Smith Jan 21 '13 at 19:24