Let $T$ be the theory with a binary symbol $\in$, an unary symbol $S$, and the following axioms:


[Axiom of extension](https://en.wikipedia.org/wiki/Axiom_of_extensionality):
\begin{equation}
 \forall x \forall y (\forall z (z \in x \leftrightarrow z \in y) \rightarrow x = y)
\end{equation}


[Axiom of heredity](https://en.wikipedia.org/wiki/Ackermann_set_theory#The_axioms):
\begin{equation}
 \forall x (S x \leftrightarrow \forall y (y \in x \rightarrow S y))
\end{equation}


[Axiom schema of comprehension](https://en.wikipedia.org/wiki/Axiom_schema_of_specification#Unrestricted_comprehension):
\begin{equation}
 \forall x (\phi x \rightarrow S x) \rightarrow \exists y \forall x (x \in y \leftrightarrow \phi x)
\end{equation}
for every formula $\phi$ not containing $S$.


This entails the existence of the [empty set](https://en.wikipedia.org/wiki/Axiom_of_empty_set) (as well as any [hereditarily finite set](https://en.wikipedia.org/wiki/Hereditarily_finite_set)) and, over sets that satisfy $S$, [powerset](https://en.wikipedia.org/wiki/Axiom_of_power_set), [union](https://en.wikipedia.org/wiki/Axiom_of_union), [pairing](https://en.wikipedia.org/wiki/Axiom_of_pairing), and [specification](https://en.wikipedia.org/wiki/Axiom_schema_of_specification).




---


Let $I$ be the formula
\begin{equation}
 \exists x (S x \land \varnothing \in x \land \forall y (y \in x \rightarrow y \cup \{y\} \in x))
\end{equation}


asserting the existence of an [inductive set](https://en.wikipedia.org/wiki/Axiom_of_infinity#Formal_statement), where $\varnothing \in x$ and $y \cup \{y\} \in x$ are expanded according to their usual definitions in set theory. What is the [shortest](https://math.stackexchange.com/questions/3207352/simplest-axiom-that-entails-the-existence-of-an-infinite-set) formula $\psi$ such that $T, \psi \vdash I$ and $T, \psi \nvdash \bot$? How strong is the resulting theory $T, \psi$? Since $T$ lacks [foundation](https://en.wikipedia.org/wiki/Axiom_of_regularity), such a $\psi$ must deal with the possibility of non-well-founded sets.


Some possible candidates, starting with $I$ itself:


\begin{align}
\psi\_1 &= \exists x (S x \land \varnothing \in x \land \forall y (y \in x \rightarrow y \cup \{y\} \in x))
\\
&= \tiny{\exists x (S x \land \exists y (y \in x \land \neg \exists z (z \in y)) \land \forall y (y \in x \rightarrow \exists z (z \in x \land \forall w (w = y \lor w \in y \leftrightarrow w \in z))))}
\\
\psi\_2 &= \forall x (S x \rightarrow \exists y (S y \land x \in y \land \forall z (z \in y \rightarrow \{z\} \in y)))
\\
&= \tiny{\forall x (S x \rightarrow \exists y (S y \land x \in y \land \forall z (z \in y \rightarrow \exists w (\forall t (t \in w \leftrightarrow t = z) \land w \in y))))}
\end{align}



Shortest axiom of infinity for foundationless set theory
**REMARK**  I hope that *negation* is legal. Perhaps some $Sx$ statements can be harmlessly removed. Feel free to polish the statement below (I am not a logician).


**STATEMENT**


Set $b$ stands for *big* (infinite). Also, set $y$ strictly contains set $x$.


\begin{align}
\psi
&= \exists b (S b \land \exists a (a\in b) \land \forall x (x \in b \rightarrow \exists y (x \subsetneq y \in b)))
\\
&= \tiny{\exists b\,(Sb\land \exists a (a\in b) \land \forall x\,(x\in b\to
 \exists y\,(y\in b\land\forall z\,(z\in x\to z\in y)\land \neg (x = y))))}
\end{align}


