Prädikatenlogik/Zweifache Substitution/Einfache Substitution/Semantik/Aufgabe

Es seien ${}x,y$ Variablen, ${}s,t$ Terme und ${}\alpha$ ein Ausdruck in einer prädikatenlogischen Sprache. Es seien ${}u,v$ neue Variablen, die weder in ${}s$ noch in ${}t$ noch in ${}\alpha$ vorkommen. Zeige, dass

$\alpha {\frac {s,t}{x,y}}\leftrightarrow \alpha {\frac {s{\frac {v}{y}}}{x}}{\frac {t{\frac {u}{x}}}{y}}{\frac {x}{u}}{\frac {y}{v}}$

allgemeingültig ist, wobei der Ausdruck rechts als die Hintereinanderausführung von vier Einzelsubstitutionen (von links nach rechts)

zu lesen ist.

Zur Lösung, Alternative Lösung erstellen