<p>There are numerous ways of formalizing set theory:</p>

<ul>
<li>ZFC uses first-order logic and a primitive relation $\in$</li>
<li>NBG uses first-order logic, a primitive relation $\in$, and a primitive predicate $S$</li>
<li>Church's type theory is multi-sorted and uses infintely many types</li>
<li>Type theory is similar to set theory, but not quite the same</li>
<li>Second-order arithmetic, through some coding tricks, can express many things we usually want to express in analysis</li>
<li>etc.</li>
</ul>

<p>But this is all quite irrelevant to what you are doing. You seem to be using automated theorem provers as "black boxes" to prove simple theorems in set theory. This is a hit-and-miss activity: some theorem provers will prove some simple things, and others will prove other simple things, but they will all fail on statements that mathematicians consider "completely trivial". Such is the state of automated theorem proving.</p>

<p>Rather than worrying which particular formalism you are using, you should investigate which automated theorem prover is good for what. It is also very likely that you do not actually need set theory. It would be helpful if you described what you're doing, but not here, this should go on <a href="http://cstheory.stackexchange.com">cstheory.stackexchange.com</a>. There perhaps we can suggest a good way of formalizing whatever you are doing.</p>

CC BY-SA 3.0
2014-07-28T15:11:15.257Z
Thanks for replying. Firstly - you say that this question should go on cstheory.stackexchange.com. Isn't that exactly where I posted it? Did you mean Math SE?
Atriya
CC BY-SA 3.0
2014-07-28T15:45:19.977Z
Now - although set theory can be formalized in ZFC, from what I understand, this is not relevant to ATP, since the axiomatization is not finite. NBG, however, can be finitely axiomatized. However, as you state, it uses the primitive concepts ∈ and S. In Quaife's NBG axioms in FOL, there is no axiom which explains the 'meaning' of ∈ or S in FOL - indeed, as you state, these are to be taken as primitives, hence no such axiom is possible. My question was - with FOL thus unable to 'define' ∈ (apparently HOL can, from the SEP entry), how can set theory theorems be expected to be proved in FOL?
Atriya
CC BY-SA 3.0
2014-07-28T15:48:12.650Z
I asked this question as I am trying to do exactly that - prove set theory theorems in FOL with NBG axioms - with no success so far. Yes, I am using the ATP as a black box. I understand your comments about hit-and-miss, and I'll post a question asking for a good way of formalizing on Math SE. However, the purpose of this current question on cstheory was to get an answer/clarification of the confusion expressed in my previous comment (directly above this one).
Atriya
CC BY-SA 3.0
2014-07-28T15:50:53.963Z
Oops, I am confused, I though I was on Mathoverflow. Apologies! Stay right here :-)
Andrej Bauer
CC BY-SA 3.0
2014-07-28T15:54:19.357Z
True, NBG is likely to be better suited than ZFC, especially since in ZFC classes are not first-class objects. How does FOL prove properties of sets? From the axioms about sets, of course. I don't understand your question. In *every* formalization there are some things that are necessarily taken as primitive. FOL has exactly the same "problem" with natural numbers, where 0 and successor are "undefined".
Andrej Bauer
CC BY-SA 3.0
2014-07-28T16:28:31.943Z
I see. In that case, my impression that FOL needs to 'understand' membership to prove theorems about sets, was a misconception. If you took a human child and gave her a lot of axioms about sets, but never told her what a∈X means - what it means for something to be a member of a set - what are the chances that she would grow up to be a set theorist? However, that's probably irrelevant to formal ATP. There still remains the specific issue of why my theorem prover is unable to prove the theorems I pose to it - but I will ask that as a separate question, with implementation and code in detail.
Atriya
CC BY-SA 3.0
2014-07-28T16:32:19.913Z
Many mathematicians will say that set membership *is* a primitive concept which cannot be defined. How would *you* define set membership in a rigorous way? The point of the axiomatic method in mathematics is precisely that we do take certain concepts as primitive, describe them through axioms, and assume nothing further about them. In particular, the axioms are all there is to the concepts, on further "explanation" or "definition" is needed.
Andrej Bauer
CC BY-SA 3.0
2014-07-28T16:37:40.643Z
Euclid tried to "define" points as "that which has no part" and lines as "breadthless length". These definitions are much less clear than his axioms. Hilbert said that instead of points, lines and planes one might just as well talk of tables, chairs and beer mugs -- his point being that the primitive terms are just empty shells, place holders if you will, and have no intrinsic properties. In other words we *should not* try to define these. The same goes with the primitive concepts in any other theory.
Andrej Bauer
CC BY-SA 3.0
2014-07-28T17:02:59.450Z
That's certainly a forceful example (Euclid and Hilbert). In that case, the inability of my theorem prover (SNARK) could be one of the hit-and-miss scenarios you described earlier. I'll describe my axioms and proof goals in a separate question. Thanks again.
Atriya
CC BY-SA 3.0
2014-10-07T19:35:31.903Z
I'm unaware that NBG requires a primitive predicate outside of membership.
dezakin
CC BY-SA 3.0
2014-10-07T19:37:54.267Z
@dezakin: $S(x)$ means "$x$ is a set" (as opposed to its being a class). It can be defined as $\exists y . x \in y$, so it is largely a matter of choice how we set things up.
Andrej Bauer
CC BY-SA 3.0
2014-07-28T10:04:24.673Z
2014-07-28T10:04:24.673Z
Andrej Bauer
<p>I cannot comment so I'll try to give an answer:
from what I understand the OP is right: in most (all ?) FOL engine, you can of course add your own axioms but not your own axioms schemata (that is why you often hear that 'ATP cannot be applied to non finitely axiomatisable theories'). You can have a look at metamath, in which each theorem is in fact a theorem schemata (hence the 'meta' in 'metamath'), unfortunately I think there is only a proof checker for now.</p>

<p>It is the same for theorem provers, often you will read that 'resolution + factoring is complete for FOL', but if you have axioms schemata or even simply FOL with equality it is not true (for equality you need to add paramodulation to your resolution).</p>

CC BY-SA 4.0
2020-05-23T15:32:14.887Z
2020-05-23T15:57:58.230Z
2020-05-23T15:57:58.230Z
agemO
<p><strong>Abbreviations</strong> - <strong>FOL</strong> is first-order logic; <strong>NBG</strong> is Von Neumann–Bernays–Gödel set theory; <strong>SEP</strong> is Stanford Encyclopedia of Philosophy; <strong>HOL</strong> is higher-order logic; <strong>ATP</strong> is automated theorem proving.</p>

<p><strong>Context</strong> - An entire section of TPTP’s [1] axioms is devoted to set theories - for example NBG - for FOL theorem provers. Art Quaife wrote an entire book [2] on axiomatizing NBG in FOL.</p>

<p><strong>It seems to me</strong> - These axioms all take <strong>membership</strong> as a sort of undefined concept, and then build subsets, power sets, union, difference, and so on.</p>

<p>In contrast, here is what SEP has to say on HOL (emphasis mine) -</p>

<blockquote>
  <p><em>Second-order logic is an extension of first-order logic where, <strong>in addition to quantifiers such as “for every object (in the universe of
  discourse),” one has quantifiers such as “for every property of
  objects (in the universe of discourse).”</strong>   This augmentation of the
  language increases its expressive strength, without adding new
  non-logical symbols, such as new predicate symbols.   For classical
  extensional logic (as in this entry), <strong>properties can be identified
  with sets</strong>, so that second-order logic provides us with the
  quantifier <strong>“for every set of objects.”</em></strong></p>
</blockquote>

<p><strong>It seems to me</strong> - that the concept of membership can only be represented in HOL. If that is true, how can FOL axiom schemas, taking membership as an undefined concept, prove theorems in set theory?</p>

<p><strong>What I am trying to do</strong> - I need to do ATP in a theory which is FOL+sets. I was unsure whether to use an FOL prover (say, Prover9) or an HOL prover (say, HOL Light). At present, I’m using SNARK (FOL) with Quaife’s axiomatization of NBG, which is unable to prove my theorems (see below for example).</p>

<p><strong>Question</strong> - Is this failure to be expected, since FOL cannot ‘understand’ membership, and hence I need an HOL prover? Or am I misunderstanding / doing something wrong?</p>

<p>[1] The TPTP Problem Library for Automated Theorem Proving, <a href="http://www.cs.miami.edu/~tptp/" rel="nofollow">http://www.cs.miami.edu/~tptp/</a>
[2] Automated Development of Fundamental Mathematical Theories, by Art Quaife, Kluwer Acadamic Publishers (1992)</p>

<p><strong>Finally, an example</strong> -</p>

<p>Here is SNARK code representing three axioms, and a theorem, which SNARK is unable to prove. SNARK has also been given Quaife's axioms of NBG set theory. (Note <strong>member</strong>, the set membership function.) -</p>

<pre><code>(assert  '(forall (x y z)
    (implies
      (and
        (part-of x y)
        (part-of y z)
      )
      (part-of x z)   ) ) :name '1point1point1)

(assert  '(forall (x y alpha t)
    (exists (z arb-part)
      (implies
        (and
          (and
            (member t alpha)
            (part-of t x)
          )
          (implies
            (part-of y x)
            (and
              (member z alpha)
              (and
                (part-of arb-part z)
                (part-of arb-part y)
        ) ) ) )
        (sum-of x alpha)   ) ) ) :name '1point1point2)

(assert  '(forall (alpha)
    (exists (arb-member sum)
      (implies
        (member arb-member alpha)
        (sum-of sum alpha)
) ) ) :name '1point1point3)

(prove  '(forall (x)
    (part-of x x)   ) :name '1point1point4)
</code></pre>

<p>EDIT -</p>

<p>Jake said - "set theories are often defined in first order logic". In fact, the question I was asking was - "Can set theories be defined in first order logic, in an automated theorem prover?". That's what I meant, when I said "is set theory equivalent to first order logic?" (which is an incorrect way of putting it, and for which I apologize).</p>

<p>It turns out that ZFC <strong>cannot</strong> be represented in an FOL theorem prover, since it is not finitely axiomatizable. NBG and one other set theories can, and several such axiomatizations exist in TPTP.</p>

<p>However, these axiomatizations seem to take the concept of membership as undefined, and build subsets, power sets, etc on that. The SEP paragraph I quoted seems to suggest that representing membership needs HOL. In such a case, it seems paradoxical to me that FOL provers are expected to prove theorems in set theory, knowing nothing of membership.</p>

<p>I'm sure this is not a real paradox - just something I don't understand. Hence the question. I hope that makes it clearer.</p>

CC BY-SA 3.0
2014-07-28T04:12:15.343Z
This doesn't make sense. Set theory is not a logic. In fact set theories are often defined in first order logic. ZFC and NBG are both defined in FOL.
Jake
CC BY-SA 3.0
2014-07-28T09:52:19.643Z
Rather than closing down the question because it is asked in a technically strange way, how about we try to explain the differences? (In which case this is not research-level and should go to Math SE.)
Andrej Bauer
CC BY-SA 3.0
2014-07-28T09:54:03.417Z
LISP code will be ignored by mathematicians on this site. You should rewrite it in mathematical notation.
Andrej Bauer
CC BY-SA 3.0
2014-07-28T14:49:55.257Z
@Jake: Sorry about the technically strange way of phrasing, and thanks to Andrej Bauer for changing the title. People have likely been down-voting the question after reading just the title. :( I have edited the answer to reflect your comment. Please see the 'EDIT:' section.
Atriya
<lo.logic><automated-theorem-proving><set-theory>
Which formalism is best suited for automated theorem proving in set theory?
Atriya
# Which formalism is best suited for automated theorem proving in set theory?

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

Abbreviations - FOL is first-order logic; NBG is Von Neumann–Bernays–Gödel set theory; SEP is Stanford Encyclopedia of Philosophy; HOL is higher-order logic; ATP is automated theorem proving.
Context - An entire section of TPTP’s [1] axioms is devoted to set theories - for example NBG - for FOL theorem provers. Art Quaife wrote an entire book [2] on axiomatizing NBG in FOL.
It seems to me - These axioms all take membership as a sort of undefined concept, and then build subsets, power sets, union, difference, and so on.
In contrast, here is what SEP has to say on HOL (emphasis mine) -

Second-order logic is an extension of first-order logic where, in addition to quantifiers such as “for every object (in the universe of
  discourse),” one has quantifiers such as “for every property of
  objects (in the universe of discourse).”   This augmentation of the
  language increases its expressive strength, without adding new
  non-logical symbols, such as new predicate symbols.   For classical
  extensional logic (as in this entry), properties can be identified
  with sets, so that second-order logic provides us with the
  quantifier “for every set of objects.”

It seems to me - that the concept of membership can only be represented in HOL. If that is true, how can FOL axiom schemas, taking membership as an undefined concept, prove theorems in set theory?
What I am trying to do - I need to do ATP in a theory which is FOL+sets. I was unsure whether to use an FOL prover (say, Prover9) or an HOL prover (say, HOL Light). At present, I’m using SNARK (FOL) with Quaife’s axiomatization of NBG, which is unable to prove my theorems (see below for example).
Question - Is this failure to be expected, since FOL cannot ‘understand’ membership, and hence I need an HOL prover? Or am I misunderstanding / doing something wrong?
[1] The TPTP Problem Library for Automated Theorem Proving, http://www.cs.miami.edu/~tptp/
[2] Automated Development of Fundamental Mathematical Theories, by Art Quaife, Kluwer Acadamic Publishers (1992)
Finally, an example -
Here is SNARK code representing three axioms, and a theorem, which SNARK is unable to prove. SNARK has also been given Quaife's axioms of NBG set theory. (Note member, the set membership function.) -
(assert  '(forall (x y z)
    (implies
      (and
        (part-of x y)
        (part-of y z)
      )
      (part-of x z)   ) ) :name '1point1point1)

(assert  '(forall (x y alpha t)
    (exists (z arb-part)
      (implies
        (and
          (and
            (member t alpha)
            (part-of t x)
          )
          (implies
            (part-of y x)
            (and
              (member z alpha)
              (and
                (part-of arb-part z)
                (part-of arb-part y)
        ) ) ) )
        (sum-of x alpha)   ) ) ) :name '1point1point2)

(assert  '(forall (alpha)
    (exists (arb-member sum)
      (implies
        (member arb-member alpha)
        (sum-of sum alpha)
) ) ) :name '1point1point3)

(prove  '(forall (x)
    (part-of x x)   ) :name '1point1point4)

EDIT -
username_1 said - "set theories are often defined in first order logic". In fact, the question I was asking was - "Can set theories be defined in first order logic, in an automated theorem prover?". That's what I meant, when I said "is set theory equivalent to first order logic?" (which is an incorrect way of putting it, and for which I apologize).
It turns out that ZFC cannot be represented in an FOL theorem prover, since it is not finitely axiomatizable. NBG and one other set theories can, and several such axiomatizations exist in TPTP.
However, these axiomatizations seem to take the concept of membership as undefined, and build subsets, power sets, etc on that. The SEP paragraph I quoted seems to suggest that representing membership needs HOL. In such a case, it seems paradoxical to me that FOL provers are expected to prove theorems in set theory, knowing nothing of membership.
I'm sure this is not a real paradox - just something I don't understand. Hence the question. I hope that makes it clearer.

**Tags:** lo.logic, automated-theorem-proving, set-theory

> **Comments:**
> **username_1**: This doesn't make sense. Set theory is not a logic. In fact set theories are often defined in first order logic. ZFC and NBG are both defined in FOL.  
> **username_2**: Rather than closing down the question because it is asked in a technically strange way, how about we try to explain the differences? (In which case this is not research-level and should go to Math SE.)  
> **username_2**: LISP code will be ignored by mathematicians on this site. You should rewrite it in mathematical notation.  
> **username_0**: @username_1: Sorry about the technically strange way of phrasing, and thanks to username_2 for changing the title. People have likely been down-voting the question after reading just the title. :( I have edited the answer to reflect your comment. Please see the 'EDIT:' section.  

---

## 2 answers

### Answer by username_2 on 2014-07-28. Score: 6 | Accepted answer

There are numerous ways of formalizing set theory:

* ZFC uses first-order logic and a primitive relation $\in$
* NBG uses first-order logic, a primitive relation $\in$, and a primitive predicate $S$
* Church's type theory is multi-sorted and uses infintely many types
* Type theory is similar to set theory, but not quite the same
* Second-order arithmetic, through some coding tricks, can express many things we usually want to express in analysis
* etc.

But this is all quite irrelevant to what you are doing. You seem to be using automated theorem provers as "black boxes" to prove simple theorems in set theory. This is a hit-and-miss activity: some theorem provers will prove some simple things, and others will prove other simple things, but they will all fail on statements that mathematicians consider "completely trivial". Such is the state of automated theorem proving.

Rather than worrying which particular formalism you are using, you should investigate which automated theorem prover is good for what. It is also very likely that you do not actually need set theory. It would be helpful if you described what you're doing, but not here, this should go on [cstheory.stackexchange.com](http://cstheory.stackexchange.com). There perhaps we can suggest a good way of formalizing whatever you are doing.

> **Comments:**
> **username_0**: Thanks for replying. Firstly - you say that this question should go on cstheory.stackexchange.com. Isn't that exactly where I posted it? Did you mean Math SE?  
> **username_0**: Now - although set theory can be formalized in ZFC, from what I understand, this is not relevant to ATP, since the axiomatization is not finite. NBG, however, can be finitely axiomatized. However, as you state, it uses the primitive concepts ∈ and S. In Quaife's NBG axioms in FOL, there is no axiom which explains the 'meaning' of ∈ or S in FOL - indeed, as you state, these are to be taken as primitives, hence no such axiom is possible. My question was - with FOL thus unable to 'define' ∈ (apparently HOL can, from the SEP entry), how can set theory theorems be expected to be proved in FOL?  
> **username_0**: I asked this question as I am trying to do exactly that - prove set theory theorems in FOL with NBG axioms - with no success so far. Yes, I am using the ATP as a black box. I understand your comments about hit-and-miss, and I'll post a question asking for a good way of formalizing on Math SE. However, the purpose of this current question on cstheory was to get an answer/clarification of the confusion expressed in my previous comment (directly above this one).  
> **username_2**: Oops, I am confused, I though I was on Mathoverflow. Apologies! Stay right here :-)  
> **username_2**: True, NBG is likely to be better suited than ZFC, especially since in ZFC classes are not first-class objects. How does FOL prove properties of sets? From the axioms about sets, of course. I don't understand your question. In *every* formalization there are some things that are necessarily taken as primitive. FOL has exactly the same "problem" with natural numbers, where 0 and successor are "undefined".  
> **username_0**: I see. In that case, my impression that FOL needs to 'understand' membership to prove theorems about sets, was a misconception. If you took a human child and gave her a lot of axioms about sets, but never told her what a∈X means - what it means for something to be a member of a set - what are the chances that she would grow up to be a set theorist? However, that's probably irrelevant to formal ATP. There still remains the specific issue of why my theorem prover is unable to prove the theorems I pose to it - but I will ask that as a separate question, with implementation and code in detail.  
> **username_2**: Many mathematicians will say that set membership *is* a primitive concept which cannot be defined. How would *you* define set membership in a rigorous way? The point of the axiomatic method in mathematics is precisely that we do take certain concepts as primitive, describe them through axioms, and assume nothing further about them. In particular, the axioms are all there is to the concepts, on further "explanation" or "definition" is needed.  
> **username_2**: Euclid tried to "define" points as "that which has no part" and lines as "breadthless length". These definitions are much less clear than his axioms. Hilbert said that instead of points, lines and planes one might just as well talk of tables, chairs and beer mugs -- his point being that the primitive terms are just empty shells, place holders if you will, and have no intrinsic properties. In other words we *should not* try to define these. The same goes with the primitive concepts in any other theory.  
> **username_0**: That's certainly a forceful example (Euclid and Hilbert). In that case, the inability of my theorem prover (SNARK) could be one of the hit-and-miss scenarios you described earlier. I'll describe my axioms and proof goals in a separate question. Thanks again.  
> **username_3**: I'm unaware that NBG requires a primitive predicate outside of membership.  
> **username_2**: @username_3: $S(x)$ means "$x$ is a set" (as opposed to its being a class). It can be defined as $\exists y . x \in y$, so it is largely a matter of choice how we set things up.  

---

### Answer by username_4 on 2020-05-23. Score: 0

I cannot comment so I'll try to give an answer:
from what I understand the OP is right: in most (all ?) FOL engine, you can of course add your own axioms but not your own axioms schemata (that is why you often hear that 'ATP cannot be applied to non finitely axiomatisable theories'). You can have a look at metamath, in which each theorem is in fact a theorem schemata (hence the 'meta' in 'metamath'), unfortunately I think there is only a proof checker for now.

It is the same for theorem provers, often you will read that 'resolution + factoring is complete for FOL', but if you have axioms schemata or even simply FOL with equality it is not true (for equality you need to add paramodulation to your resolution).


---

