|Description: Axiom of Quantifier
Introduction. One of the equality and substitution
axioms for a non-logical predicate in our predicate calculus with
equality. Axiom scheme C14' in [Megill]
p. 448 (p. 16 of the preprint).
It is redundant if we include ax-17 1628; see theorem ax15 2101.
ax-17 1628 becomes unnecessary in principle with this
axiom, but we lose the
more powerful metalogic afforded by ax-17 1628. We retain ax-15 2102 here to
provide completeness for systems with the simpler metalogic that results
from omitting ax-17 1628, which might be easier to study for some
theoretical purposes. (Contributed by NM, 5-Aug-1993.)
(New usage is discouraged.)|