Prenex form

The prenex form is a possible normal form in which statements of the predicate logic can be represented. It is required , among other things, as a preliminary stage to the Skolem form .

A statement in first-level predicate logic is in prenex form if all quantifiers (descriptions of the scope) are outside or in front of the actual formula. If the prenex form also only contains conjunction , disjunction and negation (immediately before atoms) as joiners , it is also referred to as the normal form in terms of negation .

In classical predicate logic there is a logically equivalent formula in prenex form for every formula . This is not necessarily the case in intuitionist logic .

A formula in adjusted prenex form can be fulfilled if its scolemic form can be fulfilled.

Mathematical definition

A formula of predicate logic is in prenex form if it is of the form ${\displaystyle F}$

${\displaystyle F=Q_{1}y_{1}Q_{2}y_{2}\dots Q_{k}y_{k}{\hat {F}}}$

is with

${\displaystyle k\geq 0}$ and

${\displaystyle Q_{1},\dots ,Q_{k}\in \left\{\forall ,\exists \right\}}$.

In no must quantifier occur. ${\displaystyle {\hat {F}}}$

${\displaystyle Q_{1}y_{1}Q_{2}y_{2}\dots Q_{k}y_{k}}$means prefix, is the matrix . ${\displaystyle {\hat {F}}}$

Ambiguity

The prenex form is not clear. So has the formula

${\displaystyle \forall xp(x)\rightarrow \forall yq(y)}$

the two prenex forms

${\displaystyle \exists x\forall y(p(x)\rightarrow q(y))}$

and

${\displaystyle \forall y\exists x(p(x)\rightarrow q(y))}$

example

The starting formula is:

${\displaystyle \forall x.P(x)\land \forall y.Q(y)\land \forall z.R(z,y)}$

The variable y occurs both bound and free. However, this may not be in the prenex form. Therefore a new variable is introduced: w . After the adjustment it looks like this:

${\displaystyle \forall x.P(x)\land \forall w.Q(w)\land \forall z.R(z,y)}$

Now every variable appears either bound or free and thus we can all "pull" the quantifiers forward, which then looks like this:

${\displaystyle \forall x.\forall w.\forall z.(P(x)\land Q(w)\land R(z,y))}$

Individual evidence

1. ↑ http://formal.iti.kit.edu/teaching/FormSysWS1415/09PK1Normalform-print.pdf#page=12