**Description: **Axiom of Variable
Substitution. One of the 5 equality axioms of predicate
calculus. The final consequent is a way of
expressing "
substituted for in
wff " (cf.
sb6 1705). It
is based on Lemma 16 of [Tarski] p. 70 and
Axiom C8 of [Monk2] p. 105,
from which it can be proved by cases.
The original version of this axiom was ax-11o 1654 ("o" for "old") and was
replaced with this shorter ax-11 1389 in Jan. 2007. The old axiom is
proved
from this one as theorem ax11o 1653. Conversely, this axiom is proved from
ax-11o 1654 as theorem ax11 1655.
Juha Arpiainen proved the independence of this axiom (in the form of the
older axiom ax-11o 1654) from the others on 19-Jan-2006. See item 9a
at
http://us.metamath.org/award2003.html.
Interestingly, if the wff expression substituted for contains no
wff variables, the resulting statement *can* be proved without
invoking
this axiom. This means that even though this axiom is
*metalogically*
independent from the others, it is not *logically* independent.
Specifically, we can prove any wff-variable-free instance of axiom
ax-11o 1654 (from which the ax-11 1389 instance follows by theorem ax11 1655.)
The proof is by induction on formula length, using ax11eq 1810 and ax11el 1811
for the basis steps and ax11indn 1813, ax11indi 1814, and ax11inda 1818 for the
induction steps.
See also ax11v 1703 and ax11v2 1651 for other equivalents of this axiom that
(unlike this axiom) have distinct variable
restrictions. |