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

Question

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 -

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.

Answer 1

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.

Answer 2

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