Prädikatenlogik/Ausdrücke/Substitution/1/Beispiel

Es seien ${}c,d$ Konstanten einer erststufigen Sprache, ${}x,y,z,u$ Variablen (so geordnet), ${}f,g$ einstellige Funktionssymbole und ${}R$ ein zweistelliges Relationssymbol. Wir betrachten den Ausdruck

${}\alpha =\forall x\neg Ryfx\,$

und die Substitution

${\frac {u,\,\,\,\,gc}{x,\,\,\,\,\,\,y}}.$

Von den zu substituierenden Variablen ist ${}x$ gebunden und ${}y$ frei. Die Variable ${}x$ kommt in den substituierenden Termen nicht vor. Also ist

${}{\left(\forall x\neg Ryfx\right)}{\frac {u,\,\,\,\,gc}{x,\,\,\,\,\,\,y}}=\forall x{\left(\neg Ryfx{\frac {gc}{y}}\right)}=\forall x\neg Rgcfx\,.$

Bei der Substitution

${\frac {u,\,\,\,\,gx}{x,\,\,\,\,\,\,y}}$

kommt jetzt die gebundene Variable ${}x$ in dem substituierenden Term ${}gx$ vor. Es ist ${}v=z$ die nächste Variable in der gegebenen Reihenfolge. Somit ist

${}{\left(\forall x\neg Ryfx\right)}{\frac {u,\,\,\,\,gx}{x,\,\,\,\,\,\,y}}=\forall z{\left(\neg Ryfx{\frac {gx,\,\,\,\,z}{y,\,\,\,\,\,\,x}}\right)}=\forall z\neg Rgxfz\,.$