`variable`

is a variable, which represents a set and can be quantified over, and `object`

is an expression which represents a set. For example, a variable might be `x`

, `y`

, or `z`

, but an object could be the singleton `{ x }`

, the unordered pair `{ x, y }`

, the ordered pair `〈 x, y 〉`

, the union `x ∪ y`

, etc. To some extent the concepts of variable and object correspond to set and class in some theories (like metamath's set.mm), but one key difference is that we have no [[w:proper class|proper classes]] thanks to the [[Interface:Axiom of quantifiability|axiom of quantifiability]].
#
var (object x y z w)
tvar (object s t u)
tvar (formula φ)
#
# We define one key predicate. The formula `A ∈ B`

means "A is an element of B".
#
term (formula (∈ s t))
#
# Our first axiom, the axiom of extensionality, states that if two sets have the same elements, they are equal. In symbols this is `∀ z (z ∈ x ↔ z ∈ y) → x = y`

. Versions with fewer distinct variable constaints also hold, but they can be proved from this version and other axioms, so we assume the weakest version (the one with the most distinct variable constraints).
#
stmt (ExtensionalityVariable () () (→ (∀ z (↔ (∈ z x) (∈ z y))) (= x y)))
#
# The principle that equals can be substituted for equals in JHilbert must be adopted as an axiom for each non-logical predicate (in this case ∈), which we do now.They are variants of [http://us.metamath.org/mpeuni/ax-13.html ax-13] and [http://us.metamath.org/mpeuni/ax-14.html ax-14] in metamath's set.mm, accessed July 21, 2010. The minor change is to biconditionalize them, but the major one is to make them apply for object, not just variable.
#
tvar (object A B A0 A1 B0 B1)
stmt (MembershipBuilderLL () () (→ (= B0 B1) (↔ (∈ A B0) (∈ A B1))))
stmt (MembershipBuilderRR () () (→ (= A0 A1) (↔ (∈ A0 B) (∈ A1 B))))
#
# The axiom of separation is `∃ y ∀ x (x ∈ y ↔ x ∈ z ∧ φ)`

. Given a set `z`

and a formula `φ`

this asserts the existence of a set `y`

which contains the elements of `z`

which satisfy `φ`

. The distinct variable constraint between `φ`

and `y`

is needed and is part of textbook statements of this axiom. Most of the other distinct variable constraints are implicit in the notation in many textbooks, and not all of them are necessary, but as with extensionality we include them.[http://us.metamath.org/mpeuni/ax-sep.html ax-sep], metamath's set.mm, accessed September 13, 2010
#
# TODO: Prove this from the axiom of replacement and then we won't need it as an axiom here.
stmt (SeparationThereExists ( (φ y z)) () (∃ y (∀ x (↔ (∈ x y) (∧ (∈ x z) φ)))))
#
# Axiom of replacement. Metamath has a number of variants of this axiom, but at least for now we choose this one, which has an odd feature of the apparently pointless `∀ y`

(whose function is in fact to reduce the number of distinct variable constraints needed).[http://us.metamath.org/mpeuni/ax-rep.html ax-rep], metamath's set.mm, accessed September 13, 2010
stmt (Replacement () () (→ (∀ w (∃ y (∀ z (→ (∀ y φ) (= z y))))) (∃ y (∀ z (↔ (∈ z y) (∃ w (∧ (∈ w x) (∀ y φ))))))))
#
# Axiom of pairing. There exists a set whose elements are two given sets. Although pairing can be proved by applying the axiom of replacement to any set with two elements (the existence of which can be proved using the power set axiom), for now we omit that proof by assuming pairing as an axiom. Some formulations, such as the one in metamath, merely assert the existence of a set containing the pair, not the pair itself.[http://us.metamath.org/mpeuni/ax-pr.html ax-pr], metamath's set.mm
stmt (Pairing ( ) () (∃ z (∀ w (↔ (∈ w z) (∨ (= w x) (= w y))))))
#
# Axiom of power sets. As with pairing, the metamath version asserts a set which contains the power set but we assert the power set itself.[http://us.metamath.org/mpeuni/ax-pow.html ax-pow], metamath's set.mm, accessed September 13, 2010
stmt (PowerSetAxiom () () (∃ y (∀ z (↔ (∈ z y) (∀ w (→ (∈ w z) (∈ w x)))))))
#
# Axiom of union. As with pairing, the metamath version asserts a set which contains the union but we assert the union itself.[http://us.metamath.org/mpeuni/ax-un.html ax-un], metamath's set.mm, accessed September 13, 2010
stmt (UnionAxiom () () (∃ y (∀ z (↔ (∈ z y) (∃ w (∧ (∈ z w) (∈ w x)))))))
#
# Axiom of regularity.[http://us.metamath.org/mpeuni/ax-reg.html ax-reg], metamath's set.mm, accessed September 13, 2010
stmt (Regularity () () (→ (∃ y (∈ y x)) (∃ y (∧ (∈ y x) (∀ z (→ (∈ z y) (¬ (∈ z x))))))))
#
# Axiom of infinity.[http://us.metamath.org/mpeuni/ax-inf.html ax-inf], metamath's set.mm, accessed September 13, 2010
stmt (Infinity () () (∃ y (∧ (∈ x y) (∀ z (→ (∈ z y) (∃ w (∧ (∈ z w) (∈ w y))))))))
#
# ==Defining sets==
# What we have presented so far provides the ideas of set theory, but there is one important notational detail to attend to. The above axioms let us conclude that there is a set with no elements, or a set whose only element is a set `x`

, but they do not provide any way to introduce notation such as `∅`

or `{ x }`

for those concepts.
#
# We want to define `{ y | φ }`

(the set of all `y`

for which `φ`

holds), of kind `object`

, but we need to tread carefully to avoid [[w:Russell's paradox|Russell's paradox]] and related problems. Metamath's set.mm uses the definition `x ∈ { y | φ } ↔ [ x / y ] φ`

,[http://us.metamath.org/mpeuni/df-clab.html df-clab], metamath's set.mm, accessed 2009 which allows `{ y | φ }`

to be a proper class rather than a set. As long as we assume the [[Interface:Axiom of quantifiability|axiom of quantifiability]], this avenue is not open to us. Instead, we provide a version of the metamath definition which has a hypothesis stating that the resulting set exists. This closely parallels the idiom of proving that something exists, and only then introducing a notation for it.
#
# The syntax `{ y | φ }`

is not available in JHilbert, so we will write it as `(abstract y φ)`

.
term (object (abstract x φ))
#
# Our restricted version of the metamath definition follows. The hypothesis is `∃ result ∀ x (x ∈ result ↔ [x / y]φ)`

, which can be paraphrased as "`{ y | φ }`

is a set". We adopt an axiom that this hypothesis lets us conclude `x ∈ { y | φ } ↔ [x / y]φ`

. All variables are distinct except that `y`

can (and typically does) appear in `φ`

.
var (object result)
stmt (Abstraction ((φ x result))
((∃ result (∀ x (↔ (∈ x result) (subst x y φ)))))
(↔ (∈ x (abstract y φ)) (subst x y φ)))
#
# ==References==
#