$ \newcommand{\Pt}{ \ \mathbb P \ }$ $\newcommand {\cz}{\ C_z \ }$ $\newcommand {\eps}{\ \varepsilon \ }$

Logic: first order logic with equality

Extra-logical primitives:

• "$\varepsilon$" standing for the binary relation "is an atom part of",
• a ternary relation symbol $C_z$ standing for "is connected to according to $z$".

Axioms:

1. $\textbf{Extensionality: } \forall z \, ( z \eps x \leftrightarrow z \eps y ) \to x=y$
2. $\textbf{Atomicity: } \forall x \exists y: y \eps x$
3. $\textbf{Rudimentary Membership: } \forall y \forall x: y \eps x \to \forall z \, (z \eps y \to z=y)$
4. $\textbf{Comprehension: } \exists y \, ( y \eps y \land \phi(y)) \to \exists x \forall y \, (y \eps x \leftrightarrow y \eps y \land \phi(y))$

Now, we can retrieve all of the known Mereological axioms about the part-hood relation $\mathbb P$ by simply defining parthood as: $$ x \Pt y \iff \forall z \eps x (z \eps y)$$ It can be easily verified that $\varepsilon$ is the atomic part-hood with respect to $\mathbb P$. We do have: $\forall x: x \eps x \iff \forall y: y \Pt x \to y=x$

5. $ \textbf{Atomhood: } x \cz y \to x \eps x \land y\eps y \land z\eps z$

   $\textbf{Define: } \operatorname{state}(z) \iff \exists x \exists y : x \cz y$

6. $\textbf{Reflexive: } \operatorname{state}(z) \land x \eps x \to x \cz x $

7. $\textbf{Symmetric: } x \cz y \to y \cz x$

8. $\textbf{States Extensionality: } \forall \operatorname {states}z,k: \forall x \forall y \, (x \cz y \leftrightarrow x \ C_k \ y) \to z=k $

   $\textbf{Define: } x \in z \iff \operatorname{state}(z) \land x \eps x \, \land \, \forall y: y \neq x \to \neg y \cz x $

   $\textbf{Define: } \operatorname {contacting}_z(x) \iff \exists y: y \neq x \land x \cz y$

   $\textbf{Define: } \operatorname {uniform}(z) \iff \forall x \forall y \, ( \operatorname{contacting}_z(x) \land \operatorname{contacting}_z(y) \to x \cz y)$

   $\textbf{Define: } \operatorname {set} (z) \iff \operatorname {state}(z) \land \operatorname {uniform} (z)$

   $\textbf{Define: } \operatorname {nse}(z) \iff z \eps z \land \neg \operatorname {set}(z) $

   $\textbf{Define: } \operatorname {ur}(z) \iff \operatorname {nse}(z) \land \forall x \exists y: y \neq x \land x \cz y $

/

"$\operatorname {nse}$" is short for non-set element. Now, I think the above system is consistent. What it lacks is a comprehension axiom for relation $C$. I'm contemplating the following one:

Connections: if $\phi(x,y)$ is formula that doesn't use the symbols "$C$" and "$z$", whose free variables are "$x,y,w_1,\ldots,w_n$"; then:

$$w_1 \eps w_1 \land \cdots \land w_n \eps w_n \land \forall x \forall y [\phi(x,y) \to \phi(y,x)] \\ \to \\ \exists \operatorname {state} z: \forall x \forall y \, (x \cz y \land x \neq y \leftrightarrow x \neq y \land x \eps x \land y \eps y \land \phi(x,y) )$$

It might be possible to allow $C$ in $\phi$ but only as $C_{w_i}$.

I think if the above theory is consistent then it could possibly be equal to second order arithmetic? One peculiar matter is that it does have a universal set. And, this is a suspicious feature.

Is that theory consistent?

If we allow $C$ in Connections as mentioned above would this be consistent?