**Description: **Axiom of Quantified
Negation. Axiom C5-2 of [Monk2] p. 113. This
axiom
scheme is logically redundant (see ax10w 2129) 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 2142 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 2141 through ax-13 2371,
by invoking ax10w 2129 through ax13w 2136. We encourage proving theorems
*without* ax-10 2141 through ax-13 2371 and moving them up to the ax-4 1817
through
ax-9 2120 section. (New usage is
discouraged.) |