**Description: **Axiom B7 of [Tarski] p. 75, which requires that 𝑥 and
𝑦
be
distinct. This trivial proof is intended merely to weaken axiom ax-6 1836
by adding a distinct variable restriction. From here on, ax-6 1836
should
not be referenced directly by any other proof, so that theorem ax6 2142
will show that we can recover ax-6 1836 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 redundant
requirement, no different from adding a redundant logical hypothesis,
that results in a weakening of the theorem. This means that any
*future* theorem that references ax6v 1837
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 1836.
When possible, use of this theorem rather than ax6 2142 is
preferred since
its derivation is much shorter and requires fewer axioms. (Contributed
by NM, 7-Aug-2015.) |