Herbrand-univerzum

A Herbrand-univerzum a matematikai logikában egy logikai nyelv jelkészletéből felépíthető összes ún. alapterm, vagyis a logikai változót nem tartalmazó (függvény)kifejezések halmaza; szerepe az, hogy univerzumul szolgál egy e nyelvek vizsgálata számára fontos és hasznos eszköznek, a Herbrand-interpretációknak. A részletesebb definíciót ld. lentebb

Definíció[szerkesztés]

Formális definíció[szerkesztés]

Legyen L elsőrendű nyelv, C ennek konstansjeleinek, F pedig a függvényszimbólumainak halmaza! Rekurzív módon definiáljuk a „C univerzum feletti, F függvényszimbólumaiból készített F-termek” halmazát (és ezen „F-termek” összessége lesz a Herbrand-univerzum):

Ha C = ∅, akkor legyen C' = {a}, ahol a egy, az L jelkészletében elő nem forduló szimbólum („fiktív konstans”); Ha C ≠ ∅ akkor legyen C' = C.
$H_{0}\ :=\ C'$
$H_{1}\ :=\ H_{0}\ \cup \ \left\{\ f\left(h_{1},h_{2},\dots ,h_{n}\right)\ |\ f\in F\wedge h_{j}\in C'\ \right\}.$
$\dots$
$H_{i+1}\ :=\ H_{i}\ \cup \ \left\{\ f\left(h_{1},h_{2},\dots ,h_{n}\right)\ |\ f\in F\wedge h_{j}\in H_{i}\ \right\}$

Tehát mindegyik H_i halmaz (i>0) az azt megelőző H₀, H₁, …, H_i-1 halmazok uniója feletti egyszerű alaptermek halmaza. Végül pedig a Herbrand-univerzum a következő:

H:=\bigcup _{i=0}^{\infty }H_{i}

Megjegyezzük, a definíció alapján bizonyíthatóan H_i mindig tartalmazza az összes előző H₀,H₁,…,H_i-1 halmazt.

A Herbrand-univerzumelemek mint alappéldányok[szerkesztés]

Legyen L egy (esetleg skolemizált) elsőrendű nyelv, C a (nem-logikai) konstansjelek, F a függvényszimbólumainak, V = {x,y,z … } pedig a (logikai) változóinak halmaza! Emlékeztetünk arra, hogy az f(u₁,u₂,…,u_n) alakú kifejezéseket, ahol f∈F függvényjel, a nyelv feletti termeknek (függvénykifejezéseknek) nevezzük. Egy term egyszerű, ha argumentuma nem tartalmaz függvényszimbólumot; összetett ellenben; továbbá egy term zárt, ha nincs benne logikai változó.

Legyen adott egy U (univerzum)halmaz, a nyelv egy I interpretációjának alaphalmaza! Ekkor a konstanszimbólumoknak egy-egyértelműen megfeleltetünk néhány univerzumelemet (egy adott interpretációban mozogva, ezt megadva tehát a C halmazt az univerzum részének képzelhetjük). Legyen C_U az U azon részhalmaza, melynek elemeivel a konstansszimbólumokat interpretáltuk. Ekkor az f(d₁,d₂,…,d_n) alakú (mellesleg már nem az L nyelvbeli) kifejezéseket, ahol d₁,d₂,…,d_n∈C_U; az L nyelvbeli f függvényszimbólum U univerzum feletti alappéldányainak nevezzük (figyelem, ne keverjük össze az „alapterm” és egy term „alappéldányainak” fogalmát, bár pont a Herbrand-univerzum esetében ez nem vezet súlyos hibához.

Az F és C halmazokból képezett egyszerű zárt termek és az az F és C_U halmazokból képezett term-alappéldányok között „nüansznyi” a különbség, pusztán arról van szó, hogy előbbiek az L elemei, míg az utóbbiak nem, hiszen nem a konstansjeleket, hanem az azoknak megfelelő univerzumelemeket jelölő jeleket tartalmazzák. Utóbbiak egy olyan L' nyelv elemei, melynek konstansszimbólumainak halmaza C_U. De a konstanszimbólumok és a nekik az interpretáció által megfeleltett univerzumelemek közötti bijektív megfeleltetés miatt az egyszerű zárt termek és az egyszerű term-alappéldányok is egy-egyértelműen megfeleltethetőek.

Hasonlóan igaz ez az L nyelvbeli összetett zárt termekre és az L' beli összetett term-alappéldányokra. Ha „ugyanúgy” épül fel egy L beli kifejezés mint egy L'-beli, azaz szimbólumról szimbólumra vagy megegyeznek, vagy pedig az L-beli formula c konstansjele helyett az L'-beli formulában pont a neki megfelelő univerzumelem(-jel) áll, akkor a zárt term és a term-alappéldány megfelel egymásnak. Az egyik fontos különbség az, hogy a term-alappéldány mindig egy univerzum felett, azaz interpretációban van meghatározva. A term-alappéldányok mibenléte interpretációfüggő. Minden I interpretációhoz létezik egy L'(I) nyelv. Az L nyelv termjei nem függnek az interpretációktól. Mármost az L nyelv Herbrand univerzuma pontosan az egyik ilyen L'(I) nyelv, mégpedig az, ahol az I interpretáció U univerzuma az L nyelv konstansainak halmaza (vagy ha utóbbi üres, akkor egy "fiktív konstansból" álló egyelemű konstanshalmaz).

Az L'(I) nyelv termekből áll tehát, melyeket az elsőrendű nyelvekben leírtakhoz hasonló rekurzív módon definiálunk. Kikötve még azt, hogy az L' nyelv C' konstanshalmaza a C nyelv konstanshalmaza legyen, jutunk a Herbrand-univerzum fogalmához.