| Description: Axiom B7 of [Tarski] p. 75, which requires that 𝑥 and
𝑦
be
distinct. This trivial proof is intended merely to weaken Axiom ax-6 1972
by adding a distinct variable restriction ($d). From here on, ax-6 1972
should not be referenced directly by any other proof, so that Theorem
ax6 2384 will show that we can recover ax-6 1972
from this weaker version if
it were an axiom (as it is in the case of Tarski).
Note: Introducing 𝑥, 𝑦 as a distinct variable group
"out of the
blue" with no apparent justification has puzzled some people, but
it is
perfectly sound. All we are doing is adding an additional prerequisite,
similar to adding an unnecessary logical hypothesis, that results in a
weakening of the theorem. This means that any future theorem
that
references ax6v 1973 must have a $d specified for the two
variables that
get substituted for 𝑥 and 𝑦. The $d does not
propagate
"backwards", i.e., it does not impose a requirement on ax-6 1972.
When possible, use of this theorem rather than ax6 2384 is
preferred since
its derivation is much shorter and requires fewer axioms. (Contributed
by NM, 7-Aug-2015.) |
