|Description: Axiom of Extensionality.
An axiom of Zermelo-Fraenkel set theory. It
states that two sets are identical if they contain the same elements.
Axiom Ext of [BellMachover] p.
Set theory can also be formulated with a single primitive
on top of
traditional predicate calculus without equality. In
that case the Axiom of Extensionality becomes
equality is defined as
of the usual axioms of equality then become theorems of set theory.
See, for example, Axiom 1 of [TakeutiZaring] p. 8.
To use the above "equality-free" version of Extensionality
Metamath's logical axioms, we would rewrite ax-8 1687
through ax-16 2220 with
equality expanded according to the above definition. Some of those
axioms could be proved from set theory and would be redundant. Not all
of them are redundant, since our axioms of predicate calculus make
essential use of equality for the proper substitution that is a
primitive notion in traditional predicate calculus. A study of such an
axiomatization would be an interesting project for someone exploring the
foundations of logic.
General remarks: Our set theory axioms are presented using
connectives (, , etc.) for convenience. However, it is
implicitly understood that the actual axioms use only the primitive
connectives , ,
, , and . It is
straightforward to establish the equivalence between the actual axioms
and the ones we display, and we will not do so.
It is important to understand that strictly speaking, all of our set
theory axioms are really schemes that represent an infinite number of
actual axioms. This is inherent in the design of Metamath
("metavariable math"), which manipulates only metavariables.
example, the metavariable in ax-ext 2416 can represent any actual
variable v1, v2, v3,... . Distinct variable
prevent us from substituting say v1 for both and . This
is in contrast to typical textbook presentations that present actual
axioms (except for Replacement ax-rep 4312, which involves a wff
metavariable). In practice, though, the theorems and proofs are
essentially the same. The $d restrictions make each of the infinite
axioms generated by the ax-ext 2416 scheme exactly logically equivalent
each other and in particular to the actual axiom of the textbook
version. (Contributed by NM, 5-Aug-1993.)