| Description: Axiom of Equality. One
of the equality and substitution axioms of
predicate calculus with equality. It states that equality is a
right-Euclidean binary relation (this is similar, but not identical, to
being transitive, which is proved as equtr 2029). This axiom scheme is a
sub-scheme of Axiom Scheme B8 of system S2 of [Tarski], p. 75, whose
general form cannot be represented with our notation. Also appears as
Axiom C7 of [Monk2] p. 105 and Axiom Scheme
C8' in [Megill] p. 448 (p. 16
of the preprint).
The equality symbol was invented in 1557 by Robert Recorde. He chose a
pair of parallel lines of the same length because "noe .2. thynges,
can be
moare equalle".
We prove in ax7 2024 that this axiom can be recovered from its
weakened
version ax7v 2017 where 𝑥 and 𝑦 are assumed to be
disjoint variables.
In particular, the only theorem referencing ax-7 2016
should be ax7v 2017. See
the comment of ax7v 2017 for more details on these matters.
(Contributed by
NM, 10-Jan-1993.) (Revised by BJ, 7-Dec-2020.) Use ax7 2024
instead.
(New usage is discouraged.) |
