Past exam of the model theory and Gödel's incompleteness theorems course of the University of Oxford / 2007 / A / 4

All implications in this argument are theorems of the extension $S$. From $Y\to (\square Y\to X)$, necessitation and normal modal distribution giveAxiom4 gives $\square Y\to \square \square Y$, soUnder the additional propositional antecedent $\square X\to X$, this theorem implies $\square Y\to X$. The reverse half of the fixed-point equivalence, $(\square Y\to X)\to Y$, consequently gives the theoremNecessitate that theorem and apply distribution to obtain $\square (\square X\to X)\to \square Y$. Combining with $\square Y\to \square X$ provesNecessitation was applied to a theorem after its propositional antecedent had been incorporated, never directly to a temporary assumption.

Take $\square A={\mathrm{Pr}}_{PA}(┌A┐)$ for the standard formal proof predicate symbol and putUse as given the arithmetization of syntax in PA, the derivability conditions, and the diagonal lemma. The latter supplies the fixed point needed in (a), and the former conditions interpret its normal modal distribution, necessitation on theorems and axiom4. Thus the argument in (a) proves the internal Löb implication in PA. With $X=\perp$ it readsThe inner implication is the first-order consistency first-order sentence $\neg \square \perp$, so contraposition givesThis is the arithmetic statement of the second incompleteness theorem proved within PA: if PA is first-order consistent, there is no PA formal proof of its first-order consistency first-order sentence. The displayed implication is a PA theorem without assuming that PA proves its antecedent.

For the corresponding external consequence, if a first-order consistent PA proved ${\mathrm{Con}}_{PA}$, theoremhood would give a formal proof of its boxed assertion. The displayed theorem together with the supposed formal proof of first-order consistency gives its negation, contradicting first-order consistency. Hence an externally first-order consistent PA does not prove its own first-order consistency.

Put $Y=\square X\to X$. The Löb axiom gives $\square Y\to \square X$. Consequently $Y$ implies $\square Y\to X$: if $\square Y$ holds, first obtain $\square X$ and then apply $Y$.

For the other direction, $X\to Y$ is a propositional theorem. Necessitation and distribution give $\square X\to \square Y$. Hence $\square Y\to X$ implies $\square X\to X$, which is $Y$. We have proved the unboxed theoremNecessitation yieldsThis is the explicit fixed point for the modalized operator $Z\mapsto (\square Z\to X)$.

Use the supplied uniqueness theorem for the modalized logical formula $A(p)=\square p\to X$. Its occurrence of $p$ is boxed, and the source assumes $p$ does not occur in $X$. Choose another first-order sentence letter $q$ absent from $X$ and from $p$. Besides the uniqueness theorem and propositional reasoning, use that GL is closed under uniform substitution in modal logic.

Let $Y=\square X\to X$. Uniformly substitute $Y$ for the fresh letter $q$ in the uniqueness theorem. Since $q$ occurs nowhere in $X$, this givesPart (c) proves the second conjunct outright. Propositional reasoning removes that already-proved conjunct and yieldsThe freshness conditions make the substitution legal and ensure it changes only the placeholder intended for the second fixed point.