OK (Variablenfang)

Um ungewollte Bindungen (den sogenannten Variablenfang) während einer Substitution zu vermeiden, verwendet man das Prädikat $OK(t,x,\phi )$.

Dieses Prädikat ist genau dann erfüllt, falls $\phi$ kein freies Vorkommen von $x$ aufweist, welches sich im Gültigkeitsbereich eines Quantors $Qy$ befindet, wobei $y$ eine im Term $t$ vorkommende Variable darstellt ($y\in var(t)$).