 The axioms of second-order logic are trivially true in a (full) model with just one element. This raises the question how to guarantee that there are more than one element in the domain. Of course, we can add, for every n, an axiom which says that there are more than n elements. There are various ways to say in second-order logic with one axiom that there are infinitely many individuals. These are equivalent in full models but may be non-equivalent in Henkin models. Some are equivalent if the Axiom of Choice is assumed. Let us call a second-order sentence \(\phi\) of the empty vocabulary an Axiom of Infinity if 