All Questions

$\newcommand\ZFC{\mathrm{ZFC}}\DeclareMathOperator\Con{Con}$It is often interesting to look at the theory of all first-order statements that are true in some second-order theory, giving us things like ...

To second order logic, add a primitive partial one place function symbol "$\epsilon$" from unary predicate symbols [upper cases] to object symbols [lower cases]. Define: $ x=y \equiv_{df} \...