$ \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:
- $\textbf{Extensionality: } \forall z \, ( z \eps x \leftrightarrow z \eps y ) \to x=y$
- $\textbf{Atomicity: } \forall x \exists y: y \eps x$
- $\textbf{Rudimentary Membership: } \forall y \forall x: y \eps x \to \forall z \, (z \eps y \to z=y)$
- $\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$
$ \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$
$\textbf{Reflexive: } \operatorname{state}(z) \land x \eps x \to x \cz x $
$\textbf{Symmetric: } x \cz y \to y \cz x$
$\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 (x \eps x \to \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?