Please help with translation of English to first order logic

Question

In a certain work on mereology, Alfred Tarski claims that the third following statement is deducible from the previous two:

1. The sum of a class is defined as follows: $y$ is the sum of a class $\alpha$ iff all members of $\alpha$ are parts of $y$, and for all $z$, $z$ being a part of $y$ implies that the class of parts of $z$ and the class of parts of all members of $\alpha$ are not disjoint classes. $$\sum {=} _{Df} \hat {y} \hat {\alpha} (\alpha \subset \overrightarrow {P} {'} y:.(z):zPy.\supset .P {'} {'} \alpha \cap \overrightarrow { P } {'} z\neq \Lambda )$$

2. For all $x$, the only sum of a class containing only $x$, is $x$. $$x=\sum {'} { \iota {'} x } $$

3. For all $x$, $x$ is a part of $x$. $$(x):xPx$$

(Russell-Peano notation, unfortunately.)

I am trying to automate the proof of this (or example, using Prover9), with no luck so far. Here is my translation:

1. $\forall y,\alpha :sum(y,\alpha )\leftrightarrow ((\forall p:member(p,\alpha )\rightarrow part(p,y))\wedge (\forall z:(part(z,y)\rightarrow \exists q(\exists r:(member(r,\alpha )\wedge part(q,r))\wedge part(q,z)))))$
2. $\forall x,y,\alpha :(member(x,\alpha )\wedge (\neg \exists z:(member(z,\alpha )\wedge (x\neq z)))\wedge sum(y,\alpha ))\rightarrow (x=y)$. Inside the largest parenthesis, the second term ensures that $x$ is the only member of $\alpha$.
3. $\forall x:part(x,x)$

Prover9 immediately responds with 'exhausted'. Another theorem prover, SNARK, also fails to find a proof. What mistake am I making?

Answer 1

I think that a possible origin of the problem is in forgetting that $\alpha$ is a class variable.

If we reason "informally", we have that statement 1 is (using a term operator for "sum") :

$y = sum (\alpha)$ iff $\forall x(x \in \alpha \rightarrow part(x,y))$ and ...

Statement 2 is simply :

$\alpha = \{ x \} \rightarrow sum(\alpha) = x$.

Thus, using :

$x = sum ( \{ x \})$

into the definition of "sum", we get :

$\forall x(x \in \{ x \} \rightarrow part(x,x))$.

But, by f-o logic : $\forall x (\varphi \rightarrow \psi) \rightarrow (\forall x \varphi \rightarrow \forall x \psi)$ and (intuitively) we have : $\forall x(x \in \{ x \})$.

Thus, we may conclude with :

$\forall x part(x,x)$.

---

Note

According to Principia Mathematica's symbolism, we can use $\in$ in the context : $x \in \alpha$.

The "basic" property [see 2nd ed, vol I, page 26] is : $x \in \hat{z}(\phi z) \equiv \phi x$ [in modern notation : $x \in \{ z : \phi(z) \} \equiv \phi(x)$].

$\iota‘x$ is "the class of objects which are identical with $x$" [see vol I, page 37 : $\iota‘x = \hat{y}(y = x)$ Df], i.e. the singleton : $\{ x \}$.

The "sum" is a binary relation : $\Sigma = \hat{y} \hat{\alpha} \varphi(y,\alpha)$ between a term and a class [see page 27].

Thus [see page 33] $\Sigma‘\alpha$ is the "descriptive function" associated to the relation $\Sigma$, i.e. it has as value the unique $y$ such that $y\Sigma \alpha$.

Thus, statement 2 means that $x$ is the sum of $\iota‘x$, i.e. $x= \Sigma‘ \{ x \}$.

See in Alfred Tarski, Logic, Semantics, Metamathematics : Papers from 1923 to 1938 (1956), the reprint of FOUNDATIONS OF THE GEOMETRY OF SOLIDS (1927), page 24-on.

Page 25, footnote 1 :

The terms 'individual' and 'class' are used here in the same way as in the well-known work of A.N.Whitehead and B.Russell [Principia Mathematica, 2nd ed., i-iii (Cambridge, 1925-7)].