Definíció Egy olyan függvényt, amely az elsőrendű nyelv véges sok változóján van értelmezve, és minden változóhoz termet rendel, termhelyettesítésnek nevezünk. Üres a termhelyettesítés, ha az értelmezési tartománya üres (jele:
).
Ha a
termhelyettesítés értelmezési tartománya
és
minden
-ra
,
-t megadhatjuk a
táblázattal vagy a
felsorolással.
jelölje azt a termhelyettesítést, melyre
és minden
esetén
. Vezessük be továbbá a
jelölést a
kifejezés szerkezetétől és a
termhelyettesítéstől függő logikai kifejezésre:
Vegyük észre, hogy az értékelő helyettesítések is termhelyettesítések, és ha
a
kifejezés értékelése, a
kifejezés éppen a
-beli paraméterek szabad előfordulásainak a
-val hozzájuk rendelt konstansszimbólumokkal való helyettesítésnek eredményeképpen kapott értékelt kifejezés.
Ugyanakkor nem minden
kifejezés és
termhelyettesítés esetén lesz alkalmas
a logika céljai számára. Hogy csak ezekkel a
kifejezésekkel foglalkozhassunk, vezessünk be néhány fogalmat. A
termhelyettesítés megengedett a
kifejezés számára, ha minden
esetén
minden
-beli szabad előfordulása kívül esik a
term valamennyi változóját megnevező kvantor hatáskörén.
Definíció
megengedettsége
számára
szerkezete szerint:
Termek és atomi formulák számára minden termhelyettesítés megengedett.
számára egy termhelyettesítés megengedett, ha megengedett
számára.
számára egy termhelyettesítés megengedett, ha megengedett
és
számára is.
számára egy
termhelyettesítés megengedett, ha
Példa A
formula számára az
termhelyettesítés megengedett, az
termhelyettesítés pedig nem megengedett, mert a helyettesítendő
szabad előfordulású
az
-et kötő
hatáskörében van, és a helyére beírandó
termben is előfordul az
változó.
Legyen
egy kifejezés és
egy termhelyettesítés. Konstruáljunk meg egy
-val kongruens olyan
formulát, amely számára
megengedett. Ekkor a
kifejezés a
termhelyettesítés
-ban való szabályos végrehajtásának eredménye. Jelölése:
.
Definíció
meghatározása
szerkezete szerint:
Ha
term vagy atomi formula, akkor
.
Ha egyetlen
változó esetén sem fordul elő a
termben
, akkor
.
Ha van olyan
változó, hogy
paraméter
-ben, akkor válasszunk egy új változót – például
-t –, mely nem fordul elő sem
-ban, sem
termjeiben, és
Példa A
formulában az
termhelyettesítés szabályos végrehajtásának eredménye a
formula.
Definíció Legyenek
egy nyelv termhelyettesítései.
és
kompozícióján a
termhelyettesítést értjük, ahol
Példa Legyenek
termhelyettesítések. Ekkor
és
A példa mutatja, hogy a kompozíció művelete egy nyelv termhelyettesítéseinek halmazán nem kommutatív.
Tétel Egy elsőrendű logikai nyelv tetszőleges
,
és
termhelyettesítései esetén
| (1) |
|
(a kompozíció asszociatív) |
| (2) |
|
( neutrális elem) |
Azaz a kompozíció műveletével a termhelyettesítések halmaza neutrális elemmel rendelkező félcsoport.
Lemma Legyenek
és
egy nyelv termhelyettesítései. Ekkor tetszőleges
logikai kifejezés esetén
Definíció Legyenek
és
termhelyettesítések. Az
helyettesítés általánosabb a
-nál, ha van olyan
termhelyettesítés, hogy
.
Példa Az
helyettesítések esetén
általánosabb a
helyettesítésnél, mert
, ahol
