Variablensubstitution für Terme
Es sei ein Symbolalphabet
S
{\displaystyle {}S}
Sprache erster Stufe
gegeben. Es seien
x
1
,
…
,
x
k
{\displaystyle {}x_{1},\ldots ,x_{k}}
t
1
,
…
,
t
k
{\displaystyle {}t_{1},\ldots ,t_{k}}
S
{\displaystyle {}S}
Terme .
Dann definiert man rekursiv über den Aufbau der Terme die Substitution
s
t
1
,
…
,
t
k
x
1
,
…
,
x
k
{\displaystyle {}s{\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}}
S
{\displaystyle {}S}
s
{\displaystyle {}s}
Für eine Variable
x
{\displaystyle {}x}
x
t
1
,
…
,
t
k
x
1
,
…
,
x
k
:=
{
x
,
falls
x
≠
x
i
für alle
i
,
t
i
,
falls
x
=
x
i
.
{\displaystyle {}x{\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}:={\begin{cases}x,{\text{ falls }}x\neq x_{i}{\text{ für alle }}i\,,\\t_{i},{\text{ falls }}x=x_{i}\,.\end{cases}}\,}
Für eine Konstante
c
{\displaystyle {}c}
c
t
1
,
…
,
t
k
x
1
,
…
,
x
k
:=
c
.
{\displaystyle {}c{\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}:=c\,.}
Für ein
n
{\displaystyle {}n}
f
{\displaystyle {}f}
n
{\displaystyle {}n}
s
1
,
…
,
s
n
{\displaystyle {}s_{1},\ldots ,s_{n}}
f
s
1
…
s
n
t
1
,
…
,
t
k
x
1
,
…
,
x
k
:=
f
s
1
t
1
,
…
,
t
k
x
1
,
…
,
x
k
…
s
n
t
1
,
…
,
t
k
x
1
,
…
,
x
k
.
{\displaystyle {}fs_{1}\ldots s_{n}{\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}:=fs_{1}{\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}\ldots s_{n}{\frac {t_{1},\ldots ,t_{k}}{x_{1},\ldots ,x_{k}}}\,.}
