Simplest axiom that entails the existence of an infinite set

Solution 1:

Reminds me of code-golf. Here is a nice one (length $8$):

$∃S\ ∀x\ ∃y\ ( y∈S ∧ ( x∈S ⇒ x∈y ) )$.

Let $I$ be such that $∀x\ ∃y\ ( y∈I ∧ ( x∈I ⇒ x∈y ) )$. Then (applying to $x:=I$) we get $∃y\ ( y∈I )$. Let $c_0∈I$. Then $∃y\ ( y∈I ∧ c_0∈y )$. Let $c_1∈I$ such that $c_0∈c_1$. Continuing in the same way we get $c_0∈c_1∈c_2∈\cdots$, all of which are members of $I$. By Foundation we can prove that any given two of them are distinct. But of course we want actual infinity, not the meta-observation that $I$ is infinite. We can first prove the generalization $∀x∈I\ ∃y∈I\ ( x∈y )$. After that it is easy if we have Choice or Collection. In particular, by AC we can let $f : I→I$ such that $x∈f(x)$ for every $x∈I$, and then let $N$ be the intersection of all subsets of $I$ that include $c_0$ and are closed under $f$, yielding something like Zermelo's original version.

It turns out that we can in fact proceed in ZF alone (without Choice). See this post for the key idea. We basically define in ZF minus Infinity the rank of every set $S$ (by applying Foundation to the set of unranked sets in the transitive closure of $S$). Then construct the set $R$ of all ranks of members of $I$. Now observe that every $k∈R$ is the rank of some $x∈I$, and $x∈y$ for some $y∈I$, and $y$ has a higher rank than $x$, so the transitive closure of $R$ is closed under successor. Therefore we recover the standard Infinity axiom.