Positive set theory and the "co-Russell" set This is a more focused version of a question which was asked at MSE 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^+$. 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$?

 A: 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. 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 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.
