9.1. Ítéletlogikai következtetés kontra elsőrendű logikai következtetés

Ez és a következő alfejezet bemutatja azokat a gondolatokat, amelyeken a modern logikai következtetési rendszerek alapulnak. Néhány egyszerű következtetési szabállyal kezdjük, amelyeket kvantorral ellátott mondatokhoz alkalmazhatunk, hogy a segítségükkel kvantorok nélküli mondatokhoz juthassunk. Ezek a szabályok természetes módon elvezetnek minket ahhoz a gondolathoz, hogy az elsőrendű következtetés megvalósítható azáltal, hogy a tudásbázist ítéletlogikává alakítjuk át, és a már általunk ismert ítéletlogikai következtetést használjuk. A következő alfejezet rámutat egy kézenfekvő egyszerűsítésre, amellyel olyan következtetési módszerekhez juthatunk, amelyek közvetlenül képesek az elsőrendű mondatok felhasználására.

9.1.1. Kvantorokra vonatkozó következtetési szabályok

Kezdjük az univerzális kvantorok vizsgálatával. Tételezzük fel, hogy a tudásbázisunk tartalmazza a standard hagyományos axiómákat, amelyek szerint minden mohó király gonosz:

x Király(x) ∧ Mohó(x) ⇒ Gonosz(x)

Ebből lehetségesnek tűnik kikövetkeztetni a következő mondatokat:

Király(János) ∧ Mohó(János) ⇒ Gonosz(János)

Király(Richárd) ∧ Mohó(Richárd) ⇒ Gonosz(Richárd)

Király(Apja(János)) ∧ Mohó(Apja(János)) ⇒ Gonosz(Apja(János))

...

Az univerzális példányosítás (Universal Instantiation, UI) szabálya kimondja, hogy az adott változó bármely alaptermmel (ground term) (változók nélküli termmel) való helyettesítésével elérhető mondatokat kikövetkeztethetjük.[87] Ahhoz, hogy formálisan le tudjuk írni a következtetési szabályokat, a 8.3. alfejezetben bevezetett helyettesítés (substitution) fogalmát használjuk. A HELYETTESÍT (θ, α) fogja jelölni annak az eredményét, hogy egy θ behelyettesítést alkalmazunk az α mondathoz. Ekkor a szabály így írható le:

bármely v változóra és g alaptermre. Például a korábban megadott három mondatot megkaphatjuk a következő helyettesítésekkel {x/János}, {x/Richárd} és {x/Apjα(János)}.

Az ennek megfelelő egzisztenciális példányosítási (Existential Instantiation) szabály az egzisztenciális kvantorra egy kicsivel komplikáltabb. Minden α mondatra, v változóra és olyan k konstans szimbólumra, amely sehol máshol nem jelenik meg a tudásbázisban:

Például abból a mondatból, hogy:

x Korona(x) Fején(x, János)

kikövetkeztethetjük ezt a mondatot:

Korona(C1) Fején(C1, János)

feltéve, ha a C1 nem jelenik meg sehol máshol a tudásbázisban. Alapjában véve az egzisztenciális mondat azt mondja ki, hogy van valamely objektum, amely eleget tesz egy feltételnek, és a példányosítás folyamata csak névvel látja el ezt az objektumot. Ez a név viszont már nem tartozhat más objektumhoz. Egy szép példát találunk a matematikában: tételezzük fel, hogy tudjuk, létezik olyan szám, amely egy kicsit kisebb, mint 2,71828, és eleget tesz annak az egyenletnek, hogy: d(xy)/dy = xyaz x-re. Adhatunk nevet ennek a számnak, mint például e, de hiba lenne olyan nevet adni, amely már egy létező objektumhoz tartozik, mint például a Π. A logikában ezt az új nevet Skolem-konstansnak (Skolem constant) nevezzük. Az egzisztenciális példányosítás egy speciális esete egy általánosabb folyamatnak, amelyet skolemizációnak (skolemization) nevezünk, és amelyet a 9.5. alfejezetben mutatunk be.

Amellett hogy az egzisztenciális példányosítás bonyolultabb, mint az univerzális példányosítás, kissé különböző szerepet is játszik a következtetésben. Míg az univerzális példányosítást többször is alkalmazhatjuk, hogy sok különböző eredményhez jussunk, az egzisztenciális példányosítást csak egyszer végezhetjük el, majd az egzisztenciális kvantorral ellátott mondattól megszabadulhatunk. Például amint hozzáadtuk a tudásbázishoz a Meggyilkol(Gyilkos, Áldozat) mondatot, már nincs szükségünk a ∃x Meggyilkol(x, Áldozat) mondatra. Pontosabban megfogalmazva, az új tudásbázis logikailag nem ekvivalens a régivel, de tekinthetjük úgy, hogy a következtetés szempontjából ekvivalens (inferentially equivalent), azaz pontosan akkor kielégíthető, amikor az eredeti tudásbázis is kielégíthető.

9.1.2. Redukálás ítéletlogikára

Ha egyszer vannak szabályaink arra, hogy kvantorral ellátott mondatokból hogyan következtethetünk kvantor nélküli mondatokra, akkor vissza tudjuk vezetni az elsőrendű következtetést az ítéletlogikai következtetésre. Ebben az alfejezetben áttekintjük ennek a módszernek a legfontosabb elemeit; a részletekről a 9.5. alfejezetben fogunk szólni.

Az első gondolat az, hogy éppen úgy, ahogyan egy egzisztenciális kvantorral ellátott mondatot felcserélhetünk a mondat egy példányával, egy univerzális kvantorral ellátott mondatot is felcserélhetünk a mondat összes lehetséges példányosításainak halmazával. Például tételezzük fel, hogy a tudásbázisunk mindössze a következő mondatokat tartalmazza:

x Király(x) ∧ Mohó(x) Gonosz(x)

Király(János) (9.1)

Mohó(János)

Fivér(Richárd, János)

Ekkor alkalmazzuk az univerzális páldányosítást az első mondatra úgy, hogy az összes lehetséges alapterm-helyettesítést felhasználjuk a tudásbázisszótárból, ami ebben az esetben az {x/János} és az {x/Richárd}. Így ezt kapjuk:

Király(János) Mohó(János) Gonosz(János)

Király(Richárd) Mohó(Richárd) Gonosz(Richárd)

és megválhatunk az univerzális kvantorral ellátott mondattól. Mármost, a tudásbázist alapvetően ítéletkalkulus-belinek tekinthetjük, ha az alap atomi mondatokat, mint a Király(János), Mohó(János) stb., ítéletlogikai szimbólumoknak tekintjük. Így tehát a 7. fejezetben bemutatott bármely teljes ítéletlogikai algoritmust alkalmazhatjuk, hogy olyan következtetéshez juthassunk, mint a Gonosz(János).

Ez a technika az ítéletlogikai állításokra való visszavezetés (propositionalization), amelyet teljesen általánossá tehetünk, mint azt a 9.5. alfejezetben be is fogjuk mutatni. Ez azt jelenti, hogy minden elsőrendű tudásbázis és lekérdezés átalakítható ítéletlogikai mondatokra úgy, hogy a tudásbázis vonzatai nem változnak. Így tehát van egy teljes következtetési folyamatunk vonzatok levezetésére. Vagy talán mégsem? Van egy probléma: amikor a tudásbázis tartalmaz függvényszimbólumot, a lehetséges alaptermek helyettesítéseinek halmaza végtelen! Például ha a tudásbázis megemlíti az Apja szimbólumot, akkor végtelen számú egymásba ágyazott termeket hozhatunk létre, mint például az Apja(Apja(Apja(János))). Az ítéletlogikai algoritmusainknak tehát nehézségeik lesznek a végtelen nagyságú mondathalmazokkal.

Szerencsére ismert egy Jacques Herbrandnak köszönhető híres tétel az előbbi problémára (Herbrand, 1930), ami azt mondja ki, hogy ha egy mondat következik az eredeti, elsőrendű tudásbázisból, akkor létezik olyan bizonyítás, amely csak egy véges méretű részhalmazt használ fel az ítéletkalkulus-belire átalakított tudásbázisból. Mivel bármely ilyen részhalmazban az alaptermeknek van egy maximális beágyazási mélysége, meg lehet találni a részhalmazt úgy, hogy először generáljuk az összes példányt a konstans szimbólumokhoz (Richárd és János), azután az összes 1-es mélységű termet (Apja(Richárd) és Apja(János)), majd az összes 2-es mélységű termet, és így tovább mindaddig, amíg képesek leszünk megalkotni a vonzatmondat ítéletlogikai bizonyítását.

Fontos

Felvázoltuk az elsőrendű következtetés egy megközelítését az ítéletlogikai állításokra való visszavezetés révén, amely teljes (complete) – tehát bármely következményként kapott mondatot bizonyítani tudunk. Ez jelentős eredmény, ha figyelembe vesszük, hogy a lehetséges modellek száma végtelen. Másrészt viszont nem tudhatjuk, hogy a mondat vonzat-e, amíg a bizonyítás nincs kész. Mi történik, ha α mondat nem vonzata a TB-nek? Meg tudjuk-e ezt állapítani? Nos, ahogy ez majd kiderül, az elsőrendű logika esetében erre a kérdésre a válasz nemleges. A bizonyítási eljárás tovább folytatódik, egyre mélyebben beágyazott termeket generálva, és nem tudhatjuk, hogy a folyamat egy végtelen ciklusba kerül, vagy hamarosan megleljük a bizonyítást. Ez nagyon hasonló a Turing gépek leállási problémájához. Alan Turing és Alonzo Church egymástól függetlenül és eltérő módon bizonyították be ennek a kérdésnek az eldönthetetlenségére vonatkozó tételt (Turing, 1936; Church, 1936). Az elsőrendű logikában a maga után vonzás kérdése félig eldönthető (semidecidable), ami azt jelenti, hogy létezik olyan algoritmus, amely igent mond minden vonzatmondatra, de nem létezik olyan algoritmus, amely emellett képes nemet mondani a nem levezethető mondatokra.



[87] Ne keverjük össze ezeket a helyettesítéseket a kiterjesztett interpretációkkal, amelyeket a kvantorok szemantikájának a meghatározására használtunk. A helyettesítés egy változót cserél le egy termre (egy szintaktikai elemre), hogy új mondatot hozzon létre, ezzel szemben egy interpretáció hozzárendel egy változót egy objektumhoz a tárgyterületben.