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

A logical formula separates $A$ from $B$ in $S$ if it is provable at the standard numeral tuple of every member of $A$ and refutable at that of every member of $B$:There is no obligation on tuples outside the two sets. In a first-order consistent first-order theory these two obligations make $A$ and $B$ disjoint.

Let $h$ be the Gödel number of $H(v_1)$ and take the literal diagonal first-order sentence $R=H(\bar{h})$. If $S⊢R$, then $h$ belongs to the second source set, so separation gives $S⊢\neg H(\bar{h})$, a contradiction. If $S⊢\neg R$, then $h$ belongs to the first source set, so separation gives $S⊢H(\bar{h})$, again a contradiction. HenceThe direction of separation matters: here $H$ is provable on refutable diagonal codes and refutable on provable diagonal codes.

Write $H(\vec{v})$ for the proposed stage-comparison logical formula and fix a standard tuple $\vec{a}$. If $\vec{a}\in A$, numeralwise enumeration in arithmetic supplies a standard $m$ with $S⊢F(\overline{\stackrel{⃗}{a}},\bar{m})$. Disjointness gives $\vec{a}\notin B$, so $S⊢\neg G(\overline{\stackrel{⃗}{a}},\bar{j})$ for every standard $j$, in particular $j=0,\dots ,m$. The source's finite initial-segment axiom combines this finite list intoUse $\bar{m}$ as the existential witness to obtain $S⊢H(\overline{\stackrel{⃗}{a}})$.

If instead $\vec{a}\in B$, choose $n$ with $S⊢G(\overline{\stackrel{⃗}{a}},\bar{n})$. Disjointness gives refutations of $F(\overline{\stackrel{⃗}{a}},\bar{j})$ for all $j$, so the finitely many $j\le n$ giveFor an arbitrary $x$, the source's comparison axiom gives $x\le \bar{n}$ or $\bar{n}\le x$. In the first case the first conjunct of the proposed witness condition is false. In the second case $y=\bar{n}$ witnesses failure of its bounded universal conjunct, since $G(\overline{\stackrel{⃗}{a}},\bar{n})$ is provable. Generalization over $x$ therefore gives $S⊢\neg H(\overline{\stackrel{⃗}{a}})$.

Thus the logical formula separates $A$ from $B$. The formal proof uses the enumerators' numeralwise positive and negative formal proof properties and the two explicit order principles supplied in the source; it does not assume the first-order theory can decide arbitrary unbounded existential logical formulas.

A logical formula $D(\vec{x},y)$ weakly defines a total numerical function $f$ in $S$ if, for every standard input tuple $\vec{n}$ and $m=f(\vec{n})$,Strong definability of a numerical function additionally requires the internal uniqueness statementTogether with the positive instance, this is equivalent to proving $\forall y(D(\overline{\stackrel{⃗}{n}},y)\leftrightarrow y=\bar{m})$ for each standard input. The universal quantifier is the extra strength: it covers nonstandard potential outputs in first-order models of $S$. These are the weak and strong function conventions used here. ^[ref]

Suppose the graph of the total function is Sigma-1. Its complement is also Sigma-1, sinceReplace the graph assertion on the right by its Sigma-1 definition; existential quantifiers can be collected into one block. Bounded completeness of an arithmetic theory supplies numeralwise stage enumerators for each of these two disjoint complementary sets. Apply (b) to them. Its separating logical formula is provable exactly at the required graph tuples in the positive direction and refutable at all the other standard tuples, proving weak definability of a numerical function.

Using the graph logical formula alone would only supply positive instances from true existential witnesses; the separation construction is what supplies the negative-instance formal proofs without assuming Sigma-1 soundness or completeness for false Sigma-1 statements.

Let $d(n)$ be the Gödel number of the diagonal first-order sentence obtained by substituting $\bar{n}$ into the one-free-variable logical formula with code $n$, with an arbitrary default value on noncodes. By the assumptions and (c), this total function has a strong defining logical formula $D(x,y)$.

For the specified $F$, form the one-variable logical formulaLet $h$ be the Gödel number of $H$ and put $C=H(\bar{h})$. Then $d(h)=┌C┐$. Strong definability of a numerical function at this particular standard input givesSubstitution into the existential definition yieldsThe permitted equivalence between the source's two substitution notations identifies this with its requested fixed point. Bound variables are renamed when necessary before forming $H$, so the substitution is capture-free. This constructs one particular first-order sentence from the code of the logical formula which applies $F$ to its own diagonal output.