Die Variablensubstitution definiert man rekursiv über den Aufbau der
-Ausdrücke.
- Für Terme setzt man
-
- Für ein -stelliges Relationssymbol und Terme setzt man
-
- Für einen Ausdruck setzt man
-
- Für Ausdrücke und setzt man
-
und ebenso für die anderen zweistelligen Junktoren.
- Für einen Ausdruck seien diejenigen Variablen
(unter den ),
die in frei vorkommen. Es sei , falls nicht in vorkommt. Andernfalls sei die erste Variable
(in einer fixierten Variablenaufzählung, falls es abzählbar viele Variablen gibt, bzw. in einer fixierten Wohlordnung der Variablenmenge),
die weder in noch in vorkommt. Dann setzt man
-
und ebenso für den Existenzquantor.