| 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
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.
We prove in ax8 2112 that this axiom can be recovered from its
weakened
version ax8v 2109 where 𝑥 and 𝑦 are assumed to be
disjoint variables.
In particular, the only theorem referencing ax-8 2108
should be ax8v 2109. See
the comment of ax8v 2109 for more details on these matters.
(Contributed by
NM, 30-Jun-1993.) (Revised by BJ, 7-Dec-2020.) Use ax8 2112
instead.
(New usage is discouraged.) |
