Editing Prenex normal form (section)

=== Intuitionistic logic ===

The rules for converting a formula to prenex form make heavy use of classical logic.  In [[intuitionistic logic]], it is not true that every formula is logically equivalent to a prenex formula.  The negation connective is one obstacle, but not the only one.  The implication operator is also treated differently in intuitionistic logic than classical logic; in intuitionistic logic, it is not definable using disjunction and negation.  

The [[BHK interpretation]] illustrates why some formulas have no intuitionistically-equivalent prenex form. In this interpretation, a proof of 
:<math>(\exists x \phi) \rightarrow \exists y \psi \qquad (1)</math>
is a function which, given a concrete ''x'' and a proof of <math>\phi (x)</math>, produces a concrete ''y'' and a proof of <math>\psi (y)</math>.  In this case it is allowable for the value of ''y'' to be computed from the given value of ''x''.  A proof of 
:<math>\exists y ( \exists x \phi \rightarrow \psi), \qquad  (2)</math>
on the other hand, produces a single concrete value of ''y'' and a function that converts any proof of <math>\exists x \phi</math> into a proof of <math>\psi (y)</math>.   If each ''x''  satisfying <math>\phi</math> can be used to construct a ''y'' satisfying <math>\psi</math> but no such ''y'' can be constructed without knowledge of such an ''x'' then formula (1) will not be equivalent to formula (2).

The rules for converting a formula to prenex form that do ''fail'' in intuitionistic logic are:
:(1) <math>\forall x (\phi \lor \psi)</math> implies <math>(\forall x \phi) \lor \psi</math>,
:(2) <math>\forall x (\phi \lor \psi)</math> implies <math>\phi \lor (\forall x \psi)</math>,
:(3) <math>(\forall x \phi) \rightarrow \psi</math> implies <math>\exists x (\phi \rightarrow \psi)</math>,
:(4) <math>\phi \rightarrow (\exists x \psi)</math> implies <math>\exists x (\phi \rightarrow \psi)</math>,
:(5) <math>\lnot \forall x \phi</math> implies <math>\exists x \lnot \phi</math>,
(''x'' does not appear as a free variable of <math>\,\psi</math> in (1) and (3); ''x'' does not appear as a free variable of <math>\,\phi</math> in (2) and (4)).