Bereinigte Normalform

In der Prädikatenlogik heißt 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 v P\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 folgende Umbenennung (bei der Umbenennung müssen die gebundenen Variablen umbenannt werden):

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

Siehe auch

• Normalform
• Freie Variable