ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax-ext GIF version

Axiom ax-ext 2099
Description: Axiom of Extensionality. It states that two sets are identical if they contain the same elements. Axiom 1 of [Crosilla] p. "Axioms of CZF and IZF" (with unnecessary quantifiers removed).

Set theory can also be formulated with a single primitive predicate on top of traditional predicate calculus without equality. In that case the Axiom of Extensionality becomes (∀𝑤(𝑤𝑥𝑤𝑦) → (𝑥𝑧𝑦𝑧)), and equality 𝑥 = 𝑦 is defined as 𝑤(𝑤𝑥𝑤𝑦). All 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 with Metamath's logical axioms, we would rewrite ax-8 1467 through ax-16 1770 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.

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. For example, the metavariable 𝑥 in ax-ext 2099 can represent any actual variable v1, v2, v3,... . Distinct variable restrictions ($d) prevent us from substituting say v1 for both 𝑥 and 𝑧. This is in contrast to typical textbook presentations that present actual axioms (except for axioms which involve wff metavariables). 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 2099 scheme exactly logically equivalent to each other and in particular to the actual axiom of the textbook version. (Contributed by NM, 5-Aug-1993.)

Assertion
Ref Expression
ax-ext (∀𝑧(𝑧𝑥𝑧𝑦) → 𝑥 = 𝑦)
Distinct variable group:   𝑥,𝑦,𝑧

Detailed syntax breakdown of Axiom ax-ext
StepHypRef Expression
1 vz . . . . 5 setvar 𝑧
2 vx . . . . 5 setvar 𝑥
31, 2wel 1466 . . . 4 wff 𝑧𝑥
4 vy . . . . 5 setvar 𝑦
51, 4wel 1466 . . . 4 wff 𝑧𝑦
63, 5wb 104 . . 3 wff (𝑧𝑥𝑧𝑦)
76, 1wal 1314 . 2 wff 𝑧(𝑧𝑥𝑧𝑦)
82, 4weq 1464 . 2 wff 𝑥 = 𝑦
97, 8wi 4 1 wff (∀𝑧(𝑧𝑥𝑧𝑦) → 𝑥 = 𝑦)
Colors of variables: wff set class
This axiom is referenced by:  axext3  2100  bm1.1  2102  dfcleq  2111  a9evsep  4020
  Copyright terms: Public domain W3C validator