Editing Prenex normal form (section)

=== Implication ===

There are four rules for [[material conditional|implication]]: two that remove quantifiers from the antecedent and two that remove quantifiers from the consequent. These rules can be derived by [[Rewriting#Logic|rewriting]] the implication
<math>\phi \rightarrow \psi</math> as <math>\lnot \phi \lor \psi</math> and applying the rules for disjunction and negation above.  As with the rules for disjunction, these rules require that the variable quantified in one subformula does not appear free in the other subformula. 

The rules for removing quantifiers from the antecedent are (note the change of quantifiers):
:<math>(\forall x \phi ) \rightarrow \psi</math> is equivalent to <math>\exists x (\phi \rightarrow \psi)</math> (under the assumption that <math>\exists x \top</math>),
:<math>(\exists x \phi ) \rightarrow \psi</math> is equivalent to <math>\forall x (\phi \rightarrow \psi)</math>.
The rules for removing quantifiers from the consequent are:
:<math>\phi \rightarrow (\exists x \psi)</math> is equivalent to <math>\exists x (\phi \rightarrow \psi)</math> (under the assumption that <math>\exists x \top</math>),
:<math>\phi \rightarrow (\forall x \psi)</math> is equivalent to <math>\forall x (\phi \rightarrow \psi)</math>.
For example, when the [[range of quantification]] is the non-negative [[natural number]] (viz. <math>n\in \mathbb{N}</math>), the statement
:<math>[\forall n\in \mathbb{N} (x< n) ] \rightarrow (x< 0)</math>
is [[logically equivalent]] to the statement
:<math>\exists n\in \mathbb{N}[ (x< n)  \rightarrow (x< 0)]</math>
The former statement says that if ''x'' is less than any natural number, then ''x'' is less than zero. The latter statement says that there exists some natural number ''n'' such that if ''x'' is less than ''n'', then ''x'' is less than zero. Both statements are true. The former statement is true because if ''x'' is less than any natural number, it must be less than the smallest natural number (zero). The latter statement is true because ''n=0'' makes the implication a [[Tautology (logic)|tautology]].

Note that the placement of brackets implies the [[Scope (logic)|scope of the quantification]], which is very important for the meaning of the formula. Consider the following two statements:
:<math>\forall n\in \mathbb{N} [(x< n) \rightarrow (x< 0)]</math>
and its [[logically equivalent]] statement
:<math>[\exists n\in \mathbb{N} (x< n) ] \rightarrow (x< 0)</math>
The former statement says that for any natural number ''n'', if ''x'' is less than ''n'' then ''x'' is less than zero. The latter statement says that if there exists some natural number ''n'' such that ''x'' is less than ''n'', then ''x'' is less than zero. Both statements are false. The former statement doesn't hold for ''n=2'', because ''x=1'' is less than ''n'', but not less than zero. The latter statement doesn't hold for ''x=1'', because the natural number ''n=2'' satisfies ''x<n'', but ''x=1'' is not less than zero.