**Description: **Axiom of Quantified
Negation. Axiom C5-2 of [Monk2] p. 113. This
axiom
scheme is logically redundant (see ax10w 2003) but is used as an auxiliary
axiom scheme to achieve scheme completeness. It means that 𝑥 is not
free in ¬ ∀𝑥𝜑. (Contributed by NM, 21-May-2008.)
Use its alias
hbn1 2017 instead if you must use it. Any theorem in
first order logic (FOL)
that contains only set variables that are all mutually distinct, and has
no wff variables, can be proved *without* using ax-10 2016 through ax-13 2245,
by invoking ax10w 2003 through ax13w 2010. We encourage proving theorems
*without* ax-10 2016 through ax-13 2245 and moving them up to the ax-4 1734
through
ax-9 1996 section. (New usage is
discouraged.) |