= Solution
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).
$$
Back to article page
