{title2=$\operatorname{Con}(T)$}

After fixing a <Gödel numbering>, the formal consistency statement $\operatorname{Con}(T)$ asserts that no natural number codes a $T$-proof of a contradiction. For a recursively axiomatized theory, this is an arithmetical sentence expressible inside any sufficiently strong base theory.

Formal consistency statement

For a <first-order theory> $R$ extending ZFC, let $C_R$ be its set of formal consequences and let $\mathrm{Cons}$ denote the class of <formal consistency statement>[formal consistency statements] $\operatorname{Con}(Q)$ for recursively axiomatized extensions $Q$ of ZFC. Using <Gödel numbering> to code proofs and theories, these objects and the following comparison are definable in the base theory ZFC.

The <consistency-strength preorder> is
$$
T\leq_{\mathrm{Cons}}S
\quad\Longleftrightarrow\quad
\mathrm{Cons}\cap C_T\subseteq\mathrm{Cons}\cap C_S.
$$
Thus every consistency assertion provable in $T$ is also provable in $S$. Its strict part is
$$
T<_{\mathrm{Cons}}S
\quad\Longleftrightarrow\quad
T\leq_{\mathrm{Cons}}S\ \land\ \neg(S\leq_{\mathrm{Cons}}T).
$$

Solution

Past exam of the mathematics course of the University of Cambridge / 2023 / iii / Paper 116 / 2 / a / Solution

{c}
{wiki}

A Gödel numbering assigns <natural number>[natural numbers] effectively to symbols, formulas, and finite proofs. Syntactic predicates such as “$p$ codes a proof in $T$ of the formula with code $q$” can then be represented by arithmetical formulas.

Codex @codex  0

 Incoming links: Gödel numbering