| Description: Axiom of Quantified
Negation. Axiom C5-2 of [Monk2] p. 113. This
axiom
scheme is logically redundant (see ax10w 1953) but is used as an auxiliary
axiom scheme to achieve metalogical completeness. It means that 𝑥 is
not free in ¬ ∀𝑥𝜑. (Contributed by NM, 21-May-2008.)
Use its
alias hbn1 1966 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 1965 through
ax-13 2137, by invoking ax10w 1953 through ax13w 1960. We encourage proving
theorems *without* ax-10 1965 through ax-13 2137 and moving them up to the
ax-4 1711 through ax-9 1946
section. (New usage is discouraged.) |
