Is this single-sorted set theory with sets and atoms consistent? An atom is an element of the domain that is not a set. The idea is that the elementhood predicate $\in$ is not constrained very much by the axioms when the right argument is an atom, and that this acts as a safety valve for defusing paradoxes.
I have a set theory with the following predicates:
$ S $, which determines whether something is a set, and $\in$, the elementhood relation.
$A$ meaning atom is an abbreviation for $\lnot S$.
Let $\forall x : S \mathop. \varphi$ abbreviate $\forall x \mathop. S(x) \to \varphi$ and likewise for other combinations of quantifiers and predicates.
I impose the constraint that no set can contain both sets and atoms. Let's call this the axiom of homogeneity.
$$ \lnot \exists x : S \mathop. (\exists a : S \mathop. \exists b : A \mathop. a \in x \land b \in x) $$
I also have a restricted axiom of extensionality.
$$ S(a) \land S(b) \implies [ a = b \iff (\forall x \mathop. x \in a \leftrightarrow x \in b) ]$$
; and I have a restricted form of comprehension. In the axiom schema below $\varphi$ is constrained to contain no occurrences of the predicates $S$ or $A$.
$$(\lnot \exists a : S \mathop. \exists b : A \mathop. \varphi(a) \land \varphi(b)) \implies (\exists x : S \mathop. \forall a \mathop. a \in x \leftrightarrow \varphi(a)) $$
So far, I've attempted to investigate this weird alternative set theory by throwing paradoxes at it that I've seen before. However, the comprehension restriction is so different from ZFC's and NF(U)'s that I'm stumped on how to prove its consistency relative to one of these theories.
For convenience, I'll define set-builder notation $\{ x : \varphi(x) \}$ to be the empty set $\varnothing$ when $\varphi$ holds of at least one set and at least one atom.
No restrictions at all are imposed on the $\in$ relation when the right argument is an atom. The idea is that this flexibility is a safety valve to defang possible paradoxes.
For example, the Russell set is defined as follows: $R = \{x : x \not\in x\}$.
Suppose $R$ is non-empty.
$R$ holds of at least one set, since $\varnothing \not\in \varnothing$.
Therefore $R$ contains sets alone.
Suppose $R \in R$, then by the definition of $R$, $R \not\in R$.
Suppose $R \not\in R$, then by the definition of $R$, $R \in R$.
This is a contradiction, therefore $R$ does not contain sets alone.
If $R$ would contain both a set and an atom, then the Russell predicate would hold for at least one set and at least one atom.
This is a contradiction.
Therefore $R$ is empty.
Russell's paradox is then a proof that $x \not\in x$ holds for at least one atom $m$.
Let's consider the paradoxical set $A = \{ A : A \in A \to \varphi \}$.
This set is equivalent to $A = \{A : A \not\in A \lor \varphi \}$.
However, the first predicate holds for at least one set and at least one atom $m$, therefore $A$ is empty.
As written the theory is clearly inconsistent.
Let $\varphi(x)$ be the formula $x=\emptyset$, where $\emptyset$ is the empty set, use it in comprhension, and we'll have: $x = \emptyset \iff x \neq \emptyset$.
If $\varphi(x)$ in comprehension is changed to $\varphi(a)$ [as it should be], then I think we get a consistent but weak theory.