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

Axiom of extension:
\begin{equation}
    \forall x \forall y (\forall z (z \in x \leftrightarrow z \in y) \rightarrow x = y)
\end{equation}

Axiom of heredity:
\begin{equation}
    \forall x (S x \leftrightarrow \forall y (y \in x \rightarrow S y))
\end{equation}

Axiom schema of 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$.

---

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.