Simplest axiom that entails the existence of an infinite set Let $\phi$ be a formula in first-order logic without equality and with the binary relation $\in$.
Let the size $s(\phi)$ of a formula $\phi$ be given by the following inductive definition on the grammar of well-formed formulas:
\begin{align}
s(\forall x \phi) &= 1 + s(\phi) \\
s(\exists x \phi) &= 1 + s(\phi) \\
s(\neg \phi) &= 1 + s(\phi) \\
s(\phi \land \psi) &= 1 + s(\phi) + s(\psi) \\
s(\phi \lor \psi) &= 1 + s(\phi) + s(\psi) \\
s(\phi \rightarrow \psi) &= 1 + s(\phi) + s(\psi) \\
s(x \in y) &= 1
\end{align}
What is the smallest $\phi$ such that $\text{ZF}-\text{Infinity}+\phi\vdash\text{Infinity}$ and is not known to be inconsistent?
Consider, for example,
$$\exists x (\exists y (y \in x) \land \forall y (y \in x \rightarrow \exists z (y \in z \land z \in x)))$$
The Logically Simplest Form of the Infinity Axiom by Parlamento and Policriti also addresses this question but defines "simplicity" in terms of quantifier alternations, whereas I'm interested in the size of the formula.
 A: 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.
