Had this attempt to salvage naïve comprehension been studied before?

Question

Is the following a possible way to overcome inconsistency with naive comprehension:

We add an $\in_n$ symbol for each natural $n$ to the signature of this theory, which is a first order theory with equality and all its axioms.

Then axiomatize:

Comprehension: $\exists x \forall y \, (y \in_n x \leftrightarrow \phi^n(y))$

where $\phi^n(y)$ has $\in_{n-1}$ as the maximal appearing membership symbol.

Extensionality: $ a \in_n x \land \forall z \, (z \in_n x \leftrightarrow z \in_m y) \to x=y$

Membership: $a \in_m x \land b \in_n x \to b \in_m x $

had this been done before? References?

Answer 1

Here is a model of your theory. Start with a countably infinite set of objects $X=\bigsqcup_n X_n$, partitioned into infinitely many infinite sections. We inductively define $\in_n$. Consider the various formulas $\phi^n(y,z)$ that use only at most $\in_m$ for $m<n$, with parameters $z$. With the various possible parameters $z$, these define certain subsets of $X$, but only countably many. For each such definable subset, which has not already arisen earlier, assign an object $x$ from $X_n$ to represent it, and define $y\in_n x\iff\phi^n(y,z)$ for this instance. That is, I pick the object to represent the set for each definable set, not for each formula. If the definable set had already occurred at an earlier stage $m<n$, then I use the same object $x\in X_m$ as previously, and define $y\in_n x$ for the same members $y$. Thus, we will satisfy comprehension.

One effect of using the earlier object when the set was already defined earlier is that whenever $y\in_m x$ then $y\in_n x$ for all $n\geq m$, since the same formula recurs at the higher level the way I described it, or if you insist that the higher membership symbols appear in the formula we can add a vacuous use of $\in_{n-1}$ to any formula, such as $(y\in_{n-1} x\vee y\notin_{n-1} x)$, and thereby pump up the syntactic level of the formula to any desired level $n$. So the level of membership doesn't matter—once you are in the set, you will be in at all higher levels as well, and all members of a given set start membership at the same level. This will give us the membership axiom.

And since I was careful always to reuse the old object whenever the definable set is the same, we will get extensionality.

Note that we do indeed get new definable sets at each stage. For example, if we take $\phi(y)$ as $y\notin_{n} y$, then this cannot be already represented at level $n$ by any object, and so it will define a new class at level $n+1$. And then we will have all the finite modifications of it, definable with parameters, making infinitely many new definable sets at that next level. So every object will get used as a set at its level.

This method of argument is rather similar to some of the solutions of Frege's Basic Law V for first-order definability, as discussed in my paper

• Fregean abstraction in Zermelo-Fraenkel set theory: a deflationary account, Annals of Mathematics and Philosophy, 2023. (arxiv:2209.07845)

See the prior art section there, where I discuss this method, used in various work by Parsons, Bell, and Burgess. In particular:

• Terence Parsons. “On the consistency of the first-order portion of Frege’s logical system”. Notre Dame J. Formal Logic 28.1 (1987), pp. 161–168. ISSN: 0029-4527. DOI:10. 1305/ndjfl/1093636853.

One can perform the construction over any given model already. That is, we can assume $X$ already has some other first-order structure, but then chop it into the sections and undertake this construction on top of it, allowing formulas $\phi^n$ in the full language. This is essentially how the Parsons method works.