**Description: **Axiom ax-11o 1654 ("o" for "old") was the
original version of ax-11 1389,
before it was discovered (in Jan. 2007) that the shorter ax-11 1389 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."
This axiom is redundant, as shown by theorem ax11o 1653.
Normally, ax11o 1653 should be used rather than ax-11o 1654, except by theorems
specifically studying the latter's properties. |