*This is a more focused version of a question which was [asked at MSE](https://math.stackexchange.com/q/2431146/28111) a couple years ago, but is still unanswered there. That question asks about a broad range of theories, whereas this version focuses on a single one.*


Let $S=\{x: x\in x\}$ be the "dual" to Russell's paradoxical set $R$, and consider the question "Is $S\in S$?" If we try to work purely "naively" there does not seem to be an immediate argument one way or the other (dually to the situation for $R$). However, in light of Lob's theorem it's a bit premature to leap to the conclusion that there actually **are** no such arguments. 


So it remains plausible that there is a "reasonable" set theory in which the question "Is $S\in S$?" is decided in a nontrivial way. Note that the nontriviality requirement rules out both $\mathsf{ZF}$- and $\mathsf{NF}$-style set theories: the former prove $S=\emptyset$, while the latter prove that $S$ is not a set in the first place.


The most appealing candidate to me appears to be [$\mathsf{GPK}\_\infty^+$](https://plato.stanford.edu/entries/settheory-alternative/#SystGPKiOlivEsse). This theory proves that $S$ is a set and is nonempty. It also (in my opinion) has a very attractive intuition behind it, as well as an interesting model theory. So my question is:



> 
> Does $\mathsf{GPK}\_\infty^+$ decide whether $S\in S$?
> 
> 
> 



Positive set theory and the "co-Russell" set
This answer has been superseded by a more general argument (based on a result of Cantini's) that I have posted as [an answer to Noah's original MSE question](https://math.stackexchange.com/a/4515237/228583). In particular, a fairly weak fragment of $\mathsf{GPK}$ is enough to entail that $S \in S$.




---


I will show that $\mathsf{GPK}\_\infty^+$ is consistent with $S \in S$, under the assumption of a weakly compact cardinal. Specifically, I'll show that the 'standard models' of $\mathsf{GPK}\_\infty^+$ (which require weakly compact cardinals) satisfy $S \in S$. I've made very little progress with proving anything from $\mathsf{GPK}\_\infty^+$ directly, although this is probably my failing.


The main idea of the argument is very simple: Show that these models satisfy that for every set $X$, there exists a set $Y$ satisfying $Y = X \cup \{Y\}$. You then note that $S$ must be a fixed point of this operation, so it must be the case that $S \in S$.


For the sake of completeness, I will give the construction of a model of $\mathsf{GPK}\_\infty^+$ in a way that should feel familiar to classical set theorists. I'm also doing this because I couldn't find a presentation of this construction that I liked online, although I did use the Stanford Encyclopedia of Philosophy article [Alternative Axiomatic Set Theories](https://plato.stanford.edu/entries/settheory-alternative/) to get the general idea.




---


**Construction**


Recall that a *forest* is a partially ordered set in which the set of predecessors of any element is well-ordered. A *tree* is a forest with a unique minimal element. I'll use the word *path* to refer to a downwards-closed, linearly ordered set. (I can't remember if there's a standard term for this.) The *height* of a path is its order type as an ordinal. The *height* of a node $x \in T$ is the height of the path $\{ y \in T : y < x\}$. To make the presentation more uniform between successor and limit stages, we'll refer to paths as having *children*, rather than just nodes. A node $x$ is the child of a path $A$ if $\{ y \in T : y < x\} = A$. A path $A$ is the *parent* of a node $x$ if $x$ is the child of $A$. Finally, a *branch* is a path of maximal height. (The forest we will construct will not have any dead paths that are shorter than the forest itself.)


We will build a forest (although really it's just a tree and an isolated branch corresponding to the empty set) whose nodes of height $\alpha$ are labeled with sets of paths of height $\alpha$. (Note that this isn't circular, because the paths of height $\alpha$ do not contain nodes of height $\alpha$.) Every set of paths of height $\alpha$ will be attached to precisely one node of height $\alpha$. We will use the convention that lowercase letters refer to sets of paths and that uppercase letters refer to paths of sets.


At stage $0$, there is a unique path of length $0$, the empty path $\Lambda$, and there are two sets of such paths, the empty set and the singleton $\{\Lambda\}$, so these are the roots of the two trees in our forest.


At non-zero stage $\alpha$, given the forest built up to height $\alpha$, we add each set $x$ of paths of length $\alpha$ as a node. The parent of the node $x$ is the unique path $A$ with the property that for any node $y \in A$,


* for every $B \in x$, there exists a $C \in y$ such that $B$ extends $C$ and
* for every $C \in y$, there exists a $B \in x$ such that $B$ extends $C$.


It is not hard to show by induction that this is well defined.


Now we build this forest up to a height $\kappa$, where $\kappa$ is a weakly compact cardinal. The elements of the model are the branches of the forest, and the element of relation is defined by $A \in B$ iff for every $\alpha < \kappa$, $A \upharpoonright \alpha \in B(\alpha)$. This structure is typically referred to as the *$\kappa$-hyperuniverse*, but I'll just call it $M$.




---


**Argument**


I claim that $M$ satisfies the following:



> 
> For every $X \in M$, there exists $Y \in M$ such that $Z \in Y$ if and only if either $Z \in X$ or $Z = Y$.
> 
> 
> 


It's easy to see how this resolves the status of $S \in S$. Let $S' = S \cup \{S'\}$. Clearly by construction, $S' \supseteq S$ and $S' \in S'$. Therefore we have $S' \in S$, but this implies that $S \supseteq S'$, so $S = S'$ and $S \in S$. I think the most reasonable approach to resolving your question would be to prove this claim directly from $\mathsf{GPK}\_\infty^+$, but I can't even show that $\mathsf{GPK}\_\infty^+$ entails the existence of a Quine atom. (Or that any two Quine atoms are equal, for that matter.) Someone probably knows how to do this, though, and I'd be interested to see it.


*Proof of claim.* To prove this, consider the path corresponding to $X$. Let $Y$ be the $\kappa$-indexed sequence of nodes on the forest defined inductively by $Y(\alpha) = X(\alpha) \cup \{ Y \upharpoonright \alpha\}$ for each $\alpha < \kappa$. We need to show that this is well defined.


* For $\alpha = 0$, $Y \upharpoonright 0 = \Lambda$, so $Y(0) = X(0) \cup \{\Lambda\}$.
* For a non-zero $\alpha$, assuming we've shown that $Y \upharpoonright \alpha$ is actually a path on the forest, we immediately get that $Y(\alpha) = X(\alpha) \cup \{ Y \upharpoonright \alpha\}$ is a node of height $\alpha$ in the forest. We just need to show that $Y(\alpha)$'s parent is $Y\upharpoonright \alpha$. Fix a node $Y(\beta) \in Y \upharpoonright \alpha$ (for some $\beta < \alpha$). For any $A \in Y(\alpha)$, either $A \in X(\alpha)$ or $A = Y\upharpoonright \alpha$. In the first case, by the fact that $X\upharpoonright \alpha$ is a path, there must exist a $B \in X(\alpha)$ such that $A$ extends $B$. In the second case, $Y \upharpoonright \beta \in Y(\beta)$ and is extended by $Y\upharpoonright \alpha$ (by the induction hypothesis). Essentially the same argument gives that for any $B \in Y(\beta)$, there is an $A \in Y(\alpha)$ extending $B$.


Therefore $Y$ is a branch of the forest and corresponds to an element of $M$. $Y$ is clearly a superset of $X$ and clearly contains $Y$ as an element. We need to show that $Y = X \cup \{Y\}$.


Suppose that $Z \in Y$. For each $\alpha < \kappa$, we get that either $Z \upharpoonright \alpha = Y \upharpoonright \alpha$ or $Z \upharpoonright \alpha \in X(\alpha)$. Because of the way forests/trees work, if there is an $\alpha$ such that $Z \upharpoonright \alpha \neq Y \upharpoonright \alpha$, then this must also be true for any $\beta \in (\alpha,\kappa)$. Therefore, if $Z \neq Y$, then for some $\alpha < \kappa$, we have that $Z \upharpoonright \beta \in X(\beta)$ for all $\beta \in (\alpha,\kappa)$. It's not hard to show that the same must be true for any $\beta <\kappa$, so we have that $Z \in X$, proving the claim.


