|Description: Axiom of Left Equality
for 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
an arbitrary binary predicate ∈, which we
will use for the set
membership relation when set theory is introduced. 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 scheme C12' in [Megill] p. 448 (p.
16 of the preprint).
"Non-logical" means that the predicate is not a primitive of
calculus proper but instead is an extension to it. "Binary"
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.
We prove in ax8 2133 that this axiom can be recovered from its
version ax8v 2130 where 𝑥 and 𝑦 are assumed to be
In particular, the only theorem referencing ax-8 2129
should be ax8v 2130. See
the comment of ax8v 2130 for more details on these matters.
NM, 30-Jun-1993.) (Revised by BJ, 7-Dec-2020.) Use ax8 2133
(New usage is discouraged.)