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

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$.