# Which formalism is best suited for automated theorem proving in set theory?

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  axioms is devoted to set theories - for example NBG - for FOL theorem provers. Art Quaife wrote an entire book  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?

 The TPTP Problem Library for Automated Theorem Proving, http://www.cs.miami.edu/~tptp/  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 -

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

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.

• 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 Jul 28 '14 at 4:12
• 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 Jul 28 '14 at 9:52
• LISP code will be ignored by mathematicians on this site. You should rewrite it in mathematical notation. – Andrej Bauer Jul 28 '14 at 9:54
• @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 Jul 28 '14 at 14:49

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. There perhaps we can suggest a good way of formalizing whatever you are doing.

• 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 Jul 28 '14 at 15:11
• 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 Jul 28 '14 at 15:45
• 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 Jul 28 '14 at 15:48
• Oops, I am confused, I though I was on Mathoverflow. Apologies! Stay right here :-) – Andrej Bauer Jul 28 '14 at 15:50
• 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 Jul 28 '14 at 16:37