Description: Axiom of left equality
for the binary predicate  . One of the
equality and substitution axioms for a non-logical predicate in our
predicate calculus with equality. It substitutes equal variables into the
left-hand side of the binary predicate. Axiom scheme C12' in
[Megill] p. 448 (p. 16 of the preprint).
It is a special case of Axiom B8
(p. 75) of system S2 of [Tarski] p. 77.
"Non-logical" means that the
predicate is not a primitive of predicate calculus proper but instead is
an extension to it. "Binary" means that the predicate has two
arguments.
In a system of predicate calculus with equality, like ours, equality is
not usually considered to be a non-logical predicate. In systems of
predicate calculus without equality, it typically would be. (Contributed
by NM, 5-Aug-1993.) |
