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.