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, where $\varnothing \in x$ and $y \cup \{y\} \in x$ are expanded according to their usual definitions in set theory. What is the shortest 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, 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 \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 w \in y \land \forall z (z \in y \rightarrow \exists w (\forall t (t \in w \rightarrow t = z) \land w \in y)))) \end{align}