Consistency-strength preorder (source code)

= Consistency-strength preorder
{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$.