Es seien
Konstanten einer
erststufigen Sprache,
Variablen
(so geordnet),
einstellige Funktionssymbole und
ein zweistelliges Relationssymbol. Wir betrachten den Ausdruck
-
![{\displaystyle {}\alpha =\forall x\neg Ryfx\,}](https://wikimedia.org/api/rest_v1/media/math/render/svg/348ee520c05d612bda9cd160fbb9bdd46c3dd46e)
und die Substitution
-
Von den zu substituierenden Variablen ist
gebunden und
frei. Die Variable
kommt in den substituierenden Termen nicht vor. Also ist
-
![{\displaystyle {}{\left(\forall x\neg Ryfx\right)}{\frac {u,\,\,\,\,gc}{x,\,\,\,\,\,\,y}}=\forall x{\left(\neg Ryfx{\frac {gc}{y}}\right)}=\forall x\neg Rgcfx\,.}](https://wikimedia.org/api/rest_v1/media/math/render/svg/cae83a84cbac396fbe1acbed0178445a55285250)
Bei der Substitution
-
kommt jetzt die gebundene Variable
in dem substituierenden Term
vor. Es ist
die nächste Variable in der gegebenen Reihenfolge. Somit ist
-
![{\displaystyle {}{\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\,.}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e47738211f4ae8dbe1c6b8dfe779035da11b81e6)