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

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.