**Description: **Axiom of Quantifier
Introduction. One of the equality and substitution
axioms of predicate calculus with equality. Informally, it says that
whenever is
distinct from and
, and
is true,
then quantified with is also true. In other words,
is irrelevant to the truth of
. Axiom scheme C9' 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.
An open problem is whether this axiom is redundant. Note that the
analogous axiom for the membership connective, ax-15 1807, has been shown to
be redundant. It is also unknown whether this axiom can be replaced by a
shorter formula. However, it can be derived from two slightly shorter
formulas, as shown by a12study 1825.
This axiom has been modified from the original ax-12 1393 for compatibility
with intuitionistic logic. |