Arithmetization, Incompleteness, and Relative Consistency: Examples and Counterexamples

The syntactic diagonal lemma: For every formula $\psi (v)$ with no other free variables in an effective signature extending arithmetic, there is a sentence $\theta$ such that Q in that signature proves $\theta \leftrightarrow \psi (<mi\; mathvariant="normal">⌜</mi>\theta <mi\; mathvariant="normal">⌝</mi>)$. The construction is effective and requires neither consistency nor soundness.

Deduction theorem for sentence assumptions: In ZF, for a sentence theory $T$, a sentence $\sigma$ and any formula $\theta$,

$T\cup \{\sigma \}⊢\theta ⟺T⊢\sigma \to \theta \mathrm{.}$

The forward transformation also works for an open discharged assumption $\sigma$ provided every variable generalized or existentially eliminated in the given derivation is absent from $\mathrm{FV}(\sigma )$; the other assumptions remain sentences.

Second incompleteness for standard provability: If T is consistent and has the arithmetic/interpretation and D1–D3 hypotheses above for the displayed standard predicate, T does not prove its displayed $\mathrm{Con}(T)$. Numeralwise correctness of an arbitrary predicate is insufficient.

Models and consistency for countable theories: In external ZF, an explicitly countable sentence theory is consistent iff it has a nonempty set model, and iff it has a model with carrier injecting into $\omega$. For an effective presentation, external consistency agrees with the truth of its certified Con formula in standard arithmetic. No transitivity or external well-foundedness of a model follows.

Robinson arithmetic, PA, and numeral conventions: Use the arithmetic signature $0,S,+,\cdot ,=$. Robinson arithmetic $Q$ consists of the universal closures of these seven formulas:

$Sx\mathrm{\ne }0;Sx=Sy\to x=y;x\mathrm{\ne }0\to \mathrm{\exists }yx=Sy;$ $x+0=x;x+Sy=S(x+y);x\cdot 0=0;x\cdot Sy=x\cdot y+x\mathrm{.}$

PA adds, for every formula $\varphi (x,\bar{z})$, the universal closure of $[\varphi (0,\bar{z})\wedge \mathrm{\forall }x(\varphi (x,\bar{z})\to \varphi (Sx,\bar{z}))]\to \mathrm{\forall }x\varphi (x,\bar{z})$. Parameters $\bar{z}$ are allowed. No induction schema is included in $Q$.

For an external natural number $n$, its numeral is the term $\bar{n}=S^{n}0$. Define $x\le y$ by $\mathrm{\exists }z(z+x=y)$ and $x<y$ by $x\le y\wedge x\mathrm{\ne }y$, with $z$ fresh. The left-addend witness is intentional: commutativity is not an axiom of Q.

Use def-set-coded-formal-derivation for the six logical schemes and three rules. Negation, conjunction and existential quantification are primitive: $A\to B$ expands to $\mathrm{\neg }(A\wedge \mathrm{\neg }B)$, $A\vee B$ to $\mathrm{\neg }(\mathrm{\neg }A\wedge \mathrm{\neg }B)$, and $\mathrm{\forall }xA$ to $\mathrm{\neg }\mathrm{\exists }x\mathrm{\neg }A$. Inequality means negated equality. Substitute capture-free, always taking the least available fresh variable index and universally closing the remaining parameters in increasing index order. Thus each displayed axiom and each induction instance is a definite finite sentence.

Explicit definitions are conservative: Adding relation symbols by old-language defining formulas and function symbols by old-language graphs that T proves uniquely total gives a conservative extension of T. The extension is equiconsistent with T. This includes any set of such definitions, since a proof uses only finitely many.

Robinson arithmetic, PA, and numeral conventions: Use the arithmetic signature $0,S,+,\cdot ,=$. Robinson arithmetic $Q$ consists of the universal closures of these seven formulas:

$Sx\mathrm{\ne }0;Sx=Sy\to x=y;x\mathrm{\ne }0\to \mathrm{\exists }yx=Sy;$ $x+0=x;x+Sy=S(x+y);x\cdot 0=0;x\cdot Sy=x\cdot y+x\mathrm{.}$

PA adds, for every formula $\varphi (x,\bar{z})$, the universal closure of $[\varphi (0,\bar{z})\wedge \mathrm{\forall }x(\varphi (x,\bar{z})\to \varphi (Sx,\bar{z}))]\to \mathrm{\forall }x\varphi (x,\bar{z})$. Parameters $\bar{z}$ are allowed. No induction schema is included in $Q$.

For an external natural number $n$, its numeral is the term $\bar{n}=S^{n}0$. Define $x\le y$ by $\mathrm{\exists }z(z+x=y)$ and $x<y$ by $x\le y\wedge x\mathrm{\ne }y$, with $z$ fresh. The left-addend witness is intentional: commutativity is not an axiom of Q.

Use def-set-coded-formal-derivation for the six logical schemes and three rules. Negation, conjunction and existential quantification are primitive: $A\to B$ expands to $\mathrm{\neg }(A\wedge \mathrm{\neg }B)$, $A\vee B$ to $\mathrm{\neg }(\mathrm{\neg }A\wedge \mathrm{\neg }B)$, and $\mathrm{\forall }xA$ to $\mathrm{\neg }\mathrm{\exists }x\mathrm{\neg }A$. Inequality means negated equality. Substitute capture-free, always taking the least available fresh variable index and universally closing the remaining parameters in increasing index order. Thus each displayed axiom and each induction instance is a definite finite sentence.

The transitive-model consistency-strength gap: Let $S=\mathrm{Z}\mathrm{F}\mathrm{C}+\mathrm{Con}(\mathrm{Z}\mathrm{F}\mathrm{C})$. Assuming externally Con(S), ZFC does not prove $\mathrm{Con}(\mathrm{Z}\mathrm{F}\mathrm{C})\to \mathrm{TM}(\mathrm{Z}\mathrm{F}\mathrm{C})$. Moreover $S+\mathrm{\neg }\mathrm{TM}(\mathrm{Z}\mathrm{F}\mathrm{C})$ is consistent and has a set model. The stronger external premise Con(S) is retained.

Finite-fragment model transfer proves relative consistency: Let T extend enough ZF to formalize set-model soundness, and let U be an explicitly countable sentence theory. Suppose that for each external finite $\mathrm{\Delta }\subseteq U$ there are a finite $\mathrm{\Gamma }$ and T proofs of existence of a suitable TM/CTM of $\mathrm{\Gamma }$ and of its conversion into a set model of $\mathrm{\Delta }$. Then external Con(T) implies Con(U). This is a metatheorem with fixed finite proof inputs, not a uniform internal all-fragment assertion.

Formal consistency transfer from a verified reduction: If an arithmetic base B verifies a total code map r and $\mathrm{\forall }p({\mathrm{Prf}}_U(p,<mi\; mathvariant="normal">⌜</mi>\mathrm{\perp }<mi\; mathvariant="normal">⌝</mi>)\to {\mathrm{Prf}}_T(r(p),<mi\; mathvariant="normal">⌜</mi>\mathrm{\perp }<mi\; mathvariant="normal">⌝</mi>))$, then $B⊢\mathrm{Con}(T)\to \mathrm{Con}(U)$. For reflection/finite-fragment applications the support extractor, fragment maps and reflection/transfer/soundness proof constructors must actually be supplied and verified to obtain such an r.