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)

  • 2
    $\begingroup$ 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)? $\endgroup$ Jul 29, 2014 at 5:31
  • $\begingroup$ @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! $\endgroup$
    – Atriya
    Jul 29, 2014 at 15:54
  • 6
    $\begingroup$ Do you know you can use ordinary LaTeX instead of scary GIFs? $\endgroup$ Jul 29, 2014 at 16:52
  • 1
    $\begingroup$ 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. $\endgroup$
    – Kaveh
    Jul 30, 2014 at 12:49
  • 1
    $\begingroup$ 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. $\endgroup$
    – Kaveh
    Jul 30, 2014 at 13:26


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.