Shortest axiom of infinity for foundationless set theory

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

Axiom of extension: $$$$\forall x \forall y (\forall z (z \in x \leftrightarrow z \in y) \rightarrow x = y)$$$$

Axiom of heredity: $$$$\forall x (S x \leftrightarrow \forall y (y \in x \rightarrow S y))$$$$

Axiom schema of comprehension: $$$$\forall x (\phi x \rightarrow S x) \rightarrow \exists y \forall x (x \in y \leftrightarrow \phi x)$$$$ 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 $$$$\exists x (S x \land \varnothing \in x \land \forall y (y \in x \rightarrow y \cup \{y\} \in x))$$$$

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}

• the formula $\phi x$ must not contain $y$ free also. Mar 15, 2020 at 23:30
• I think the following is shorter: $\exists x (S x \land \exists k (k \in x) \land \\\forall y \forall z (y \in x \land \forall m (m \in z \to m = y) \to z \in x))$ Mar 17, 2020 at 18:56
• In your second predicate, the first $w$ is not quantified upon? I think you mean $x$ but you accidentally wrote $w$. Mar 17, 2020 at 19:37
• @ZuhairAl-Johar You’re right. Fixed. Mar 17, 2020 at 20:25
• @I think you need to remove $\forall x(S x$ and just put $\exists x$ before (or after) $\exists y$ Mar 18, 2020 at 8:58

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}

• @EmilJeřábek, thank you. (I was fighting non-existing logical dragons). Mar 22, 2020 at 21:24
• If $\ \emptyset\$ is legal then I can save 2 characters. Mar 24, 2020 at 7:04
• You mean in the external language? Mar 24, 2020 at 23:19
• Can't $\exists a$ be moved inside to capture just $a \in b$? Mar 24, 2020 at 23:20
• @user76284, u'r right, now the distance between the symbols to be associated is shorter (local formula understanding is easier than global). I don't see the edit yet, I hope that it will show up soon when admins have time to look at it. Mar 25, 2020 at 0:05

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.

• Does the weakened axiom of heredity allow us to prove $S \varnothing$? Mar 18, 2020 at 6:20
• Yes, simply let $\phi$ be any false formula, and the result is the empty set satisfying $S$.Notice that comprehension needs to stipulate that the asserted set satisfy $S$ Mar 18, 2020 at 7:10
• You mean comprehension needs the extra conjunct $\exists y \dots \land S y$? Mar 18, 2020 at 15:03
• @user76284, Exactly! Mar 18, 2020 at 15:05