 of natural numbers. This, together with the axioms \(\forall x\,\neg(x^+=0)\) and \(\forall x\,\forall y(x^+=y^+\to x=y)\) characterizes the natural numbers with their successor operation up to isomorphism. In first order logic any theory which has a countably infinite model has also an uncountable model (by the Upward Löwenheim Skolem Theorem). Hence (\ref{ind}) cannot be expressed in first order logic. Another typical second-order expression is the Completeness Axiom of the linear order \(\le\) of the real numbers: 