Variablensubstitution für Terme
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 Terme die Substitution
für jeden
-Term
.
- Für eine Variable
ist
-

- Für eine Konstante
ist
-

- Für ein
-stelliges Funktionssymbol
und
Terme
ist
-
