Description: Axiom of Distinctness.
This axiom quantifies a variable over a formula
in which it does not occur. Axiom C5 in [Megill] p. 444 (p. 11 of the
preprint). Also appears as Axiom B6 (p. 75) of system S2 of [Tarski]
p. 77 and Axiom C5-1 of [Monk2] p. 113.
(See comments in ax5ALT 34192 about the logical redundancy of ax-5 1839
in the
presence of our obsolete axioms.)
This axiom essentially says that if does not occur in ,
i.e.
does not depend on in
any way, then we can add the
quantifier to with no further
assumptions. By sp 2053, we
can also remove the quantifier (unconditionally). (Contributed by NM,
10-Jan-1993.) |