I've been somewhat interested in positive set theory recently, which solves Russell's paradox by changing the comprehension axiom schema to only allow positive formulas. I had the thought that an infinitary variation on this idea basically formalizes the set theory I'd always envisioned in my head, and I was curious if it'd ever been studied and what its properties would be.
There are several variations, but my basic idea is this: given some set $S$, a "true subset" of $S$ is some arbitrary infinitary combination of the elements of $S$. This can be expressed as an infinitary formula in something like $\mathcal L_{\infty,\infty}$ which is an infinitary OR of individual equality checks for whatever individual elements of $S$ are in the subset. We get something similar for a "true subclass" of the universe. This can be done as long as there is some way to unambiguously represent each element in the universe within the language of $\mathcal L_{\infty,\infty}$. Let's call these "positive infinitary formulas."
We would like to modify comprehension and/or replacement to only apply to these positive infinitary formulas. We really just want that, given some set $S$, that only those subsets which really do end up corresponding to some true combination of elements of $S$ are required to exist. Thus, since we have, for instance, that the formula ${x \not \in x}$ does not trace out any true combination of elements in the universe in this way, and as we do not stipulate that it does, the Russell set does not exist.
There are a bunch of nuances here which seem as though they could be dealt with in different ways to yield different positive infinitary set theories:
- $\text{GPK}_{\infty}^+$ is a positive set theory with a "positive comprehension" axiom schema, and we could replace it with an "infinitary positive comprehension" schema instead, with one instance for each infinitary positive formula.
- In first-order ZFC (perhaps without foundation) we could replace the comprehension and replacement schemas to have one instance for these positive infinitary formulas instead.
- We could use a different semantics for second-order ZFC-minus-foundation so that second-order quantification is interpreted as quantifying over these positive infinitary formulas or "true subclasses".
- We could go similarly back to a sort of "naive set theory" and replace the original unrestricted comprehension axiom with one quantifying on these positive infinitary formulas instead.
Or something else - I'm kind of handwaving here as I'm curious what other people have looked at or how this works.
Has this ever been studied?