Prädikatenlogik/Variablensubstitution/Terme/Definition

Variablensubstitution für Terme

Es sei ein Symbolalphabet $S$ einer Sprache erster Stufe gegeben. Es seien $x_1,\dots ,x_k$ paarweise verschiedene Variablen und $t_1,\dots ,t_k$ fixierte $S$-Terme. Dann definiert man rekursiv über den Aufbau der Terme die Substitution $s\frac{t_1,\dots ,t_k}{x_1,\dots ,x_k}$ für jeden $S$-Term $s$.

1. Für eine Variable $x$ ist

   $x\frac{t_1,\dots ,t_k}{x_1,\dots ,x_k}:=\{\begin{array}{c}x,\text{ falls }x\ne x_i\text{ für alle }i,\\ t_i,\text{ falls }x=x_i.\end{array}$

2. Für eine Konstante $c$ ist

   $c\frac{t_1,\dots ,t_k}{x_1,\dots ,x_k}:=c.$

3. Für ein $n$-stelliges Funktionssymbol $f$ und $n$ Terme $s_1,\dots ,s_n$ ist

   $f{s}_1\dots s_n\frac{t_1,\dots ,t_k}{x_1,\dots ,x_k}:=f{s}_1\frac{t_1,\dots ,t_k}{x_1,\dots ,x_k}\dots s_n\frac{t_1,\dots ,t_k}{x_1,\dots ,x_k}.$