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

Write $\square A$ for the arithmetical sentence asserting $S$-provability of $A$. If $S⊢G$, the first derivability condition gives $S⊢\square G$. The stipulated fixed-point equivalence also gives $S⊢\neg \square G$. This contradicts consistency. Conversely an inconsistent classical theory proves every sentence, including $G$. ThusOnly the direction from an actual proof to its formalized provability is used here. There is no inference from a theorem $\square G$ to a theorem $G$, and no assumption that every theorem of $S$ is true.

The Hilbert-Bernays-Löb derivability conditions are: if $S⊢A$ then $S⊢\square A$; $S⊢\square (A\to B)\to (\square A\to \square B)$; and $S⊢\square A\to \square \square A$. The first is an external rule about provability; the latter two are internal theorems. Standard numerical correctness and the stipulated ${\Sigma }_1$ form accompany the predicate in this question. These conditions do not include reflection $\square A\to A$.

Choose a fixed refutable sentence $\perp$ and identify ${\mathrm{Con}}_S$ with $\neg \square \perp$. Different fixed refutable choices have provably equivalent consistency sentences, because $S$ proves their equivalence to a contradiction. From $\perp \to G$, necessitation and distribution give $\square \perp \to \square G$. Since $G\to \neg \square G$, this yields $G\to {\mathrm{Con}}_S$.

For the converse, necessitate $G\to \neg \square G$ and distribute to get $\square G\to \square \neg \square G$. Positive introspection also gives $\square G\to \square \square G$. The two boxed contradictories imply $\square \perp$ by formalized propositional reasoning. Thus $\square G\to \square \perp$, and contraposition gives ${\mathrm{Con}}_S\to \neg \square G\to G$. ConsequentlyFinally the deduction theorem says that $S+G$ is inconsistent exactly when $S⊢\neg G$. The internal equivalence identifies $S+G$ and $S+{\mathrm{Con}}_S$ in their deductive consequences. Hence $S⊬\neg G$ exactly when $S+{\mathrm{Con}}_S$ is consistent. Consistency of $S$ alone need not ensure this stronger consistency condition.

For consistency of a negated-consistency extension, put $A=S+\neg {\mathrm{Con}}_S$. The arithmetized deduction theorem, together with double-negation elimination and formalized proof transformations, givesFrom the preceding proof, $S⊢{\square }_{S}G\to {\square }_S\perp$. Necessitating the equivalence between $G$ and ${\mathrm{Con}}_S$ and using distribution therefore gives $S⊢{\square }_S{\mathrm{Con}}_S\to {\square }_S\perp$. Its contrapositive isThis is an internal conditional statement. It does not assert that $S$ proves its own consistency or permits the consistency premise to be discarded.

For unrestricted consistency self-strengthening is inconsistent, again take $A=S+\neg {\mathrm{Con}}_S$. In $S^{++}$ the axiom ${\mathrm{Con}}_S$ and the preceding implication prove ${\mathrm{Con}}_A$. The additional rule then proves ${\mathrm{Con}}_{A+{\mathrm{Con}}_A}$.

However consistency of an extension implies consistency of its subtheory by the formalized inclusion of proofs: $S⊢{\mathrm{Con}}_A\to {\mathrm{Con}}_S$. Thus the ordinary theory $A+{\mathrm{Con}}_A$ contains $\neg {\mathrm{Con}}_S$ and derives ${\mathrm{Con}}_S$, so it has a finite contradiction proof. Checking that concrete proof in arithmetic gives $S⊢\neg {\mathrm{Con}}_{A+{\mathrm{Con}}_A}$. This theorem is also present in $S^{++}$, contradicting the result of the new rule. Therefore $S^{++}$ is inconsistent.

The error in the added rule is its unrestricted internal use on arbitrary arithmetically presented systems, including systems containing false consistency assertions. A true external consistency progression for a specified sound system is not this unrestricted inference rule.

For separation of number sets in an arithmetic theory, a formula separates $A$ from $B$ in $S$ if $n\in A$ implies $S⊢F(\overline{n})$, and $n\in B$ implies $S⊢\neg F(\overline{n})$. No demand is made for numbers outside their union. Consistency forces disjointness when such a separator exists.

Let $r$ be the code of the fixed-point sentence. If $S⊢R$, then $r$ is in the provable set, so separation gives $S⊢H(\overline{r})$. The fixed-point equivalence gives its negation, a contradiction. If $S⊢\neg R$, then $r$ is in the refutable set, so separation gives $S⊢\neg H(\overline{r})$, and the fixed-point equivalence gives $S⊢R$, again a contradiction. ThusThe argument is syntactic: it needs only the separating implications and consistency, not omega-consistency or general soundness.

For Rosser separation by a bounded stage comparison, use the numeralwise enumeration in arithmetic properties meant by enumeration in $S$: membership supplies some standard stage with a provable positive instance, while nonmembership makes every standard-stage instance refutable. These are stronger than merely attaching a ${\Sigma }_1$ syntactic label to an arbitrary formula. The finite-initial-segment axiom lets us combine finitely many numeralwise refutations into a bounded universal assertion.

If $n$ is provable, choose a standard stage $p$ with $S⊢P(\overline{n},\overline{p})$. Consistency means $n$ is not refutable. Therefore $S⊢\neg R(\overline{n},\overline{j})$ for each $j\le p$. Using the displayed finite-segment axiom and equality substitution, combine these proofs to get $S⊢\forall z\le \overline{p}\neg R(\overline{n},z)$. Existential introduction with stage $p$ proves the separator at $n$.

If $n$ is refutable, choose a standard stage $q$ with $S⊢R(\overline{n},\overline{q})$. Consistency implies that $n$ is not provable, so all standard instances of $P(\overline{n},\cdot )$ are refutable. In particular their finitely many instances through $q$ give $S⊢\forall z\le \overline{q}\neg P(\overline{n},z)$. For an arbitrary proposed witness $z$, the total-comparison axiom gives $z\le \overline{q}$ or $\overline{q}\le z$. In the first case its $P$ conjunct fails; in the second case the known $R$ instance at $q$ contradicts its bounded no-refutation conjunct. Generalize on $z$ to refute the existential separator. Hence the proposed first-proof-before-refutation formula separates the two sets.

The literal semantic hypothesis is insufficient: a semantic Gödel fixed point need not be canonical. A sentence can be false and provable in a consistent, unsound arithmetic theory, in which case both sides of the stipulated semantic biconditional can be false.

For a concrete counterexample, assume PA is consistent and set $S=\mathrm{PA}+\neg {\mathrm{Con}}_{\mathrm{PA}}$. Gödel's second incompleteness theorem makes this extension consistent: otherwise PA would prove its own consistency. It is still bounded-complete. Use ordinary numeralwise proof and refutation enumerators for this recursively axiomatized theory, and take $G=\neg {\mathrm{Con}}_{\mathrm{PA}}$. This $G$ is false in the standard natural numbers but is an axiom of $S$. Since it is provable, $\exists yP(┌G┐,y)$ is true; its negation is false. Thus the semantic fixed-point biconditional required in this part is true, with both sides false.

Choose $R$ by the usual canonical Rosser construction for these proof matrices. Its undecidability follows from the preceding parts, and it is a true ${\Pi }_1$ sentence: if it were false, its true ${\Sigma }_1$ negation would be provable in this bounded-complete theory, contradicting undecidability. Hence $G$ is false and $R$ true, so their proposed semantic equivalence is false. This counterexample meets the literal assumptions and does not exploit a missing source page.

Under the intended canonical ${\Pi }_1$ Gödel/Rosser convention, the expected answer does hold. Consistency plus bounded completeness implies ${\Pi }_1$ soundness: a false ${\Pi }_1$ theorem has a standard bounded counterexample whose negation the theory proves. If canonical $G$ were false, its truth fixed point would make it provable, contradicting this soundness; thus $G$ is true. Canonical $R$ is true by the preceding ${\Sigma }_1$-negation argument, so both canonical sentences are true and their equivalence is true. This last conclusion needs that canonical construction or an equivalent additional restriction; truth of a biconditional alone does not supply it.

Use the two formal consistency equivalences expressly supplied for this part. If $S⊢G\leftrightarrow R$, the derivability conditions give $S⊢\square \neg G\leftrightarrow \square \neg R$. Taking negations and applying those supplied equivalences yieldsOne-consistency implies ${\Sigma }_1$ soundness under bounded completeness. Hence $S+{\mathrm{Con}}_S$ is consistent: if not, $S$ would prove $\neg {\mathrm{Con}}_S$, a false ${\Sigma }_1$ sentence. But in that consistent extension the last equivalence and its consistency axiom prove its own consistency ${\mathrm{Con}}_{S+{\mathrm{Con}}_S}$. Gödel's second incompleteness theorem rules this out. ThereforeThis establishes the requested unprovability using the explicit formal hypotheses, without inferring internal provability from the semantic equivalence discussed in the preceding part. The hypotheses for the second theorem are the standard effective arithmetic presentation and adequate provability predicates stipulated here.

Gödel's second incompleteness theorem says that a consistent effectively presented arithmetic theory with an adequate proof predicate cannot prove its formal consistency statement. The background strength must support the diagonal lemma and the derivability conditions, as in the present arithmetic setting.

Löb's theorem saysIt is a theorem about derivability for every sentence $A$, not merely an external soundness assertion about the interpretation of $\square$. Taking $A=\perp$, a proof of consistency gives $S⊢\square \perp \to \perp$; Löb then gives $S⊢\perp$. Thus a consistent $S$ cannot prove consistency. This is how the second incompleteness theorem is the contradiction-sentence instance of Löb's more general result.

Suppose $S+A$ proves every specified reflection instance. Use only the instance with $X=\neg A$. The deduction theorem givesClassical propositional reasoning turns this into $S⊢\square \neg A\to \neg A$: if $\neg A$ already holds the implication is true, while otherwise $A$ holds and the displayed theorem supplies it. Löb's theorem now yields $S⊢\neg A$, making $S+A$ inconsistent. Therefore no sentence consistent with $S$ can supply all the local reflection instances in a one-sentence extension. The proof uses just one well-chosen instance, and never applies necessitation to a derivation with the extra assumption still open.

GL has all classical propositional tautologies, the normal distribution axiom $\square (A\to B)\to (\square A\to \square B)$ and the Löb axiom $\square (\square A\to A)\to \square A$, closed under uniform substitution, modus ponens and necessitation of theorems. We use its derived positive-introspection theorem $\square A\to \square \square A$, normal boxed reasoning, and the boxed replacement principle supplied in the question.

For completeness, positive introspection follows from these axioms. Put $C=A\wedge \square A$. Distribution gives $\square C\to \square A$, so propositional logic proves $A\to (\square C\to C)$. Necessitate and distribute to get $\square A\to \square (\square C\to C)$; Löb's axiom gives $\square A\to \square C$, and boxing $C\to \square A$ finishes $\square A\to \square \square A$.

For a GL fixed point by truth substitution, set $\top =(\perp \to \perp )$, $U=\square Y(\top )$ and $V=\square Y(U)$. From the tautology $U\to (\top \leftrightarrow U)$, boxed reasoning gives $\square U\to \square (\top \leftrightarrow U)$. The supplied replacement principle and distribution then giveSince $U$ is itself boxed, positive introspection gives $U\to \square U$, and hence $U\to V$.

For the reverse direction, the displayed implication entails the theorem $V\to (\square U\to U)$. Necessitate it and distribute to obtain $\square V\to \square (\square U\to U)$. Since $V$ is boxed, $V\to \square V$ holds. The Löb axiom therefore yields $V\to \square U$, and the same displayed implication then yields $V\to U$. ConsequentlyAll occurrences of the unknown letter have been removed from $U$ by substitution of truth; any other parameter letters remain available. The proof does not assume the invalid reflection principle $\square U\to U$ as an unconditional axiom.

The fixed point of boxed negated provability gives, in fact, that GL proves $F\leftrightarrow \square \perp$. Here is a direct derivation. Since $F$ is provably equivalent to a boxed formula, positive introspection and necessitation of that equivalence give $F\to \square F$. Another introspection step gives $F\to \square \square F$. The stipulated fixed point also gives $F\to \square \neg \square F$. Combining these two boxed contradictories yields $F\to \square \perp$. Conversely $\square \perp \to \square \neg \square F$ follows by normal boxed explosion, and the fixed point then yields $\square \perp \to F$.

Arithmetical soundness of GL, proved by translating distribution into the second derivability condition, necessitation into the first, and Löb's axiom into its internal arithmetic theorem, now givesAny remaining propositional parameters may be assigned arbitrary arithmetic sentences; this equivalence is uniform in those assignments. If PA is one-consistent, it is consistent and ${\Sigma }_1$ sound. Its standard provability predicate for a contradiction is then a false ${\Sigma }_1$ sentence and cannot be a theorem. Hence $F^{\ast }$ is not provable in PA. Moreover its negation is equivalent to PA's consistency statement and is unprovable by the second incompleteness theorem. Thus this fixed point is, under the stated hypothesis, undecidable rather than an unboxed reflection principle.