**Description: **Axiom of Variable
Substitution. One of the 5 equality axioms of predicate
calculus. The final consequent ∀*x*(*x* = *y* →
*φ*) is a way of
expressing "*y*
substituted for *x* in wff
*φ* " (cf. sb6 1637).
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.
In classical logic, ax-11o 1579 can be derived from this axiom, as can be
seen at ax11o 1578. However, the current proof of ax11o 1578 is not valid
intuitionistically.
In classical logic, this axiom is *metalogically* independent from
the
others, but not *logically* independent. Lack of logical
independence
means that if the wff expression substituted for *φ* contains no wff
variables, the resulting statement *can* be proved without invoking
this
axiom. The current proofs of this are not valid in intuitionistic logic,
however. Specifically, we can prove any wff-variable-free instance of
axiom ax-11o 1579 (from which the ax-11 1330 instance follows by theorem
ax11 1918.) The proof is by induction on formula
length, using ax11eq 1920 and
ax11el 1921 for the basis steps and ax11indn 1922, ax11indi 1923, and ax11inda 1927
for the induction steps. Many of those theorems rely on classical logic
for their proofs.
Variants of this axiom which are equivalent in classical logic but which
have not been shown to be equivalent for intuitionistic logic are
ax11v 1583, ax11v2 1576 and ax-11o 1579. (Contributed by NM,
5-Aug-1993.) |