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

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.