|Description: Axiom of Distinct
Variables. The only axiom of predicate calculus
requiring that variables be distinct (if we consider ax-5 1709
to be a
metatheorem and not an axiom). Axiom scheme C16' in [Megill] p. 448 (p.
16 of the preprint). It apparently does not otherwise appear in the
literature but is easily proved from textbook predicate calculus by
cases. It is a somewhat bizarre axiom since the antecedent is always
false in set theory (see dtru 4628), but nonetheless it is technically
necessary as you can see from its uses.
This axiom is redundant if we include ax-5 1709;
see theorem axc16 1946.
Alternately, ax-5 1709 becomes logically redundant in the presence
axiom, but without ax-5 1709 we lose the more powerful metalogic that
results from being able to express the concept of a setvar variable not
occurring in a wff (as opposed to just two setvar variables being
distinct). We retain ax-c16 2225 here to provide logical completeness
systems with the simpler metalogic that results from omitting ax-5 1709,
which might be easier to study for some theoretical purposes.
This axiom is obsolete and should no longer be used. It is proved above
as theorem axc16 1946. (Contributed by NM, 10-Jan-1993.)
(New usage is discouraged.)