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 34977 about the logical redundancy of ax-5 2009
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 2224, we
can also remove the quantifier (unconditionally). (Contributed by NM,
10-Jan-1993.) |