Bereinigte Normalform

In der Prädikatenlogik heisst eine Formel bereinigt, wenn

1. keine Variable sowohl frei als auch gebunden vorkommt,
2. hinter jedem Quantor eine andere Variable steht.

Hinweis: Zu jeder Formel gibt es eine bereinigte äquivalente Formel. Jede Formel F, lässt sich durch geeignete, gebundene Umbenennung in eine bereinigte Form überführen.

Beispiel:

$F:=\forall x\exists y\left(P\left(x,y\right)\wedge Q\left(x,a\right)\right)$

$G:=\exists u\left(\forall vP\left(u,v\right)\vee Q\left(v,v\right)\right)$

In der Formel F sind die Variablen x und y gebunden und a ist frei. F ist somit bereinigt. In der Formel G sind alle Vorkommen der Variable u gebunden, allerdings tritt v sowohl gebunden als auch frei auf. G ist daher nicht in bereinigter Form. Eine Überführung für G ist folgene Umbenennung:

$G':=G\left[v/w\right]=\exists u\left(\forall vP\left(u,v\right)\vee Q\left(w,w\right)\right)$

---

siehe auch Normalform Abschnitt Prädikatenlogik