Prädikatenlogik (Bindungen)

Jede Formel hat eine Baumstruktur (vgl. Ausgabe autotool)

Ein Vorkommen einer Variablen x heißt gebunden, falls sich auf dem Pfad vom Vorkommen zur Wurzel ein Quantor befindet, der x bindet.

(sonst heißt das Vorkommen frei)