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

Write $\mathrm{Prf}(n,m)$ for the specified proof relation and $R(n)$ for its Rosser provability predicate. If $R(\overline{n})$ is true in the standard natural numbers, its existential witness $m$ is the code of an actual proof of the expression with code $n$. Thus that expression is provable.

Conversely, suppose an actual proof has code $m$. If Peano arithmetic is consistent, there is no proof of the negation at all, in particular none with code at most $m$. The same $m$ therefore witnesses the bounded proof-order condition as well as the positive proof condition. Henceunder consistency. For numbers that do not code well-formed expressions, neither side holds under the usual proof coding. This is an external equivalence of theoremhood; it does not establish every internal derivability conditions for $R$.

Let $\perp$ abbreviate the fixed false arithmetic equality, and fix an actual proof of $\neg \perp$ with code $m$. For a proposed proof code $y\ge m$, that known proof of the negation already violates the bounded negative-proof test in $R(┌\perp ┐)$.

For the finitely many codes $y<m$, either one is an actual proof of $\perp$, in which case Peano arithmetic is inconsistent and proves the requested conclusion by explosion, or none is. In the latter case the finitely many true bounded facts $\neg \mathrm{Prf}(┌\perp ┐,\overline{y})$ are all provable by bounded completeness. Their conjunction excludes every code below $m$. The positive bounded fact that $m$ proves $\neg \perp$ is likewise provable. Splitting $y<m$ and $y\ge m$ inside arithmetic now givesThus the consistency statement for this Rosser provability predicate is provable. The argument uses only a fixed finite initial segment of proof codes; it does not prove the usual unbounded consistency statement.

The external necessitation rule assertion is valid. Suppose $PA⊢X$ and fix a proof code $m$. If $PA$ is inconsistent the assertion follows by explosion. Otherwise there is no actual proof of $\neg X$. Each of the finitely many bounded checks up to $m$ is therefore a true bounded arithmetic fact and is provable. Together with the positive proof check at $m$ this gives

The requested internal modus-ponens assertion needs an additional coding property. Combining a proof of $X$ and a proof of $X\to Y$ produces a proof of $Y$, but its code can exceed both original codes. The two Rosser hypotheses exclude proofs of $\neg X$ and $\neg (X\to Y)$ only up to their respective witness bounds. They provide no bound excluding proofs of $\neg Y$ below the new proof code. Ordinary internal modus ponens rule for the unbounded provability predicate does not fill this gap.

Consequently the premises printed here do not, just by themselves, justifyThis property varies with the Rosser proof-order dependence: some specially chosen proof predicates satisfy it, while general Rosser proof predicates need not. ^[ref].

The reference to a proof predicate “as given in the course” would need an explicit additional proof-order lemma to establish this part for that particular coding. Standard correctness on numeral instances and the ordinary Hilbert-Bernays-Löb derivability conditions alone are insufficient. The next solution gives the intended argument with the missing condition stated explicitly.

Assume additionally that the internal modus-ponens condition requested in part (c) holds for this $R$. If positive introspection also held for every sentence, then $R$ would satisfy all three Hilbert-Bernays-Löb derivability conditions: external necessitation rule was proved in part (c), modus ponens rule is the added condition, and introspection is the supposition.

The diagonal lemma applies to $R$ just as to any arithmetic formula. The usual Gödel second incompleteness theorem for a predicate with these conditions would then implywhen $PA$ is consistent. Part (b) proves the opposite. Therefore the three conditions cannot all hold, and under the added modus-ponens hypothesis there must be some sentence $X$ such thatThis is the intended contradiction argument and requires no identification of a particular $X$.

Without that extra hypothesis, the valid conclusion is only that at least one of internal modus ponens rule and positive introspection fails. Rosser predicates can be constructed that satisfy positive introspection, so a failure of that condition cannot be inferred from the printed general assumptions alone. ^[ref]. The distinction concerns proof coding, not a missing page of the exam.