Past exam of the Gödel's incompleteness theorems course of the University of Oxford / 2011 / 2

Löb's theorem states that, for a first-order theory with the stated provability and diagonalization properties,where $BA=P_S(┌A┐)$. It does not require an extra consistency assumption.

By the diagonal lemma, choose $D$ with $S⊢D\leftrightarrow (BD\to A)$. necessitation rule and distribution applied to $D\to (BD\to A)$ giveUsing positive introspection $BD\to B(BD)$ gives the unconditional theorem $S⊢BD\to BA$. If $S⊢BA\to A$, it follows that $S⊢BD\to A$, and the reverse fixed-point implication gives $S⊢D$. Necessitating gives $S⊢BD$, hence $S⊢BA$ and finally $S⊢A$.

The same derivation also gives the Internal form of Löb's theorem, needed for modal soundness. Put $H=(BA\to A)$. From the unconditional $BD\to BA$, propositional reasoning and the fixed point give $S⊢H\to D$. necessitation rule and distribution imply $S⊢BH\to BD$, and henceThis internal statement was derived without necessitating a temporary assumption.

The Gödel second incompleteness theorem says that a consistent, effectively axiomatized first-order theory with enough arithmetic and its standard derivability and diagonalization properties cannot prove its formal consistency statement ${\mathrm{Con}}_S=\neg B\perp$.

If a consistent $S$ proved ${\mathrm{Con}}_S$, it would prove $B\perp \to \perp$ by classical propositional logic. Apply Löb's theorem to $A=\perp$. This would give $S⊢\perp$, contradicting consistency. ThereforeFor an inconsistent first-order theory the conclusion need not hold, since it proves every first-order sentence.

Assume $S⊢\neg X$ and $S⊢BX\to X$. Combining these theorems gives $S⊢\neg BX$. Because $X$ is refutable, $\neg BX$ is a legitimate formal consistency statement for $S$: the standard contradiction first-order sentence and $X$ are provably interderivable, and the derivability conditions transfer those implications to their provability statements.

Thus if $S$ were consistent, the Gödel second incompleteness theorem would contradict $S⊢\neg BX$. Consequently the assumed reflection theorem forces $S$ to be inconsistent; explosion then gives $S⊢X$. This establishes the instance of Löb's theoremfor every $X$ refutable in $S$, using only the second incompleteness theorem.

Assume $S⊢B_{S}X\to X$ and put $T=S+\{\neg X\}$. Then $T⊢\neg B_{S}X$. The given extension-provability implication, with $Y=\perp$, givesThe provable classical implication $(\neg X\to \perp )\to X$, together with distribution, gives $S⊢B_S(\neg X\to \perp )\to B_{S}X$. HenceIf $T$ were consistent, this would violate its Gödel second incompleteness theorem. Thus $T$ is inconsistent. The deduction theorem for propositional logic and double-negation elimination give $S⊢\neg \neg X$, hence $S⊢X$. Therefore the second incompleteness theorem for $S+\{\neg X\}$ yields Löb's theorem for arbitrary $X$.

Use just the assumed local reflection instance with $Y=\neg X$:By the deduction theorem for propositional logic, $S⊢X\to (B_S(\neg X)\to \neg X)$. Classical propositional logic makes this imply the unconditional reflection statement $S⊢B_S(\neg X)\to \neg X$: if $X$ is false the consequent is already true, and if $X$ is true the displayed implication supplies it. Löb's theorem applied to $\neg X$ now givesThus full local reflection in a one-sentence extension is inconsistent; in this argument even the single instance concerning $\neg X$ suffices.

Put $T=S+\{X\}$ and choose its Gödel sentence $Z$, so $T⊢Z\leftrightarrow \neg B_{T}Z$. The assumed reflection scheme gives the particular theoremThe given extension-provability implication is $S⊢B_{T}Z\to B_S(X\to Z)$. The fixed-point equivalence gives $T⊢\neg Z\to B_{T}Z$, so these implications compose toThe supplied propositional tautology $((\neg Z\to (X\to Z))\to (X\to Z))$ gives $T⊢X\to Z$, and $T⊢X$ then yields $T⊢Z$. The first of the derivability conditions for $T$ gives $T⊢B_{T}Z$, while its Gödel equivalence gives $T⊢\neg B_{T}Z$. Hence $T$ is inconsistent. By the deduction theorem for propositional logic,This proof uses diagonalization and proof transfer for the extension, and invokes neither Löb's theorem nor the second incompleteness theorem.