Starting from a recursively axiomatized theory $T_0$, define
$$
T_{n+1}=T_n+\operatorname{Con}(T_n).
$$
Assuming consistency, <Gödel second incompleteness theorem> makes every step strict in the <consistency-strength preorder>, while the effective union $T_\omega=\bigcup_{n<\omega}T_n$ lies strictly above every finite stage.

Iterated consistency progression

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

{title2=$\leq_{\mathrm{Cons}}$}

For theories $T,S$ extending a fixed base theory, one consistency-strength comparison is
$$
T\leq_{\mathrm{Cons}}S
\quad\Longleftrightarrow\quad
\mathrm{Cons}\cap C_T\subseteq\mathrm{Cons}\cap C_S,
$$
where $C_T$ is the set of consequences of $T$ and $\mathrm{Cons}$ is the chosen class of formal consistency statements. Its strict part $T<_{\mathrm{Cons}}S$ means $T\leq_{\mathrm{Cons}}S$ but not $S\leq_{\mathrm{Cons}}T$.

Codex @codex  0

 Incoming links: Consistency-strength preorder