Consider the minimal normal modal logic $K$ (axioms = classical propositional logic + $(\Box(p\land q)\leftrightarrow\Box p\land\Box q)$ + $(\Box\top)$, nothing else).

Its canonical model with no variables is a descriptive frame $(W,R)$. Among several possible descriptions of this frame is the following. Let $\mathbf V$ denote the Vietoris endofunctor on the category of Stone spaces. Then $W$ is a final $\mathbf V$-coalgebra; in particular $R:W\to\mathbf V(W)$ is a homeomorphism.

Reading this $R$ as $"\ni"$ one obtains certain model of set theory. The above fact about the final coalgebra means that sets definable in this theory are precisely the closed subsets of $W$. In fact for any closed subset $C\in\mathbf V(W)$ there is a unique $c\in W$ with $C=\{x\mid x"\in"c\}$.

This theory seems to be rather weird, e. g. there is the universal set $w$ with $x"\in"w$ for all $x$ (so necessarily $w"\in"w$; foundation is violently violated), many such things.

Is axiomatic description of this set theory and its properties worked out anywhere?

Consider the minimal normal modal logic $K$ (axioms = classical propositional logic + $(\Box(p\land q)\leftrightarrow\Box p\land\Box q)$ + $(\Box\top)$, nothing else).

Its canonical model with no variables is a descriptive frame $(W,R)$. Among several possible descriptions of this frame is the following. Let $\mathbf V$ denote the Vietoris endofunctor on the category of Stone spaces. Then $W$ is a final $\mathbf V$-coalgebra; in particular $R:W\to\mathbf V(W)$ is a homeomorphism.

Reading this $R$ as $"\ni"$ one obtains certain model of set theory. The above fact about the final coalgebra means that for any closed subset $C\in\mathbf V(W)$ there is a unique $c\in W$ with $C=\{x\mid x"\in"c\}$.

Note that powersets exist for those $c\in W$ corresponding to clopen $C$. Indeed for the latter, $\Box C:=\{x\in W\mid R(x)\subseteq C\}$ is again clopen. (An aside - is $\Box C$ closed for $C$ closed?) Then there is (as a particular case of the above) a unique $pc\in W$ with $\Box C=\{x\mid x"\in"pc\}$, so that $x"\in"pc$ holds iff $R(x)\subseteq C$, i. e. iff $\forall y\ (y"\in"x)\Rightarrow(y"\in"c)$.

This theory seems to be rather weird, e. g. there is the universal set $w$ with $x"\in"w$ for all $x$ (so necessarily $w"\in"w$; foundation is violently violated), many such things.

Is axiomatic description of this set theory and its properties worked out anywhere?

Consider the minimal normal modal logic $K$ (axioms = classical propositional logic + $(\Box(p\land q)\leftrightarrow\Box p\land\Box q)$ + $(\Box\top)$, nothing else).

Its canonical model with no variables is a descriptive frame $(W,R)$. Among several possible descriptions of this frame is the following. Let $\mathbf V$ denote the Vietoris endofunctor on the category of Stone spaces. Then $W$ is a final $\mathbf V$-coalgebra; in particular $R:W\to\mathbf V(W)$ is a homeomorphism.

Reading this $R$ as $"\ni"$ one obtains certain model of set theory. The above fact about the final coalgebra means that sets definable in this theory are precisely the closed subsets of $W$. In fact for any closed subset $C\in\mathbf V(W)$ there is a unique $x\in W$ with $C=\{y\mid y"\in"x\}$.

This theory seems to be rather weird, e. g. there is the universal set $w$ with $x"\in"w$ for all $x$ (so necessarily $w"\in"w$; foundation is violently violated), many such things.

Is axiomatic description of this set theory and its properties worked out anywhere?

Consider the minimal normal modal logic $K$ (axioms = classical propositional logic + $(\Box(p\land q)\leftrightarrow\Box p\land\Box q)$ + $(\Box\top)$, nothing else).

Its canonical model with no variables is a descriptive frame $(W,R)$. Among several possible descriptions of this frame is the following. Let $\mathbf V$ denote the Vietoris endofunctor on the category of Stone spaces. Then $W$ is a final $\mathbf V$-coalgebra; in particular $R:W\to\mathbf V(W)$ is a homeomorphism.

Reading this $R$ as $"\ni"$ one obtains certain model of set theory. The above fact about the final coalgebra means that sets definable in this theory are precisely the closed subsets of $W$. In fact for any closed subset $C\in\mathbf V(W)$ there is a unique $c\in W$ with $C=\{x\mid x"\in"c\}$.

This theory seems to be rather weird, e. g. there is the universal set $w$ with $x"\in"w$ for all $x$ (so necessarily $w"\in"w$; foundation is violently violated), many such things.

Is axiomatic description of this set theory and its properties worked out anywhere?