Variablensubstitution für Ausdrücke
Es sei ein Symbolalphabet
einer Sprache erster Stufe gegeben. Es seien
paarweise verschiedene Variablen und
fixierte
-Terme.
Dann definiert man rekursiv über den Aufbau der
-Ausdrücke
die
Substitution
für jeden
-Ausdruck
.
- 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.