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

An arithmetic logical formula is ${\Sigma }_0$, or bounded, if all its quantifiers are bounded by arithmetical first-order terms. A ${\Sigma }_1$ logical formula has an initial block of existential quantifiers followed by a bounded matrix, up to the usual logical transformations. Soundness of an arithmetic theory at a given level means that every first-order sentence of that level proved by the first-order theory is true in the standard natural numbers. Here ${\Sigma }_0$-completeness means that every true bounded arithmetic sentence is provable.

A first-order theory is one-consistent if there is no bounded arithmetic formula $A(x)$ for which it proves $\exists xA(x)$ while proving $\neg A(\bar{n})$ for every standard natural number $n$. This is a restricted form of omega-consistency. In particular one-consistency implies first-order consistency, since an inconsistent first-order theory proves every first-order sentence and its negation.

Suppose a ${\Sigma }_0$-complete first-order theory $S$ is first-order consistent. If it proved a false bounded arithmetic sentence $\theta$, the true bounded arithmetic sentence $\neg \theta$ would also be provable by completeness, contradicting first-order consistency. Thus $S$ is ${\Sigma }_0$-sound. Conversely ${\Sigma }_0$-soundness excludes inconsistency because an inconsistent first-order theory proves the false bounded arithmetic sentence $0=1$. ThereforeIf $S$ is one-consistent but proved a false existential sentence $\exists xA(x)$ with bounded matrix, every standard instance $\neg A(\bar{n})$ would be true and hence provable. This violates one-consistency. Thus it is ${\Sigma }_1$-sound. Conversely, ${\Sigma }_1$-soundness implies first-order consistency by the previous argument, since bounded arithmetic sentences are included at the existential level. If $S$ proved $\exists xA(x)$, soundness of an arithmetic theory would give a standard witness $n$ with $A(n)$ true. Bounded completeness of an arithmetic theory would then give $S⊢A(\bar{n})$, so first-order consistency prevents simultaneous formal proofs of all the negated instances. HenceMultiple existential logical variables can be treated as a finite tuple of witnesses; the same reasoning applies.

The definition of $a$ makes the diagonal instance $E_a[\bar{a}]$ exactly $G_S$. The representing logical formula therefore has the standard interpretationIf $S⊢G_S$, choose an actual witness $m$ to the left-hand existential statement. The bounded arithmetic sentence $A(\bar{a},\bar{m})$ is true and hence provable by ${\Sigma }_0$-completeness. But $G_S$ also gives $S⊢\neg A(\bar{a},\bar{m})$, a contradiction. ThusNow assume one-consistency. It implies first-order consistency, so no formal proof of $G_S$ exists and $A(a,m)$ is false for each standard $m$. Each bounded arithmetic sentence $\neg A(\bar{a},\bar{m})$ is consequently true and provable. A formal proof of $\neg G_S$ would give a formal proof of $\exists v_{2}A(\bar{a},v_2)$ while every standard witness instance is refuted, contrary to one-consistency. HenceThe two hypotheses play different roles: ordinary first-order consistency excludes the positive Gödel sentence, while the stronger hypothesis also excludes its negation.

By the standard interpretation of the representing logical formula,If $S$ is first-order consistent, part (b) supplies the right-hand side, so $G_S$ is true. If $S$ is inconsistent, explosion gives $S⊢G_S$, so the representing existential statement is true and $G_S$ is false. ThereforeThis is an external truth assertion about the standard natural numbers. Formalizing that assertion inside a first-order theory requires the additional facts explicitly supplied in part (d).

Put $T=S\cup \{\neg G_S\}$. The first supplied equivalence, retained in $T$, combines with its new axiom to giveThe supplied implication $\mathrm{Con}(T)\to \mathrm{Con}(S)$ then yields, by contraposition,Finally the second supplied equivalence is $T⊢G_T\leftrightarrow \mathrm{Con}(T)$, so propositional reasoning givesNo extra first-order consistency assumption is needed for this formal derivation. If $S$ is first-order consistent, part (b) shows that adding $\neg G_S$ preserves first-order consistency, because inconsistency of the extension would imply $S⊢G_S$. Such a first-order consistent extension therefore proves the negation of its own true Gödel sentence, illustrating why first-order consistency alone does not imply one-consistency.

Write $\rho ={\mathrm{Pr}}_{PA}^{\ast }(┌R┐)$. The supplied fixed-point equivalence gives $PA⊢R\leftrightarrow \neg \rho$.

If PA proved $R$, the first assumed property would give $PA⊢\rho$, while the equivalence would give $PA⊢\neg \rho$. This contradicts first-order consistency. If PA proved $\neg R$, the second assumed property would give $PA⊢\neg \rho$, and the reverse implication of the equivalence would give $PA⊢R$, again a contradiction. HenceThis is the Rosser improvement: its comparison of formal proof codes permits ordinary first-order consistency to exclude both alternatives, without assuming one-consistency.

If PA is inconsistent, every desired conclusion is already a theorem, so it suffices to analyze the first-order consistent case. Use $Q(u,v)$ for the bounded arithmetical proof relation and $\mathrm{neg}(u)$ for the code of the negation of the logical formula coded by $u$.

Suppose $PA⊢E_n$ and let $m$ be the code of an actual formal proof. By first-order consistency there is no formal proof of $\neg E_n$, in particular none with code at most $m$. Thusis a true bounded arithmetic sentence. Bounded completeness of an arithmetic theory proves it in PA, and existential introduction gives $PA⊢{\mathrm{Pr}}_{PA}^{\ast }(\bar{n})$.

Conversely suppose $PA⊢\neg E_n$ and choose an actual formal proof code $k$ of that negation. First-order consistency excludes every formal proof of $E_n$, so each of the finitely many statements $\neg Q(\bar{n},\bar{j})$ for $j<k$ is true and provable. The supplied finite-case theorem permits PA to combine them into the assertion that no formal proof code below $k$ proves $E_n$.

PA also proves $Q(\overline{\mathrm{neg}(n)},\bar{k})$. For any candidate formal proof code $v\ge \bar{k}$, this one code already refutes the universal no-earlier-negation condition in the Rosser predicate symbol. For $v<\bar{k}$, the finite verification refutes its positive formal proof condition. The supplied order dichotomy and finite-case expansion cover all $v$. ThereforeThe argument uses bounded verification of a finite initial segment and one fixed counter-witness beyond it; it does not infer that PA proves the absence of all ordinary formal proofs merely from first-order consistency.

If PA is first-order consistent and already proves $\neg X$, it cannot also prove $X$. By the correctness of the ordinary arithmetized arithmetical proof relation, $\mathbb{N}\models \neg {\mathrm{Pr}}_{PA}(┌X┐)$.

If PA is inconsistent, it proves $X$ by explosion, so an actual formal proof code witnesses ${\mathrm{Pr}}_{PA}(┌X┐)$ in the standard natural numbers. ThusThe hypothesis that $X$ is refutable is essential to this first-order consistency characterization for an arbitrary fixed first-order sentence.

Let $C$ denote the addition-commutativity first-order sentence and put $d=┌\neg C┐$. In the ordinary checker for PA derivations, replace the axiom test ${\mathrm{Ax}}_{PA}(u)$ byKeep all tests for sequence formation, earlier lines, logical axiom schemes and inference rules unchanged. This gives a formal proof checker $Q_S(u,w)$ which recognizes exactly ordinary $S$-derivations. The finite syntactic modification is arithmetizable by the same bounded coding apparatus as the original checker.

For the proof-order comparison in the next part, make the choice of coding explicit. Reserve code $0$ for the one-line derivation of the newly added axiom $\neg C$, and give an ordinary derivation with code $w$ the new code $w+1$. A corresponding bounded relation isEvery code has a specified decoding, every genuine formal proof is represented, and no false formal proof is admitted. The reserved code duplicates one genuine derivation, which is harmless. This is one explicit arithmetized arithmetical proof relation obtainable from the PA checker by the requested axiom change and a simple renumbering. Stating the proof-order convention matters because a Rosser predicate symbol uses code order, not merely the existence of formal proofs.

Use the arithmetical proof relation and coding just constructed. A formal proof of $C$ cannot have code $0$, since that code was reserved for $\neg C$. Every candidate code $v$ for a formal proof of $C$ is therefore positive. But code $0\le v$ is already a formal proof of $\neg C$, so the no-earlier-negation condition fails for every candidate. HencePA proves $C$ by induction, while $S$ has $\neg C$ as an added axiom. Thus $S$ is inconsistent and its ordinary arithmetical provability predicate is true of every first-order sentence, including $C$. The displayed negative Rosser assertion can nevertheless be true, because the Rosser condition compares the order of opposite formal proofs rather than asking for their mere existence.

There is an important coding qualification. The PDF refers to a course formal proof coding but does not specify its numerical ordering. The truth of this Rosser assertion for an inconsistent first-order theory is not coding-invariant, so formal proof length alone cannot establish it for an unspecified fixed coding. For example, a different legitimate numbering could reserve code $0$ for a known PA formal proof of $C$, code $1$ for the new axiom $\neg C$, and higher codes for all other derivations. Then code $0$ would witness ${\mathrm{Pr}}_S^{\ast }(┌C┐)$ instead. The explicit allowed construction in part (i) supplies a convention under which the requested assertion holds; interpreting it as a claim about some externally fixed course numbering requires that numbering's corresponding order property.

Use the Hilbert-Bernays-Löb derivability conditions for an arithmetical provability predicate. Abbreviate $P_S(┌A┐)$ by $PA$. The conditions needed below areThese are the usual theoremhood, distribution and positive-introspection conditions intended by a standard arithmetical provability predicate; arbitrary predicate symbols merely agreeing with provability externally need not satisfy them.

Since $S⊢\neg Y$, it proves $Y\to G$. The first two conditions give $S⊢PY\to PG$. For the converse, the fixed-point equivalence gives $S⊢G\to (PG\to Y)$. Applying theoremhood and distribution givesPositive introspection also gives $PG\to PPG$, and distribution combines these to yield $S⊢PG\to PY$. Thus $S⊢PG\leftrightarrow PY$. Combining with $G\leftrightarrow \neg PG$ provesIf $S$ proved $\neg PY$, it would prove $G$. The theoremhood condition would then give $PG$, while the fixed-point equivalence gives $\neg PG$. Therefore first-order consistency implies

Put $T=S\cup \{\neg X\}$ and assume $S⊢P_S(┌X┐)\to X$. In $T$, contraposition against its extra axiom gives $\neg P_S(┌X┐)$.

Classical logic proves $(\neg X\to X)\to X$. By the derivability conditions,Compose this with the supplied formalized deduction implication from $P_T(┌X┐)$ to its left-hand side. Then $T$ provesand thereforeThe other supplied assumption says this is impossible if $T$ is first-order consistent. Thus $T$ is inconsistent. By the deduction theorem, inconsistency after adjoining $\neg X$ yields $S⊢\neg \neg X$, henceThis establishes Löb's inference rule using precisely the strengthened unprovability assumption and the formalized deduction property supplied in the question.

Take a first-order sentence $Y$ refutable in $S$ and suppose, toward contradiction, that a first-order consistent $S$ proved $\neg P_S(┌Y┐)$. Propositional logic would then giveLöb's inference, applied with $X=Y$, would give $S⊢Y$, contradicting the existing formal proof of $\neg Y$. Hence first-order consistency excludes the proposed formal proof of non-provability.

Thus the familiar unprovability of the first-order consistency statement associated with a refutable first-order sentence is a special consequence of the general ruleThe general rule applies to every first-order sentence, not just a chosen false or refutable one.

Let $j=i+n$ with $n\ge 1$. Positive introspection supplies the theorem $F_k\to F_{k+1}$ for every $k\ge 1$, since $F_k$ itself has the form $P_S(┌F_{k-1}┐)$.

Induction on $n$ consequently givesAt $n=1$ this is the identity implication. To pass from $n$ to $n+1$, compose the induction hypothesis with the positive-introspection implication at $k=i+n$, which is at least one. Composing the result with the assumed $F_j\to F_i$ givesi.e. $S⊢P_S(┌F_i┐)\to F_i$. Löb's rule now yieldsThe index restriction on positive introspection has been respected even when $i=0$: the chain begins at $F_{i+1}$, which already is a provability assertion.

The source's system called $K$ already contains positive introspection, so its displayed axioms are those usually called $K4$. PutWe first show that its axioms prove $\square A\to A$, the implication suggested in the hint. From $B$, positive introspection gives $\square B$. Distribution applied to $\square A=\square (B\to \square X)$ and $\square B$ gives $\square \square X$. Distribution applied to $B=\square (\square X\to X)$ and this last result gives $\square X$. Thus the theorem-level implications combine by propositional reasoning intowhich is $K4⊢\square A\to A$.

Since $S$ contains these axioms, it proves that implication. Its assumed Löb inference rule, applied to the first-order sentence $A$, yields $S⊢A$. Unpacking $A$ provesThis uses necessitation only as part of the ordinary modal theorem rules; no inference of a boxed temporary assumption has been made.

Let $C=\square X\wedge X$. The normal distribution axiom and necessitation of $C\to X$ give $\square C\to \square X$. Combining this with propositional reasoning yields the theoremIndeed, $X$ together with $\square C$ supplies both conjuncts of $C$. Necessitate this theorem and apply distribution to obtainThe new Löb axiom at $C$ now gives $\square X\to \square C$. Finally, necessitation and distribution applied to the tautology $C\to \square X$ give $\square C\to \square \square X$. Composition provesNo positive-introspection instance was used in deriving it. The argument shows why that scheme can be dropped when the Löb scheme is added.

Set $Y=\square X\to X$. The Löb axiom at $X$ is $\square Y\to \square X$. Therefore $Y$ and $\square Y$ together imply $X$, provingFor the converse, the tautology $X\to Y$ gives $\square X\to \square Y$ by necessitation and distribution. Consequently $\square Y\to X$ together with $\square X$ gives $X$, sowhose consequent is $Y$. Combining both directions gives an unboxed equivalence as a theorem of GL. Necessitation then yields exactly

Under the arithmetical interpretation $\square A=P_S(┌A┐)$, the Löb axiom says that a formal proof of the local reflection implication for $A$ already entails a formal proof of $A$:It is a formalized constraint on self-verification of a formal proof system. Externally, Löb's theorem says that if the system itself proves its own local reflection implication for $A$, it proves $A$. Distribution reflects closure of formal proofs under implication, necessitation reflects that a theorem has an arithmetically recognizable formal proof, and positive introspection reflects formal proof verification inside arithmetic.

Taking $A$ to be a refutable first-order sentence, especially a contradiction, recovers the obstruction behind the second incompleteness theorem: a first-order consistent sufficiently strong system cannot prove the corresponding claim that no formal proof of that first-order sentence exists. This does not identify provability with truth, nor grant the unrestricted factivity principle $\square A\to A$ as a theorem of the system. The Löb axiom is the characteristic additional scheme of Gödel–Löb provability logic.