Before I'll present the exposition of this theory, I'll speak a little bit about the Mereological concept it is meant to catpure.

The idea is to work in Atomic General Extensional Mereology "AGEM", one can think of it easily as a theory about collections of atoms, where atoms are indivisible objects, i.e. objects that do not have proper parts. The relation is an atomic part of is defined as:

$\sf Definition:$ $x P^a y \iff atom(x) \land x P y$.

where $P$ stands for "is a part of", and atom(x) is defined as:

$atom(x) \iff \not \exists y (y P x \land y \neq x)$

This atomic part-hood relation can be regarded, conceptually speaking, as an instance of set membership relation.

Now the following theory is a try to define a set theory by a strategy of mimicking properties of this atomic part-hood relation with the background theory being AGEM.

Notation: let $\phi^{P^a}$ denote a formula that only use the binary relation $P^a$ or otherwise the equality relation, as predicate symbols. The notation $\phi^{\in|P^a}$ denotes the formula obtained by merely replacing each occurrence of the symbol $``P^a"$ in $\phi^{P^a}$ by the symbol $``\in"$.

Comprehension axiom schema: if $\phi^{\in|P^a}(y)$ doesn't have the symbol $x$ occurring free, then all closures of:

$$\forall A [\exists x \forall y (y \ P^a \ x \leftrightarrow \phi^{P^a}(y)) \to \exists x \forall y (y \in x \leftrightarrow \phi^{\in|P^a}(y))]$$

are axioms.

In order to complete this theory we add axioms of Extensionality, Empty set and Singletons:

Extensionality: $\forall xy [\forall z (z \in x \leftrightarrow z \in y) \to x=y]$.

Empty set: $\exists x \forall y (y \not \in x)$

Singletons:: $\forall A \exists x \forall y (y \in x \leftrightarrow y=A)$

This theory has a universal set, also has a set of all sets that are in themselves, however it doesn't have complements; axioms of Set union and Power are there. There are separation axioms for formulas $\phi^{\in|P^a}$ where $\phi^{P^a}$ holds of at least one atom. Similarly replacement axioms are granted if $\phi^{P^a}$ formula replace atoms with atoms and of course holds of at least one atom.

The trick is that all formulas of the form $x \not \in x$, $\exists x_1,..,x_n: \neg (x_1 \in x_2 \land...\land x_n \in x_1)$; $x \text { is well founded }$, $x \text{ is a von Neumann ordinal }$, etc.. all of those won't have their $\phi^{P^a}$ corresponding formulas hold of mereological atoms and so cannot be used in comprehension because there do not exist an object that has no atomic parts, since we are already working in AGEM.

Question: if one attempts to prove the consistency of this theory, which of the known alternative set theories have in some sense a near structure to this theory, other than positive set theory?

Before I'll present the exposition of this theory, I'll speak a little bit about the Mereological concept it is meant to catpure.

The idea is to work in Atomic General Extensional Mereology "AGEM", one can think of it easily as a theory about collections of atoms, where atoms are indivisible objects, i.e. objects that do not have proper parts. The relation is an atomic part of is defined as:

$\sf Definition:$ $x P^a y \iff atom(x) \land x P y$.

where $P$ stands for "is a part of", and atom(x) is defined as:

$atom(x) \iff \not \exists y (y P x \land y \neq x)$

This atomic part-hood relation can be regarded, conceptually speaking, as an instance of set membership relation.

Now the following theory is a try to define a set theory by a strategy of mimicking properties of this atomic part-hood relation with the background theory being AGEM.

Notation: let $\phi^{P^a}$ denote a formula that only use the binary relation $P^a$ or otherwise the equality relation, as predicate symbols. The notation $\phi^{\in|P^a}$ denotes the formula obtained by merely replacing each occurrence of the symbol $``P^a"$ in $\phi^{P^a}$ by the symbol $``\in"$.

Comprehension axiom schema: if $\phi^{\in|P^a}(y)$ doesn't have the symbol $x$ occurring free, then all closures of:

$$\exists x \forall y (y \ P^a \ x \leftrightarrow \phi^{P^a}(y)) \to \exists x \forall y (y \in x \leftrightarrow \phi^{\in|P^a}(y))$$

are axioms.

In order to complete this theory we add axioms of Extensionality, Empty set and Singletons:

Extensionality: $\forall xy [\forall z (z \in x \leftrightarrow z \in y) \to x=y]$.

Empty set: $\exists x \forall y (y \not \in x)$

Singletons:: $\forall A \exists x \forall y (y \in x \leftrightarrow y=A)$

This theory has a universal set, also has a set of all sets that are in themselves, however it doesn't have complements; axioms of Set union and Power are there. There are separation axioms for formulas $\phi^{\in|P^a}$ where $\phi^{P^a}$ holds of at least one atom. Similarly replacement axioms are granted if $\phi^{P^a}$ formula replace atoms with atoms and of course holds of at least one atom.

The trick is that all formulas of the form $x \not \in x$, $\exists x_1,..,x_n: \neg (x_1 \in x_2 \land...\land x_n \in x_1)$; $x \text { is well founded }$, $x \text{ is a von Neumann ordinal }$, etc.. all of those won't have their $\phi^{P^a}$ corresponding formulas hold of mereological atoms and so cannot be used in comprehension because there do not exist an object that has no atomic parts, since we are already working in AGEM.

Question: if one attempts to prove the consistency of this theory, which of the known alternative set theories have in some sense a near structure to this theory, other than positive set theory?

Before I'll present the exposition of this theory, I'll speak a little bit about the Mereological concept it is meant to catpure.

The idea is to work in Atomic General Extensional Mereology "AGEM", one can think of it easily as a theory about collections of atoms, where atoms are indivisible objects, i.e. objects that do not have proper parts. The relation is an atomic part of is defined as:

$\sf Definition:$ $x P^a y \iff atom(x) \land x P y$.

where $P$ stands for "is a part of", and atom(x) is defined as:

$atom(x) \iff \not \exists y (y P x \land y \neq x)$

This atomic part-hood relation can be regarded, conceptually speaking, as an instance of set membership relation.

Now the following theory is a try to define a set theory by a strategy of mimicking properties of this atomic part-hood relation with the background theory being AGEM.

Notation: let $\phi^{P^a}$ denote a formula that only use the binary relation $P^a$ or otherwise the equality relation, as predicate symbols. The notation $\phi^{\in|P^a}$ denotes the formula obtained by merely replacing each occurrence of the symbol $``P^a"$ in $\phi^{P^a}$ by the symbol $``\in"$.

Comprehension axiom schema: if $\phi^{\in|P^a}(y)$ doesn't have the symbol $x$ occurring free, then all closures of:

$$\forall A [\exists x \forall y (y \ P^a \ x \leftrightarrow \phi^{P^a}(y)) \to \exists x \forall y (y \in x \leftrightarrow \phi^{\in|P^a}(y))]$$

are axioms.

In order to complete this theory we add axioms of Extensionality, Empty set and Singletons:

Extensionality: $\forall xy [\forall z (z \in x \leftrightarrow z \in y) \to x=y]$.

Empty set: $\exists x \forall y (y \not \in x)$

Singletons:: $\forall A \exists x \forall y (y \in x \leftrightarrow y=A)$

This theory has a universal set, also has a set of all sets that are in themselves, however it doesn't have complements; axioms of Set union and Power are there. There are separation axioms for formulas $\phi^{\in|P^a}$ where $\phi^{P^a}$ holds of at least one object. Similarily replacement axioms are granted if $\phi^{P^a}$ formula replace atoms with atoms and of course is non empty.

The trick is that all formulas of the form $x \not \in x$, $\exists x_1,..,x_n: \neg (x_1 \in x_2 \land...\land x_n \in x_1)$; $x \text { is well founded }$, $x \text{ is a von Neumann ordinal }$, etc.. all of those won't have their $\phi^{P^a}$ corresponding formulas hold of mereological atoms and so cannot be used in comprehension because there do not exist an object that has no atomic parts, since we are already working in AGEM.

Question: if one attempts to prove the consistency of this theory, which of the known alternative set theories have in some sense a near structure to this theory, other than positive set theory?

Before I'll present the exposition of this theory, I'll speak a little bit about the Mereological concept it is meant to catpure.

The idea is to work in Atomic General Extensional Mereology "AGEM", one can think of it easily as a theory about collections of atoms, where atoms are indivisible objects, i.e. objects that do not have proper parts. The relation is an atomic part of is defined as:

$\sf Definition:$ $x P^a y \iff atom(x) \land x P y$.

where $P$ stands for "is a part of", and atom(x) is defined as:

$atom(x) \iff \not \exists y (y P x \land y \neq x)$

This atomic part-hood relation can be regarded, conceptually speaking, as an instance of set membership relation.

Now the following theory is a try to define a set theory by a strategy of mimicking properties of this atomic part-hood relation with the background theory being AGEM.

Notation: let $\phi^{P^a}$ denote a formula that only use the binary relation $P^a$ or otherwise the equality relation, as predicate symbols. The notation $\phi^{\in|P^a}$ denotes the formula obtained by merely replacing each occurrence of the symbol $``P^a"$ in $\phi^{P^a}$ by the symbol $``\in"$.

Comprehension axiom schema: if $\phi^{\in|P^a}(y)$ doesn't have the symbol $x$ occurring free, then all closures of:

$$\forall A [\exists x \forall y (y \ P^a \ x \leftrightarrow \phi^{P^a}(y)) \to \exists x \forall y (y \in x \leftrightarrow \phi^{\in|P^a}(y))]$$

are axioms.

In order to complete this theory we add axioms of Extensionality, Empty set and Singletons:

Extensionality: $\forall xy [\forall z (z \in x \leftrightarrow z \in y) \to x=y]$.

Empty set: $\exists x \forall y (y \not \in x)$

Singletons:: $\forall A \exists x \forall y (y \in x \leftrightarrow y=A)$

This theory has a universal set, also has a set of all sets that are in themselves, however it doesn't have complements; axioms of Set union and Power are there. There are separation axioms for formulas $\phi^{\in|P^a}$ where $\phi^{P^a}$ holds of at least one atom. Similarly replacement axioms are granted if $\phi^{P^a}$ formula replace atoms with atoms and of course holds of at least one atom.

The trick is that all formulas of the form $x \not \in x$, $\exists x_1,..,x_n: \neg (x_1 \in x_2 \land...\land x_n \in x_1)$; $x \text { is well founded }$, $x \text{ is a von Neumann ordinal }$, etc.. all of those won't have their $\phi^{P^a}$ corresponding formulas hold of mereological atoms and so cannot be used in comprehension because there do not exist an object that has no atomic parts, since we are already working in AGEM.

Question: if one attempts to prove the consistency of this theory, which of the known alternative set theories have in some sense a near structure to this theory, other than positive set theory?

Before I'll present the exposition of this theory, I'll speak a little bit about the Mereological concept it is meant to catpure.

The idea is to work in Atomic General Extensional Mereology "AGEM", one can think of it easily as a theory about collections of atoms, where atoms are indivisible objects, i.e. objects that do not have proper parts. The relation is an atomic part of is defined as:

$\sf Definition:$ $x P^a y \iff atom(x) \land x P y$.

where $P$ stands for "is a part of", and atom(x) is defined as:

$atom(x) \iff \not \exists y (y P x \land y \neq x)$

This atomic part-hood relation can be regarded, conceptually speaking, as an instance of set membership relation.

Now the following theory is a try to define a set theory by a strategy of mimicking properties of this atomic part-hood relation with the background theory being AGEM.

Notation: let $\phi^{P^a}$ denote a formula that only use the binary relation $P^a$ or otherwise the equality relation, as predicate symbols. The notation $\phi^{\in|P^a}$ denotes the formula obtained by merely replacing each occurrence of the symbol $``P^a"$ in $\phi^{P^a}$ by the symbol $``\in"$.

Comprehension axiom schema: if $\phi^{\in|P^a}(y)$ doesn't have the symbol $x$ occurring free, then all closures of:

$$\forall A [\exists x \forall y (y \ P^a \ x \leftrightarrow \phi^{P^a}(y)) \to \exists x \forall y (y \in x \leftrightarrow \phi^{\in|P^a}(y))]$$

are axioms.

In order to complete this theory we add axioms of Extensionality, Empty set and Singletons:

Extensionality: $\forall xy [\forall z (z \in x \leftrightarrow z \in y) \to x=y]$.

Empty set: $\exists x \forall y (y \not \in x)$

Singletons:: $\forall A \exists x \forall y (y \in x \leftrightarrow y=A)$

This theory has a universal set, also has a set of all sets that are in themselves, however it doesn't have complements; axioms of Set union and Power are there. There are separation axioms for formulas $\phi^{\in|P^a}$ where $\phi^{P^a}$ holds of at least one object. Similarily replacement axioms are granted if $\phi^{P^a}$ formula replace atoms with atoms and of course is non empty.

The trick is that all formulas of the form $x \not \in x$, $\exists x_1,..,x_n: \neg (x_1 \in x_2 \land...\land x_n \in x_1)$; $x \text { is well founded }$, $x \text{ is a von Neumann ordinal }$, etc.. all of those won't have their $\phi^{P^a}$ corresponding formulas hold of mereological atoms and so cannot be used in comprehension because there do not exist an object that has no atomic parts, since we are already working in AGEM.

Question: if one attempts to prove the consistency of this theory, which of the known alternative set theories have in some sense the nearest structure to this theory, other than positive set theory?

Before I'll present the exposition of this theory, I'll speak a little bit about the Mereological concept it is meant to catpure.

The idea is to work in Atomic General Extensional Mereology "AGEM", one can think of it easily as a theory about collections of atoms, where atoms are indivisible objects, i.e. objects that do not have proper parts. The relation is an atomic part of is defined as:

$\sf Definition:$ $x P^a y \iff atom(x) \land x P y$.

where $P$ stands for "is a part of", and atom(x) is defined as:

$atom(x) \iff \not \exists y (y P x \land y \neq x)$

This atomic part-hood relation can be regarded, conceptually speaking, as an instance of set membership relation.

Now the following theory is a try to define a set theory by a strategy of mimicking properties of this atomic part-hood relation with the background theory being AGEM.

Notation: let $\phi^{P^a}$ denote a formula that only use the binary relation $P^a$ or otherwise the equality relation, as predicate symbols. The notation $\phi^{\in|P^a}$ denotes the formula obtained by merely replacing each occurrence of the symbol $``P^a"$ in $\phi^{P^a}$ by the symbol $``\in"$.

Comprehension axiom schema: if $\phi^{\in|P^a}(y)$ doesn't have the symbol $x$ occurring free, then all closures of:

$$\forall A [\exists x \forall y (y \ P^a \ x \leftrightarrow \phi^{P^a}(y)) \to \exists x \forall y (y \in x \leftrightarrow \phi^{\in|P^a}(y))]$$

are axioms.

In order to complete this theory we add axioms of Extensionality, Empty set and Singletons:

Extensionality: $\forall xy [\forall z (z \in x \leftrightarrow z \in y) \to x=y]$.

Empty set: $\exists x \forall y (y \not \in x)$

Singletons:: $\forall A \exists x \forall y (y \in x \leftrightarrow y=A)$

This theory has a universal set, also has a set of all sets that are in themselves, however it doesn't have complements; axioms of Set union and Power are there. There are separation axioms for formulas $\phi^{\in|P^a}$ where $\phi^{P^a}$ holds of at least one object. Similarily replacement axioms are granted if $\phi^{P^a}$ formula replace atoms with atoms and of course is non empty.

The trick is that all formulas of the form $x \not \in x$, $\exists x_1,..,x_n: \neg (x_1 \in x_2 \land...\land x_n \in x_1)$; $x \text { is well founded }$, $x \text{ is a von Neumann ordinal }$, etc.. all of those won't have their $\phi^{P^a}$ corresponding formulas hold of mereological atoms and so cannot be used in comprehension because there do not exist an object that has no atomic parts, since we are already working in AGEM.

Question: if one attempts to prove the consistency of this theory, which of the known alternative set theories have in some sense a near structure to this theory, other than positive set theory?