|Description: Axiom of Variable
Substitution. One of the 5 equality axioms of predicate
calculus. The final consequent
is a way of
substituted for in wff
" (cf. sb6 1993).
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 1941 ("o" for "old") and was
replaced with this shorter ax-11 1624 in Jan. 2007. The old axiom is
from this one as theorem ax11o 1940. Conversely, this axiom is proved from
ax-11o 1941 as theorem ax11 1942.
Juha Arpiainen proved the independence of this axiom (in the form of the
older axiom ax-11o 1941) from the others on 19-Jan-2006. See item 9a
Interestingly, if the wff expression substituted for contains no
wff variables, the resulting statement can be proved without
this axiom. This means that even though this axiom is
independent from the others, it is not logically independent.
Specifically, we can prove any wff-variable-free instance of axiom
ax-11o 1941 (from which the ax-11 1624 instance follows by theorem ax11 1942.)
The proof is by induction on formula length, using ax11eq 2108 and ax11el 2109
for the basis steps and ax11indn 2111, ax11indi 2112, and ax11inda 2116 for the
induction steps. (This paragraph is true provided we use ax-10o 1836 in
place of ax-10 1678.)
See also ax11v 1991 and ax11v2 1936 for other equivalents of this axiom that
(unlike this axiom) have distinct variable restrictions. (Contributed by