**Description: **Axiom ax-11o 2217 ("o" for "old") was the
original version of ax-11 1761,
before it was discovered (in Jan. 2007) that the shorter ax-11 1761 could
replace it. It appears as Axiom scheme C15' in [Megill] p. 448 (p. 16 of
the preprint). 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. To understand this
theorem more easily, think of " ..." as informally
meaning "if
and are distinct
variables then..." The
antecedent becomes false if the same variable is substituted for and
, ensuring the
theorem is sound whenever this is the case. In some
later theorems, we call an antecedent of the form a
"distinctor."
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 2217 (from which the ax-11 1761 instance follows by theorem ax11 2231.)
The proof is by induction on formula length, using ax11eq 2269 and ax11el 2270
for the basis steps and ax11indn 2271, ax11indi 2272, and ax11inda 2276 for the
induction steps. (This paragraph is true provided we use ax-10o 2215 in
place of ax-10 2216.)
This axiom is obsolete and should no longer be used. It is proved above
as theorem ax11o 2077. (Contributed by NM, 5-Aug-1993.)
(New usage is discouraged.) |