Shortest axiom of infinity for foundationless set theory

Question

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$.

This entails the existence of the empty set (as well as any hereditarily finite set) and, over sets that satisfy $S$, powerset, union, pairing, and 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, 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 \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}

Answer 1

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}

Answer 2

Possibly something like Separation by $\neg S$: $$\forall a \exists x \forall y (y \in x \leftrightarrow y \in a \land \neg Sy)$$ The idea is that if we define natural as: well founded transitive set of transitive sets, that when nonempty then it must have a predecessor, and such that every nonempty element of it must have a predecessor, then this separation would prevent having a natural that fulfills $\neg S$. Otherwise any such a natural $n$ would have a nonempty subset of it that is the set of all of its elements that fulfill $\neg S$, but that set wont have a minimal! Thus $n$ won't be well founded, which contradicts $n$ being a natural. So this theory would prove that any natural fulfills $S$, therefore by set construction proving the existence of a set of all naturals, which is an inductive set!.

However, I do suspect some kind of inconsistency lurking here or there?!

Regarding the consistency issue, I'd say that if the axiom of Heredity is weakened to two axioms:

Axiom of Heredity: $$\forall x (Sx \to \forall y \in x (Sy))$$

Axiom of Subsets: $$\forall x \forall y (Sx \land y \subset x \to Sy)$$

And if we weaken the Axiom of comprehension as to additionally require all parameters of $\phi$ to satisfy $S$, and stipulate the asserted set to satisfy $S$.

Then the resulting theory plus Separation by $\neg S$ is a proper fragment of Muller's class theory! And so it's consistent relative to Muller's class theory.

So the question of consistency of addition of Separation by $\neg S$ to the axioms stated by the $OP$ is mostly related to the upward heredity statement $$ \forall x (\forall y \in x (Sy) \to S(x))$$, and to unleashing parameters in comprehension. Those need to be checked.

[Addendum]: The addition of separation by $\neg S$ to the axioms of the theory presented here is INCONSISTENT:

Proof: define von Neumann ordinal as a transitive set of transitive sets, that has every nonempty subset of it having a minimal element with respect to relation $\in$, that is:

$$\text{ von Neumann ordinal}(x) \iff \\ transitive(x) \land \forall y \in x (transitive(y)) \land \\\forall z \subseteq x (z \neq \emptyset \to \exists m \in z \forall n \in z (n \not \in m))$$

Now clearly from Separation by $\neg S$ we'll easily prove (from Heredity) that every von Neumann ordinal satisfy $S$! Thus having a set of all of them (comprehension), enacting Burali-Forti.

However the result doesn't affect the suggested weaker fragment of Muller's set theory that I've exposited here. But the answer to the shortest axiom that would imply infinity when added to the axioms of the theory presented here is still an open question.