Individuenvariable (elementare Sprache), die in einem logischen Ausdruck frei vorkommt.

Das freie Vorkommen einer Variablen in einem Ausdruck kann wie folgt induktiv über den Aufbau der Ausdrücke definiert werden: Sei L eine elementare Sprache, x eine Individuenvariable und φ ein Ausdruck in L. xkommt in φfrei vor genau dann, wenn eine der folgenden Bedingungen erfüllt ist:

1. φ ist ein Atomarer Ausdruck und x kommt in φ vor.
2. φ besitzt die Gestalt ¬ψ und x kommt in ψ frei vor.
3. φ ist einer der Ausdrücke ψ ∧ χ, ψ ∨ χ, ψ → χ, ψ ↔ χ, und x kommt in ψ oder in χ frei vor.
4. φ besitzt die Gestalt ∃yψ oder ∀yψ und x kommt in ψ frei vor, und x, y sind verschiedene Variablen.

In einem Ausdruck der Gestalt ∃yψ bzw. ∀yψ ist ψ der Wirkungsbereich des Quantors ∃ bzw. ∀ bzgl. x. Eine Variable x kommt in dem Ausdruck φ gebunden vor genau dann, wenn x in φ vorkommt und x unmittelbar nach ∃ oder ∀ folgt, oder im Wirkungsbereich eines der Quantoren bzgl. x steht. x heißt dann auch gebundene Variable.

Eine Variable kann in einem Ausdruck sowohl frei als auch gebunden auftreten. Wir betrachten als Beispiel den Ausdruck \begin{eqnarray}\varphi :=\forall z(\exists x(x+y\lt z)\to \forall y(y+1\lt x))\end{eqnarray} mit ψ := x + y< z und χ : = y + 1 < x. In ψ bzw. χ kommen x, y, z bzw. x, y frei vor. In ∃yΦ kommen y, z frei und x gebunden vor und in ∀yχ kommt x frei und y gebunden vor. Schließlich kommen x, y in φ frei und gebunden vor, und z kommt in φ nur gebunden vor.