| Description: Axiom of Equality. One
of the equality and substitution axioms of
predicate calculus with equality. It states that equality is
right-Euclidean (this is similar, but not identical, to being transitive,
which is proved as equtr 1876). 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 1527 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 1871 that this axiom can be recovered from its
weakened
version ax7v 1863 where  and 
are assumed to be disjoint
variables. In particular, the only theorem referencing ax-7 1862
should be
ax7v 1863. See the comment of ax7v 1863
for more details on these matters.
(Contributed by NM, 10-Jan-1993.) (Revised by BJ, 7-Dec-2020.) Use ax7 1871
instead. (New usage is discouraged.) |
