| Description: Define the equality
connective between classes. Definition 2.7
of [Quine] p. 18. Also Definition 4.5 of
[TakeutiZaring] p. 13;
Chapter 4 provides its justification and methods for
eliminating it. Note that its elimination will not necessarily result
in a single wff in the original language but possibly a
"scheme" of
wffs. This is an example of a somewhat "risky" definition,
because
it extends the use of the existing equality symbol rather than
introducing a new symbol, allowing us to make statements in the original
language that may not be true. For example, it permits us to deduce
y = z ↔ ∀x(x ∈
y ↔ x ∈ z)
which is not a theorem of
logic but rather presupposes the Axiom of Extensionality, which we
must therefore include as a hypothesis. We could avoid the danger
by introducing another symbol, say == , in place of =; this would
also have the advantage of making elimination of the definition
straightforward, so that we could eliminate Extensionality as a
hypothesis. We would then also have the advantage of being able to
identify in various proofs exactly where Extensionality truly comes into
play. Then, one of our theorems would then be x == y ↔
x = y
by invoking Extensionality. However in keeping with standard practice
we retain the "dangerous" definition; this also makes some
proofs
shorter. See also comments under df-clab 1093, df-clel 1099, and
cleqab 1174. |
Home