<p>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).</p>

<p>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.</p>

<ul>
<li><p>Assertions:</p>

<ol>
<li><p>The relation ‘part of’ is transitive:
$$\forall x,y,z. PartOf(x,y) \land PartOf(y,z) \to PartOf(x,z)$$</p></li>
<li><p>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 \}$$</p></li>
<li><p>Every class which is not null has a sum:
$$\forall a. \exists m,s. Member(m,a) \to SumOf(s,a)$$</p></li>
</ol></li>
<li><p>Proof Goal: The relation ‘part of’ is reflexive:
$$\forall x. PartOf(x,x)$$</p></li>
</ul>

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

CC BY-SA 3.0
2014-07-29T05:31:09.233Z
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
CC BY-SA 3.0
2014-07-29T15:54:13.197Z
@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
CC BY-SA 3.0
2014-07-29T16:52:50.970Z
Do you know you can use ordinary LaTeX instead of scary GIFs?
Andrej Bauer
CC BY-SA 3.0
2014-07-29T16:53:43.207Z
This is just a case of hit-and-miss, I suppose.
Andrej Bauer
CC BY-SA 3.0
2014-07-29T19:30:51.360Z
@AndrejBauer: I do know. It's just that I had this notation done already (in Theorema 2.0), and I'm not great with LaTeX. About it being hit-and-miss - that's unfortunate! I'll try Prover9, if that helps. Thanks!
Atriya
CC BY-SA 3.0
2014-07-30T12:46:48.633Z
Note that it is more difficult for a prover to find a proof when you have more axioms, not easier. You should stick to bare minimum required, if you don't need NBG axioms for the proof you shouldn't give them to the prover. ps: I edited the question and replaced the images with LaTeX, next time please don't use images. Also it makes it easier to read if you use symbols or one letter names in place of expressions like "PartOf" etc.
Kaveh
CC BY-SA 3.0
2014-07-30T12:49:16.867Z
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
CC BY-SA 3.0
2014-07-30T13:00:19.913Z
@Kaveh: Thanks for the edits. I currently think this proof should not need NBG axioms at all, since it does not use any set constructs other than membership. However, even removing those (which makes one statement to be proved from 3), the prover finds no proof. Yes, I will look into the mailing list, if any.
Atriya
CC BY-SA 3.0
2014-07-30T13:26:55.720Z
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
CC BY-SA 3.0
2014-07-30T13:32:17.407Z
2 seems to be saying something like $$\forall s,a. Sum(s,a) \to$$ $$(\forall m. m\in a \to Part(m,s)) \land$$ $$(\forall p. Part(p,s) \to \exists m. m \in a \land \forall q. Part(q,m) \leftrightarrow Part(q,p))$$
Kaveh
CC BY-SA 3.0
2014-07-30T19:24:18.807Z
@Kaveh: Thanks, and you're probably right about the mistakes. Unfortunately, the prover finds no proof with the corrected 2 and 3 either. Is it possible that this proof could take a long time? I'm only running for about 10 minutes (on a Core i7 machine).
Atriya
CC BY-SA 3.0
2014-07-30T20:44:24.617Z
I think you should try to formalize the proof you think you have. It might be the case that your proof is not correct and the statement is not true and Tarksi might have used other assumptions in addition to these.
Kaveh
CC BY-SA 3.0
2014-07-30T21:28:24.287Z
That could be. Thanks - I'll update this question with more information soon.
Atriya
<lo.logic><automated-theorem-proving><set-theory>
Theorem prover fails to find simple set theory proof?
Atriya
# Theorem prover fails to find simple set theory proof?

(Asked by: username_0 on 2014-07-28)

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)

**Tags:** lo.logic, automated-theorem-proving, set-theory
> **Comments:**
> **username_1**: 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)?  
> **username_0**: @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!  
> **username_1**: Do you know you can use ordinary LaTeX instead of scary GIFs?  
> **username_1**: This is just a case of hit-and-miss, I suppose.  
> **username_0**: @AndrejBauer: I do know. It's just that I had this notation done already (in Theorema 2.0), and I'm not great with LaTeX. About it being hit-and-miss - that's unfortunate! I'll try Prover9, if that helps. Thanks!  
> **username_2**: Note that it is more difficult for a prover to find a proof when you have more axioms, not easier. You should stick to bare minimum required, if you don't need NBG axioms for the proof you shouldn't give them to the prover. ps: I edited the question and replaced the images with LaTeX, next time please don't use images. Also it makes it easier to read if you use symbols or one letter names in place of expressions like "PartOf" etc.  
> **username_2**: 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.  
> **username_0**: @Kaveh: Thanks for the edits. I currently think this proof should not need NBG axioms at all, since it does not use any set constructs other than membership. However, even removing those (which makes one statement to be proved from 3), the prover finds no proof. Yes, I will look into the mailing list, if any.  
> **username_2**: 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.  
> **username_2**: 2 seems to be saying something like $$\forall s,a. Sum(s,a) \to$$ $$(\forall m. m\in a \to Part(m,s)) \land$$ $$(\forall p. Part(p,s) \to \exists m. m \in a \land \forall q. Part(q,m) \leftrightarrow Part(q,p))$$  
> **username_0**: @Kaveh: Thanks, and you're probably right about the mistakes. Unfortunately, the prover finds no proof with the corrected 2 and 3 either. Is it possible that this proof could take a long time? I'm only running for about 10 minutes (on a Core i7 machine).  
> **username_2**: I think you should try to formalize the proof you think you have. It might be the case that your proof is not correct and the statement is not true and Tarksi might have used other assumptions in addition to these.  
> **username_0**: That could be. Thanks - I'll update this question with more information soon.  

---

## 0 answers

