Bereinigte Normalform

In der Prädikatenlogik heißt eine Formel bereinigt, wenn

1. keine Variable in der Formel einmal als freie und als gebundene Variable vorkommt,
2. hinter jedem Quantor eine andere Variable steht.

Zu jeder Formel gibt es eine äquivalente bereinigte Formel. Jede Formel ${\displaystyle F}$ lässt sich durch geeignete, gebundene Umbenennung in eine bereinigte Form überführen.