# Theorem prover fails to find simple set theory proof?

I am trying to use an automated theorem prover (SNARK) to prove a theorem in first-order logic. Tarski claims in his "a work on mereology" that the goal is provable from assertions 1-3 but he does not give a proof (I have found an easy proof by contradiction).

However SNARK is currently unable to find a proof, even with the axioms of (NBG) set theory in [1]. Any suggestions will be greatly appreciated.

• Assertions:

1. The relation ‘part of’ is transitive: $$\forall x,y,z. PartOf(x,y) \land PartOf(y,z) \to PartOf(x,z)$$

2. The sum of a class is defined as follows: x is the sum of a class alpha if alpha is contained in the ‘parts’ of x, and if when y is any part of x there is always a z belonging to alpha having parts in common with the parts of y: $$\forall x,y,a,t. \exists z,p. SumOf(x,a) \to (Member(t,a) \to PartOf(t,x)) \land (PartOf(y,z) \to Member(z,a) \land PartOf(p,z) \land PartOf(p,y))$$ This was originally given in Peano-Russell notation as: $$S=_{Df} \hat{x} \hat{\alpha} \{\alpha\subset\vec{P^‘} x:.(y):yPx.\supset .(\exists z).z\in \alpha .\vec{P^‘} y\cap \vec {P^‘} z\neq \Lambda \}$$

3. Every class which is not null has a sum: $$\forall a. \exists m,s. Member(m,a) \to SumOf(s,a)$$

• Proof Goal: The relation ‘part of’ is reflexive: $$\forall x. PartOf(x,x)$$

[1] Automated Development of Fundamental Mathematical Theories, by Art Quaife, Kluwer Acadamic Publishers (1992)

• Please, can we have these formulas in non-LISP form? There seem a lot of undefined concepts here. How is part-of defined or axiomatized? Same for sum-of (not in words, in LaTeX)? – Andrej Bauer Jul 29 '14 at 5:31
• @AndrejBauer: I substituted LISP code with 'readable' notation. 'PartOf' is taken as an undefined concept (1.1.1 is its transitivity). 'SumOf' is defined in 1.1.2. 'Member' is set membership ('a' is always a set/class). Thanks! – Atriya Jul 29 '14 at 15:54
• Do you know you can use ordinary LaTeX instead of scary GIFs? – Andrej Bauer Jul 29 '14 at 16:52
• Btw, I think this question (at least in its current form) is not a good question for cstheory: it is too specific and unlikely to be useful/interesting for anyone else. I think this kind of questions are more suitable for mailing list dedicated for these provers. – Kaveh Jul 30 '14 at 12:49
• It might be because you have not correctly formalized the axioms, e.g. I think 3 should be $\forall a. \exists m. m \in a \to \exists s. Sum(s,a)$, you cannot take the $\exists s$ out, it is negated because of $\to$ preceding it. Similarly you might have made a mistake in formalizing 2. – Kaveh Jul 30 '14 at 13:26