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

Gödel's second incompleteness theorem says that a consistent effectively presented arithmetic theory with an adequate proof predicate cannot prove its formal consistency statement. The background strength must support the diagonal lemma and the derivability conditions, as in the present arithmetic setting.

Löb's theorem saysIt is a theorem about derivability for every sentence $A$, not merely an external soundness assertion about the interpretation of $\square$. Taking $A=\perp$, a proof of consistency gives $S⊢\square \perp \to \perp$; Löb then gives $S⊢\perp$. Thus a consistent $S$ cannot prove consistency. This is how the second incompleteness theorem is the contradiction-sentence instance of Löb's more general result.

Suppose $S+A$ proves every specified reflection instance. Use only the instance with $X=\neg A$. The deduction theorem givesClassical propositional reasoning turns this into $S⊢\square \neg A\to \neg A$: if $\neg A$ already holds the implication is true, while otherwise $A$ holds and the displayed theorem supplies it. Löb's theorem now yields $S⊢\neg A$, making $S+A$ inconsistent. Therefore no sentence consistent with $S$ can supply all the local reflection instances in a one-sentence extension. The proof uses just one well-chosen instance, and never applies necessitation to a derivation with the extra assumption still open.

GL has all classical propositional tautologies, the normal distribution axiom $\square (A\to B)\to (\square A\to \square B)$ and the Löb axiom $\square (\square A\to A)\to \square A$, closed under uniform substitution, modus ponens and necessitation of theorems. We use its derived positive-introspection theorem $\square A\to \square \square A$, normal boxed reasoning, and the boxed replacement principle supplied in the question.

For completeness, positive introspection follows from these axioms. Put $C=A\wedge \square A$. Distribution gives $\square C\to \square A$, so propositional logic proves $A\to (\square C\to C)$. Necessitate and distribute to get $\square A\to \square (\square C\to C)$; Löb's axiom gives $\square A\to \square C$, and boxing $C\to \square A$ finishes $\square A\to \square \square A$.

For a GL fixed point by truth substitution, set $\top =(\perp \to \perp )$, $U=\square Y(\top )$ and $V=\square Y(U)$. From the tautology $U\to (\top \leftrightarrow U)$, boxed reasoning gives $\square U\to \square (\top \leftrightarrow U)$. The supplied replacement principle and distribution then giveSince $U$ is itself boxed, positive introspection gives $U\to \square U$, and hence $U\to V$.

For the reverse direction, the displayed implication entails the theorem $V\to (\square U\to U)$. Necessitate it and distribute to obtain $\square V\to \square (\square U\to U)$. Since $V$ is boxed, $V\to \square V$ holds. The Löb axiom therefore yields $V\to \square U$, and the same displayed implication then yields $V\to U$. ConsequentlyAll occurrences of the unknown letter have been removed from $U$ by substitution of truth; any other parameter letters remain available. The proof does not assume the invalid reflection principle $\square U\to U$ as an unconditional axiom.

The fixed point of boxed negated provability gives, in fact, that GL proves $F\leftrightarrow \square \perp$. Here is a direct derivation. Since $F$ is provably equivalent to a boxed formula, positive introspection and necessitation of that equivalence give $F\to \square F$. Another introspection step gives $F\to \square \square F$. The stipulated fixed point also gives $F\to \square \neg \square F$. Combining these two boxed contradictories yields $F\to \square \perp$. Conversely $\square \perp \to \square \neg \square F$ follows by normal boxed explosion, and the fixed point then yields $\square \perp \to F$.

Arithmetical soundness of GL, proved by translating distribution into the second derivability condition, necessitation into the first, and Löb's axiom into its internal arithmetic theorem, now givesAny remaining propositional parameters may be assigned arbitrary arithmetic sentences; this equivalence is uniform in those assignments. If PA is one-consistent, it is consistent and ${\Sigma }_1$ sound. Its standard provability predicate for a contradiction is then a false ${\Sigma }_1$ sentence and cannot be a theorem. Hence $F^{\ast }$ is not provable in PA. Moreover its negation is equivalent to PA's consistency statement and is unprovable by the second incompleteness theorem. Thus this fixed point is, under the stated hypothesis, undecidable rather than an unboxed reflection principle.