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

The source's system called $K$ already contains positive introspection, so its displayed axioms are those usually called $K4$. PutWe first show that its axioms prove $\square A\to A$, the implication suggested in the hint. From $B$, positive introspection gives $\square B$. Distribution applied to $\square A=\square (B\to \square X)$ and $\square B$ gives $\square \square X$. Distribution applied to $B=\square (\square X\to X)$ and this last result gives $\square X$. Thus the theorem-level implications combine by propositional reasoning intowhich is $K4⊢\square A\to A$.

Since $S$ contains these axioms, it proves that implication. Its assumed Löb inference rule, applied to the first-order sentence $A$, yields $S⊢A$. Unpacking $A$ provesThis uses necessitation only as part of the ordinary modal theorem rules; no inference of a boxed temporary assumption has been made.

Let $C=\square X\wedge X$. The normal distribution axiom and necessitation of $C\to X$ give $\square C\to \square X$. Combining this with propositional reasoning yields the theoremIndeed, $X$ together with $\square C$ supplies both conjuncts of $C$. Necessitate this theorem and apply distribution to obtainThe new Löb axiom at $C$ now gives $\square X\to \square C$. Finally, necessitation and distribution applied to the tautology $C\to \square X$ give $\square C\to \square \square X$. Composition provesNo positive-introspection instance was used in deriving it. The argument shows why that scheme can be dropped when the Löb scheme is added.

Set $Y=\square X\to X$. The Löb axiom at $X$ is $\square Y\to \square X$. Therefore $Y$ and $\square Y$ together imply $X$, provingFor the converse, the tautology $X\to Y$ gives $\square X\to \square Y$ by necessitation and distribution. Consequently $\square Y\to X$ together with $\square X$ gives $X$, sowhose consequent is $Y$. Combining both directions gives an unboxed equivalence as a theorem of GL. Necessitation then yields exactly

Under the arithmetical interpretation $\square A=P_S(┌A┐)$, the Löb axiom says that a formal proof of the local reflection implication for $A$ already entails a formal proof of $A$:It is a formalized constraint on self-verification of a formal proof system. Externally, Löb's theorem says that if the system itself proves its own local reflection implication for $A$, it proves $A$. Distribution reflects closure of formal proofs under implication, necessitation reflects that a theorem has an arithmetically recognizable formal proof, and positive introspection reflects formal proof verification inside arithmetic.

Taking $A$ to be a refutable first-order sentence, especially a contradiction, recovers the obstruction behind the second incompleteness theorem: a first-order consistent sufficiently strong system cannot prove the corresponding claim that no formal proof of that first-order sentence exists. This does not identify provability with truth, nor grant the unrestricted factivity principle $\square A\to A$ as a theorem of the system. The Löb axiom is the characteristic additional scheme of Gödel–Löb provability logic.