Positive set theory, antifoundation, and the "co-Russell set"

Question

A more focused version of this question has now been asked at MO.

Tl;dr version: are there "reasonable" theories which prove/disprove "the set of all sets containing themselves, contains itself"?

---

Inspired by this question, I'd like to ask a question which has been vaguely on my mind for a while but which I've never looked into.

Working naively for a moment, let $S=\{x: x\in x\}$ be the "dual" to Russell's paradoxical set $R$. There does not seem to be an immediate argument showing that $S$ is or is not an element of itself, nicely paralleling the fact that there are of course arguments for $R$ both containing and not containing itself (that's exactly what the paradox is, of course).

However, it's a bit premature to leap to the conclusion that there actually are no such arguments. Namely, if we look at the Godel situation, we see something quite different: while the Godel sentence "I am unprovable (in $T$)" is neither provable nor disprovable (in $T$), the sentence "I am provable (in $T$)" is provable (in $T$) (as long as we express "is provable" in a reasonable way)! So a certain intuitive symmetry is broken. So this raises the possibility that the question

$$\mbox{Does $S$ contain itself?}$$

could actually be answered, at least from "reasonable" axioms.

Now ZFC does answer it, albeit in a trivial way: in ZFC we have $S=\emptyset$. So ideally we're looking for a set theory which allows sets containing themselves, so that $S$ is nontrivial. Also, to keep the parallel with Russell's paradox, a set theory more closely resembling naive comprehension is a reasonable thing to desire.

All of this suggests looking at some positive set theory - which proves that $S$ exists, since "$x\in x$" is a positive formula, but is not susceptible to Russell's paradox since "$x\not\in x$" is not a positive formula - possibly augmented by some kind of antifoundation axiom.

To be specific:

Is there a "natural" positive set theory (e.g. $GPK_\infty^+$), or extension of such by a "natural" antifoundation axiom (e.g. Boffa's), which decides whether $S\in S$?

In general, I'm interested in the status of "$S\in S$" in positive set theories. I'm especially excited by those which prove $S\in S$; note that these would have to prove the existence of sets containing themselves, since otherwise $S=\emptyset\not\in S$.

Answer 1

I found a paper of Cantini's that contains an argument that can be used to establish that $S \in S$ under fairly weak assumptions (on both the amount of comprehension and the underlying logic). Ultimately the proof is a fixed-point argument in the vein of Löb's theorem. This argument is strong enough to establish that $S \in S$ in $\mathsf{GPK}$. While Cantini is concerned with a contractionless logic, I would like to avoid writing out sequent calculus in this answer, so I will state and prove a weaker result in classical first-order logic.

EDIT: I recently found out that adding an abstraction operator (i.e., set builder notation) is far less innocuous than I had realized. (This is discussed by Forti and Hinnion in the introduction of this paper. My understanding of the issue is that it allows you to code negation with equality.) I suspect that the old version of my answer was only vacuously correct in that the resulting theory is inconsistnt, so I have fixed it, although I have specialized the argument to the particular case at hand. I've also cleaned up the argument a bit, mostly to make sure I actually understood it.

We need to assume that our theory $T$ has enough machinery for the following:

• $T$ entails extensionality.
• There is definable pairing function $(x,y) \mapsto \langle x,y\rangle$.
• For any $a$ and $f$, there is a set $f[a]$ such that $x \in f[a]$ if and only if $\langle a,x\rangle \in f$. Note that $(f,a) \mapsto f[a]$ is a definable function by extensionality.
• There is a set $D$ such that every element of $D$ is an ordered pair $\langle x,y\rangle$ and $\langle x,y\rangle \in D$ if and only if either $y \in y$ or $y = x[x]$.

(It is easy to check that $\mathsf{GPK}$ satisfies all of these.)

Now let $I = D[D]$. Unpacking, we have that $x \in I$ if and only if $\langle D,x\rangle \in D$ if and only if either $x \in x$ or $x = D[D] = I$. Therefore $I$ contains precisely the elements of the co-Russell class $S$ and $I$ itself, but since $I \in I$, $I \in S$ and so $I = S$, whence $S \in S$.

(Incidentally, a similar argument also resolves a question in my earlier answer to your related question. In particular, $\mathsf{GPK}$ does entail the existence of a Quine atom by the above argument if we just say that $\langle x,y\rangle \in D$ if and only if $y = x[x]$.)

In light of this, I wonder whether there even is a 'reasonable' set theory in which $S$ is non-trivial and $S \notin S$ is consistent.