Least-occurrence order on cardinal properties (source code)

= Least-occurrence order on cardinal properties
{title2=$<_1$}

For cardinal properties $\Phi$ and $\Psi$ that occur, let $\iota_\Phi$ and $\iota_\Psi$ be their least witnesses. Define $\Phi<_1\Psi$ when
$$
\mathrm{ZFC}+\Phi\mathbf C+\Psi\mathbf C\vdash\iota_\Phi<\iota_\Psi.
$$
This relation need not be transitive, because the two implications can be proved under different joint existence assumptions.