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][1]'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. [1]: http://philsci-archive.pitt.edu/1372/1/SetClassCat.PDF