Gödel's incompleteness theorems course of the University of Oxford (C1.1a)

Write $BA=P(┌A┐)$, with the corner notation understood as the numeral for the Gödel number. An arithmetical provability predicate numerates the theorems of $S$ in the standard natural numbers and satisfies the Hilbert-Bernays-Löb derivability conditions:The last two conditions are internal theorems, not rules authorizing reflection from $BA$ to $A$.

Here $P(x)=\exists y\mathrm{Prov}(x,y)$ numerates the theorem set by the given assumption. If $S⊢A$, its proof supplies a genuine natural-number witness, making $BA$ a true Sigma-1 formula. Sigma-1 completeness gives $S⊢BA$, proving the first condition. The second condition is supplied explicitly. Since $BA$ is itself a Sigma-1 formula, the given formalized Sigma-1 completeness yields $S⊢BA\to B(BA)$, the third condition. Thus the specified existential proof predicate is an arithmetical provability predicate.

Write $BA=\exists y\mathrm{Prov}(┌A┐,y)$ and fix a refutable first-order sentence $\perp$, so $S⊢\neg \perp$ and ${\mathrm{Con}}_S=\neg B\perp$. First prove the internal equivalenceBecause $\perp \to G$ is provable, the derivability conditions give $B\perp \to BG$. The fixed-point equivalence $G\leftrightarrow \neg BG$ therefore yields $G\to \neg B\perp$.

For the reverse implication, necessitating $G\to \neg BG$ and applying distribution gives $BG\to B(\neg BG)$. positive introspection gives $BG\to B(BG)$. Finally the provable implication $BG\to (\neg BG\to \perp )$, necessitated and distributed, givesConsequently $S⊢BG\to B\perp$, so $\neg B\perp \to \neg BG\to G$. The same argument works with any chosen refutable first-order sentence in place of $\perp$; their formal consistency statements are provably equivalent.

By the classical deduction theorem for propositional logic applied to adjoining a first-order sentence, $S+\{G\}$ is consistent exactly when $S⊬\neg G$. The displayed equivalence makes $S+\{G\}$ and $S+\{{\mathrm{Con}}_S\}$ deductively equivalent. ThereforeNo soundness assumption on that extension is being substituted for consistency.

If $S$ is inconsistent, it proves $\neg R$ by explosion. Conversely, suppose $S$ is consistent and, towards a contradiction, has a proof of $\neg R$ with standard code $n$. Consistency excludes any proof of $R$. In particular, for each $k\le n$, the closed bounded statement $\neg \mathrm{Prov}(┌R┐,\overline{k})$ is true and is provable in $S$ by Sigma-1 completeness. The true bounded statement $\mathrm{Prov}(┌\neg R┐,\overline{n})$ is also provable.

Using the given finite-numeral exhaustion below $\overline{n}$, these finitely many nonproof facts giveFor arbitrary $y$, the given comparison splits into $y\le \overline{n}$ or $\overline{n}\le y$. In the first case the antecedent $\mathrm{Prov}(┌R┐,y)$ is false. In the second case the known negative proof at code $\overline{n}$ supplies the required witness $z\le y$. Hence $S$ provesThe Rosser sentence equivalence now gives $S⊢R$, contradicting consistency. ThusOnly a fixed finite list of closed bounded facts was used; no assumption that the first-order theory is omega-consistent is needed.

The preceding Gödel sentence argument gives $S⊢G\to {\mathrm{Con}}_S$. The permitted arithmetized positive half of the Rosser sentence argument isPure first-order logic gives $\neg BR\to R$: if there is no proof of $R$, each antecedent in its defining universal implication is false. ThereforeThis uses the supplied internal Rosser implication, rather than replacing an external nonprovability fact by an unproved internal first-order sentence.

Let $T=S+\{{\mathrm{Con}}_S\}$ and assume $T$ is consistent. The allowed arithmetizations of the previous equivalences giveSuppose $S⊢R\to G$. Its contrapositive is $\neg G\to \neg R$, and the Hilbert-Bernays-Löb derivability conditions then giveCombining with the two internal equivalences yields $S⊢{\mathrm{Con}}_S\to \mathrm{Con}(T)$. Since $T$ contains ${\mathrm{Con}}_S$, it would prove $\mathrm{Con}(T)$, contrary to the given Gödel second incompleteness theorem for this consistent extension. HenceTogether with the preceding implication, this is the Strict Gödel-to-Rosser implication under the stated consistency hypothesis.

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.

The Gödel-Löb logic $\mathrm{GL}$ uses propositional variables, $\perp$, implication, and a unary modal operator $\square$. Other Boolean connectives are abbreviations; for example $\neg A$ means $A\to \perp$ and $\top$ means $\perp \to \perp$.

Its axioms are all classical propositional tautologies and the two schemesIts rules are the modus ponens rule and the necessitation rule, $\mathrm{GL}⊢A\Rightarrow \mathrm{GL}⊢\square A$. Uniform propositional substitution is allowed, or equivalently built into the axiom schemes. necessitation rule applies to theorems; a temporary assumption cannot simply be boxed. In provability logic, $\square A$ is read as the formal assertion that $A$ is provable.

Induct on a derivation in Gödel-Löb logic. Propositional axiom instances translate to theorems of Peano arithmetic. The image of $\perp$ is a refutable sentence, so it behaves as falsity in those translated propositional arguments.

The translation of axiom $\mathrm{K}$ is the distribution clause of the Hilbert-Bernays-Löb derivability conditions. The translation of axiom $\mathrm{L}$ isthe Internal form of Löb's theorem, whose derivation was given above and applies to the stipulated arithmetical provability predicate for Peano arithmetic. Thus every axiom has a provable translation.

The modus ponens rule is preserved because the interpretation commutes with implication. The necessitation rule is preserved by the first derivability condition: if $\mathrm{PA}⊢{\mathcal{I}}_i(A)$, thenHere the equality denotes the definition of the translated formula, not an arithmetic equality of truth values. A propositional substitution merely changes the arithmetic sentences assigned to the variables. The induction proves the Arithmetical soundness of GL:

Take $Y(p)=p\to q$ and put $\top =(\perp \to \perp )$, $H=Y(\top )$ and $F_0=Y(\square H)=\square H\to q$. The first supplied substitution identity readsUse the supplied replacement of equivalents in the context $D(p)=p\to q$. It givesBut $H=(\top \to q)$ is equivalent to $q$. Replacement under a box gives $\square H\leftrightarrow \square q$, so $F_0$ is equivalent toReplacing equivalents once more transfers the fixed-point equation to $F$, proving $\mathrm{GL}⊢F\leftrightarrow (\square F\to q)$.

A direct check of this GL fixed point for a provability implication is useful: the Löb axiom gives $\square F\to \square q$, and necessitating the tautology $q\to F$ gives $\square q\to \square F$ by $\mathrm{K}$. Thus $\square F\leftrightarrow \square q$, and replacing the antecedent in $\square F\to q$ recovers $F$.

Use the preceding fixed point with $q=\perp$. If the chosen arithmetic interpretation sends $\perp$ to a PA-refutable sentence $Z$, it gives the arithmetic sentenceThis follows from Arithmetical soundness of GL. Since Peano arithmetic proves $\neg Z$, the two implications are equivalent to negated provability:Thus $C$ expresses the formal consistency statement for Peano arithmetic and is also a negative provability fixed point, like its Gödel sentence $G$.

Apply the supplied modal uniqueness formula to the context with a modalized occurrence $X(p)=(\square p\to \perp )$, with two fresh variables interpreted as $G$ and $C$. A modalized occurrence means that each indicated variable occurrence lies inside a box. Peano arithmetic proves both arithmetic fixed-point equations. The first derivability condition boxes those equations, so the translated uniqueness formula givesOne must not infer $G\leftrightarrow C$ by reflection. Instead, distribution and the provability of the two propositional projections give $\mathrm{PA}⊢BG\leftrightarrow BC$. Negating and using the two fixed-point equations now yieldsThis proves the Equivalence of a Gödel sentence and a consistency statement using the required modal soundness, fixed point and uniqueness results.