Ugrás a tartalomhoz

A matematikai logika alkalmazásszemléletű tárgyalása

Pásztorné Varga Katalin, Várterész Magda, Sági Gábor

Panem Kft.

Rövid történeti áttekintés

Rövid történeti áttekintés

A logika történetének legalább nagy vonalakban való ismerete nem érdektelen azok számára, akik e tudományág átfogó megismerését, egyenetlen fejlődése és mély összefüggéseken alapuló alkalmazhatósága ok-okozati összefüggésének felismerését, valamint fejlődése sajátosságainak megértését tűzik ki célul. A történeti áttekintés során megemlítünk néhány klasszikus problémát és meglepő eredményt, amelyek alapjaiban változtatták meg a tudományos világképet és reméljük, hogy ezek a nagy jelentőségű, mély, ugyanakkor érdekes eredmények kedvet csinálnak a könyv további fejezeteinek tanulmányozásához is. Tehát mielőtt rátérnénk a logika tárgyalására, röviden áttekintjük a logika fejlődésének főbb szakaszait először a XIX. századig. Eddig a logika még egységes tudományág volt, bár közben jelen voltak azok az irányzatok, amelyek később önálló diszciplínákként jelentkeztek. Ilyenek a matematikai logika, ezen belül a modális logika, a többértékű logika és a típuselméleti logika. Ezután a logika XIX. és XX. századbeli történetét foglaljuk össze vázlatosan. A XX. század első felében a matematikai logika nagyívű fejlődése, majd a század második felében az összegző munkák, az alkalmazások és újabb fejlődési szakasz a jellemző.

A gondolkodás olyan folyamat, amelynek során az anyagi világot érzékelve tapasztalatokat gyűjtünk, megállapításokat teszünk és következtetéseket vonunk le. A természettudományok kialakulása és fejlődése a legjobb példa ennek illusztrálására. Ahhoz, hogy a következtetéseknek a valósággal való összevetéséből a gondolkodásnak olyan módozatai alakuljanak ki, amelyek mindig helyes eredményre vezetnek, igen sok tapasztalat és bizonyos fokú absztrakció volt szükséges. A gondolkodás kialakulásához az absztrakció képességét az emberiség hosszú történelmi fejlődés során szerezte meg. A logika kialakulásához, vagyis ahhoz, hogy a gondolkodás fejlődése során kialakult általános törvényeket lehessen vizsgálni, egy a korábbinál magasabb absztrakciós szintre kellett eljutni. A logika a gondolkodási folyamatokat úgy elemzi, hogy elvonatkoztat a gondolkodás tárgyát képező konkrét körülményektől, az adatokhoz kapcsolódó érzelmektől, hiedelmektől. Tehát csak azokat a törvényszerűségeket vizsgálja, amelyek a gondolkodásra jellemzőek, és ebben az értelemben általános érvényűek.

A logika története elsőként Arisztotelész görög filozófus (i. e. 384–322) logikai vizsgálatait említi. Arisztotelész tudományelméleti és logikai írásai az ,,Organon” című négykötetes műben maradtak fenn. Ennek két kötete, az ,,Analitika”, a formális logikát és annak a tudományos kutatásban és bizonyításban való alkalmazását tárgyalta.

Az arisztotelészi logika gondolkodási törvényei, a kategorikus szillogizmusok, több mint egy évezreden keresztül általánosan elfogadottak voltak. Továbblépés csak a XIV–XVI. században következett be. E szillogizmusok alapját négy, meghatározott szerkezetű, úgynevezett kategorikus állítás képezi. Ezeket a középkorban az a, e, i, o betűkkel jelölték, és a bennük szereplő betűket ,,predikátumoknak” (mai fogalmaink szerint formuláknak) nevezték. Szövegesen és mai olvasatunkban a kategorikus állítások a következők:

a általános állító:

a ( F , G )

Minden, ami F, az G.

x ( F ( x ) G ( x ) )

e általános tagadó:

e ( F , G )

Egyetlen F sem G.

x ( F ( x ) ¬ G ( x ) )

i részleges állító:

i ( F , G )

Van olyan F, ami G.

x ( F ( x ) G ( x ) )

o részleges tagadó:

o ( F , G )

Van olyan F, ami nem G.

x ( F ( x ) ¬ G ( x ) )

A szillogisztikában ezeket a kategorikus állításokat használjuk úgy, hogy három predikátum – M,S,P – esetén a feltételekben minden predikátum előfordul, de egyikük mindkét feltételben. A konklúzióban viszont (amely bármely kategorikus állítás lehet) csak a feltételben egyszer előfordulók szerepelnek. Arisztotelész azt vizsgálta, hogy az így kapható következtetési sémák közül melyek helyesek. Ilyenek például a

Barbara:

a ( M , P ) , a ( S , M ) a ( S , P )

Celarent:

e ( M , P ) , a ( S , M ) e ( S , P )

Darii:

a ( M , P ) , i ( S , M ) i ( S , P )

Ferio:

e ( M , P ) , i ( S , M ) o ( S , P )

A helyes következtetési formák kutatásával foglalkoztak még a sztoikusok (i. e. II. század) is, akik nem ragaszkodtak a kategorikus állítások kizárólagos használatához. Erre példa a

Minden ember halandó.

János ember.

Tehát

János halandó.

következtetés, amelynek alakja

x ( Ember  ( x ) Halandó  ( x ) )

Ember  ( János )

Tehát

Halandó  ( János )

A görög logika másik nagy alakja, Eukleidész, az ,,Elemek” című könyvében a korábbi és az általa feltárt geometriai eredményeket viszonylag kevés alapvető megállapítás, vagy posztulátum (később axióma) alapján vezette le. Szándéka az volt, hogy induláskor megadva a feltevéseket, tisztán logikai úton, a posztulátumok felhasználásával vezesse le a tételeket. Arisztotelész bonyolult logikai állítások analizálásával látta be azok igazságát. Eukleidész viszont a fordított irányú feladattal a szintézissel foglalkozott. Vagyis alapfeltevésekből kiindulva bonyolult logikai állítások logikai eszközökkel való igazolására törekedett. Ezzel a geometria axiomatizálásának gondolatát alapozta meg. A matematika későbbi fejlődési szintjén a XIX. század vége felé az aritmetika, majd később a többi diszciplína axiomatikus tárgyalása is kialakult. A matematikai absztrakció fejlődése a görögöktől napjainkig igen tanulságos a matematikai logika kialakulásának szempontjából.

A római korban és a reneszánsz idején kidolgoztak ugyan egy sor következtetésformát, azonban a logika megmaradt nagyjából azon a szinten, amelyet Arisztotelész munkássága határozott meg. A reneszánsz kor után is sokan foglalkoztak a logikával, de csak a XVI–XVIII. században alakulnak ki új irányzatok. Ez – a logika történetével foglalkozók szerint – annak köszönhető, hogy a filozófusok mellett olyan tudósok kezdtek logikával foglalkozni, akik – mint Leibniz és Bacon – a saját tudományterületük vizsgálatára és a kutatások megalapozására akarták használni a logikát. F. Bacon (1561–1626) a tapasztalati tudás gondolatának úttörője. Ő kezdeményezte az induktív kutatás és a kísérleti természettudomány eszméjét. G. W. Leibniz (1646–1716) áttörést hozott a logika fejlesztésében. Nem fogadta el, hogy minden következtetés szillogisztikus formába öntendő. Kidolgozta a formális bizonyítások elméletét, és megalapozta a formális logikát. Leibniz szerint ha a matematikai képletek közötti logikai kapcsolatokat logikai műveletekkel fejezzük ki, akkor ilyen képletekkel teljes bizonyításokat lehetne leírni és ki lehetne számolni a képlet igazságértékét. Az eredmény a tétel igazolását vagy cáfolatát adná. Ez volt az automatikus tételbizonyítás lehetőségének első megfogalmazása. A matematika területéről kilépve, egy vita eldöntésére a formalizált állításokkal és logikai kapcsolatokkal felírt ,,ideográfiai” képlet igazságértékének kiszámítását javasolta. Bevezetett néhány logikai jelölést és matematikai módszerekkel vizsgálta meg néhány logikai törvény helyességét.

Újabb számottevő eredmény hosszú ideig nem látott napvilágot. Sokan azt állítják, hogy a matematikai logika problematikus fejlődéséhez az járult hozzá, hogy a filozófusok, Hume, Kant és Hegel eszméi váltak uralkodóvá. Őket ugyanis az idealizmus és az empirizmus viszálya foglalkoztatta. Ebben lehet igazság, de a probléma gyökere inkább az lehetett, hogy a matematika fejlettségi szintje még nem tette lehetővé a további formalizáláshoz szükséges absztrakciót. A XIX. század közepén a logika újjáéledését azok a matematikusok hozták létre, akik a matematika alapjainak vizsgálatában élenjártak. A számunkra fontos irányokban, a formalizálás kialakításában és a matematikai logika fejlesztése útján megtett lépések nagy vonalakban a következők voltak. G. Boole (1815–1864) a ,,The Mathematical Analysis of Logic” című könyvében a logikai számítások céljára kialakított algebrai rendszert vizsgálta. Ez azt jelenti, hogy Boole a logikát numerikus algebrához hasonló kalkulusként kívánta bemutatni. Ezért a logikát mint a matematika egy ágát kezelte és mint matematikai struktúrát vizsgálta. Ez az algebrai rendszer még nem azonos a mai értelemben vett Boole-algebrák elméletével, de a logika algebrai eszközökkel való modellezése fontos előrelépés volt. A szimbolikus kalkulusokkal foglalkozott A. de Morgan (1826–1871) is, de kutatásainak tárgyát képezte a matematika alapjai és a logika közötti kapcsolatok vizsgálata, valamint a matematika különböző területeinek logikai megalapozása is. A Boole által folytatott kutatási irányhoz hozzájárultak még W. S. Jevons, C. S. Peirce, E. Schröder, J. Venn, A. N. Whitehead és B. V. Huntington. Peirce 1880 körüli érdekes eredménye, miszerint a logikai műveletek kifejezhetők egyetlen művelet, a ,,sem …, sem …” felhasználásával, feledésbe merült, majd 1913-ban H. M. Sheffer újra felfedezte. A Boole-algebrák elméletének kialakulásához J. Venn munkássága is hozzájárult. Ő a logikát mint algebrai struktúrát vizsgálta (1881-ben publikálta a ,,Symbolic Logic” c. könyvet). A formulákat szemléletesen ábrázolta (Venn-diagram), és így a tárgyalási univerzum részhalmazaival jellemezte azokat. Whitehead 1898-as publikációját követően Huntington 1904-es cikkében eljut a mai Boole-algebra – axiómák és rendezési reláció alapján való – definíciójához ([35], 408-409. oldal).

A soron következő előrelépés a matematikai logika felé G. Frege nevéhez fűződik. Frege azt akarta megmutatni, hogy az aritmetika azonos a logikával, más szóval, hogy az aritmetikai törvények visszavezethetők a logikára. Ehhez olyan logikára volt szüksége, amely bizonyos szempontból hasonló a numerikus algebrához. Kidolgozott egy nyelvet a logika leírására és vizsgálta, hogy hogyan lehet a logikát olyan rendszerré fejleszteni, amely már azonos az aritmetikával. 1879-ben megjelent könyvében (egyszerűsített címe ,,Fogalomírás” [35], 458-469. oldal) ezzel elsőként teremti meg a szimbolikus vagy formális logikát. Frege elsőként adott teljesértékű szimbolikus nyelvet a logika leírására, ahol a változtatható és a nem változtatható szimbólumok elkülönülnek, valamint elsőként dolgozott ki logikai kalkulust, vagy másképp levezetőrendszert is. Azzal pedig, hogy az aritmetikát mint diszciplínát logikai tárgyalásra alkalmassá tette, megalapozta a matematikai logikát ([25], magyar nyelvű, összefoglaló válogatás). Meg kell jegyezni, hogy G. Cantor már Frege előtt kidolgozott az aritmetikára egy logikai elméletet, J. W. R. Dedekind és G. Peano pedig kortársakként tettek sokat az aritmetika axiomatizálása terén. A halmazelmélet vizsgálata során az antinómiák felfedezésével Cantor és Russell ráirányították a figyelmet a matematika alapjainak vizsgálatára, ami szükségszerűvé tette a matematikai logika következetes kidolgozását. Frege hatása, valószínűleg nehéz olvashatósága miatt, utólagos. Tudjuk, hogy a nagy utód, B. Russell, csak a ,,Principles of Mathematics” c. könyvének megírása után (1903) tanulmányozta részletesebben Frege teljes munkásságát. Ennek köszönhető, hogy könyvének a függelékében ad átfogó ismertetést róla. Frege hatása azonban hosszú idő után is jelentős. R. Carnap 1947-ben [13], A. Church 1956-ban [16] nyúlt vissza Frege gondolataihoz. A logikai kutatásokat végignézve világos, hogy hogyan válik egyik legfontosabb feladattá a matematikai logika precíz, következetes felépítése.

Az egyik nagy témakör a matematikai diszciplínák axiomatizálása, az axiómarendszerek vizsgálata. A matematikai logika feladata a matematika egyes ágaival – mint axiomatizált elméletekkel – kapcsolatos globális kérdések vizsgálata. Ehhez a matematikai elméletet egy precíz matematikai-logikai nyelv segítségével formalizálják, majd a logika eszközeivel vizsgálják. Egy formalizált és axiomatizált elmélettel kapcsolatos első fontos kérdés, hogy mely állítások vezethetők le benne és melyek nem. Egy másik fontos kérdés, hogy ellentmondásos-e egy elmélet, azaz levezethető-e benne egy állítás és annak tagadása is. Egy sor elméletre – mint az aritmetika, az elemi geometria, az analízis – sokoldalúan vizsgálták és tisztázták az ellentmondásosság kérdését. A ,,gazdag” axiomatikus halmazelméletek (pl. a Zermelo–Fraenkel-féle vagy a Quine-féle) ellentmondásossága jóval bonyolultabb probléma. Ezzel kapcsolatos az 1930-as években bebizonyított Gödel-féle nemteljességi tétel. Ez azt mondja ki, hogy ha egy elmélet elég kifejező, akkor ellentmondástalansága nem bizonyítható az elmélet keretein belül. A teljességi kérdés egy elmélet esetén azt veti fel, hogy van-e olyan állítás az elméletben, amely sem nem bizonyítható, sem nem cáfolható, vagy másképp igaz-e bármely állításra, hogy vagy az állítás, vagy a tagadása levezethető a szóbanforgó elméletben. Például a Zermelo–Fraenkel-féle halmazelméletben a kiválasztási axióma egy olyan állítás, amely sem nem bizonyítható, sem nem cáfolható. Lényeges tulajdonsága egy elméletnek az eldönthetőség. Vagyis, hogy az elmélet bármely állításáról eldönthető-e, hogy levezethető-e vagy sem. 1948-ban A. Tarski megadott egy eljárást, amely az elemi geometria bármely állításáról el tudja dönteni, hogy levezethető-e vagy sem. Más elméletekről – például az aritmetikáról, az analízisről és a halmazelméletről – bebizonyították, hogy ott ilyen döntési eljárás nem létezik. A nemteljességi és eldönthetetlenségi eredmények ismeretelméleti jelentősége rendkívüli: matematikai precizitással szabnak elvi korlátokat a tudományos megismerés számára.

Egy másik nagy témakör az automatikus tételbizonyítás problémáinak a kutatása. Az eldöntésprobléma szemantikai és szintaktikai eszközökkel való megfogalmazása és megoldásának elvi kérdései jelentik az alapot. A logikai technika, a levezetőrendszerek, logikai kalkulusok fejlesztése mutat a megvalósítás irányába. A kalkulusok helyességi és teljességi[4] kérdése a szintaktikai és a szemantikai tárgyalásmód kapcsolatát hivatott tisztázni. Ezekre a kérdésekre az 1940-es évekre első körben már sikerült válaszolni. D. Hilbert, K. Gödel, A. Tarski, E. Post, T. Skolem, J. Herbrand, A. M. Turing, J. Lukasiewicz, G. Gentzen, P. I. Bernays, L. Henkin, G. Hasenjaeger és még mások nevei fémjelzik ezeket az eredményeket. Egyedül az elsőrendű bizonyításelmélet teljességének bizonyítása váratott magára. Ezt csak 1949-ben látta be Henkin. Ez a ragyogó technikával elért eredmény rendkívüli jelentőségű, nagy vonalakban azt mondja ki, hogy ha egy következtetés helyes, akkor be is lehet bizonyítani a helyességét.

Az 1950-es évektől az összegző munkák korszakának vagyunk tanúi. Ezek nagy része a logika formalizált nyelven való leírására alapozott tárgyalását viszi végig, ahol a formalizált nyelvhez hozzátartoznak azok a szimbólumok, amelyek alkalmasak bármely matematikai diszciplínát leíró nyelv kialakítására. A teljesség igénye nélkül néhány hivatkozás [7,16,32,33,34,41,59]. Kitűnik a sorból R. M. Smullyan könyve [60], amelyben a szerző a logika egységes tárgyalását tűzi ki célul. Így a különböző kalkulusok – Hilbert-féle bizonyításelmélet, a természetes levezetés, a Gentzen-féle (szekvent) módszer, a rezolúciós elv és a tabló módszer – teljességét egységes eszközökkel tudja igazolni. Ezzel megmutatja, hogy a különböző levezetőrendszerek teljessége a hozzájuk kapcsolódó konzisztenciafogalom tulajdonságaitól függ. Megmutatja, hogy a teljes kalkulusok konzisztenciafogalma lényegében azonos. Ezt a közös tulajdonságot az analitikus-, majd a szintetikus konzisztenciafogalom definíciójában adja meg. A számítógépek időközbeni fejlődése és a bonyolult algoritmusok implementációs lehetősége is erőteljesen motiválta a levezetőrendszerek fejlesztését. Az elsőrendű rezolúciós kalkulus kidolgozása 1968-ban [55], majd a rezolúciós levezetésekre kidolgozott stratégiák [15] megnyitották az utat az automatikus tételbizonyítás számítógéppel való végrehajtása előtt. Az automatikus tételbizonyítás elméleti és gyakorlati problémáinak megoldásával foglalkozó három alapkönyvet kell itt megemlíteni [15,38,40]. A rezolúciós kalkulus tette lehetővé a logikai programozás kialakulását [36,55] az 1970-es évek elejére. A Prolog-szerű logikai programozás logikai hátterének és lehetőségeinek kérdéseivel a [4,39] összefoglaló művek foglalkoznak.

Tarski kezdeményezte az 1930-as években és az 1960–70-es években kapott új lendületet a matematikai logika strukturális kérdéseinek magasabb szinten való kutatása. Ez a terület modellelmélet néven ismert. Egy összefoglaló mű: [14]. A modellelmélet a formális nyelvek és interpretációik (modelljeik) közötti kapcsolatokkal foglalkozik. Ezt a területet szokás logikai algebrának, vagy a logika univerzális algebrai tárgyalásának is nevezni. Korai modellelméleti eredmények L. Löwenheim 1915-ös tétele (ha egy mondatnak van végtelen modellje, akkor van megszámlálható modellje is), valamint Gödel (1930) és A. I. Malcev (1936) kompaktsági tétele (ha egy mondathalmaz minden véges részhalmazának van modellje, akkor a mondathalmaznak is van modellje). A modellelmélet jelenleg is egyik fontos kutatási területe a matematikai logikának. Alkalmazásként említjük a nemstandard analízis témát [17,54].

Az 1940–50-es évekre bebizonyosodott, hogy a matematikai logika a gyakorlatban igen sok területen alkalmazható. Az elektronikában, az elektronikus berendezések tervezése, ellenőrzése és analizálása az ítéletkalkulus egy igen fontos alkalmazási területe az 1950-es évek óta. Ezek az alkalmazások nagyban hozzájárultak ahhoz, hogy a két- és többértékű logikák strukturális vizsgálata és a funkcionális teljesség kutatása előtérbe került. A számítógépes hálózatok nyújtotta adatátviteli lehetőségek megkövetelik az adatok titkosítását. A kriptográfia elméletében nagy szerepet játszik a Boole-függvények elmélete és e függvények speciális, a szuperpozícióra zárt osztályai, a klónok [19]. A programozáselméletben, a párhuzamos és a konkurens rendszerek szintézisében, a számítástudományban, az adatbázis és tudásbázis kezelésben, a logikai programozásban és a mesterséges intelligenciában a logika fontos leíró, vizsgáló és bizonyító eszköz. Ezeken a területeken főleg a levezető – tételbizonyító eljárások fontosak. A logikai programozás [4,39] és a relációs adatbáziskezelés [1,68] elméleti megalapozása és az eljárások képességeinek kutatása igen érdekes eredményekhez és bizonyos nemstandard logikákhoz vezetett. A véges modellelmélet [23] az adatbázis és a tudásbázis kezelésével kapcsolatos problémák megoldásához nyújt elméleti hátteret, de hasznos eszközöket biztosít a bonyolultságelmélet számára is. A levezetőrendszerek megvalósításánál a tablók módszere és a Gentzen-féle kalkulus vizsgálata a 90-es évek témáinak jelentős részét képezi [2,26]. Ezek a kalkulusok lényeges elemei néhány ismert tételbizonyító rendszernek (PVS [48], ISABELLE) A magasabbrendű logikák alkalmazása mellett a típuselméleti logika [3], a λ-kalkulus, a kombinátor logika új utakat nyitnak és felhasználható eszközök sok gyakorlati probléma leírásában és megoldásában.



[4] Egy kalkulus teljességén mást értünk, mint egy elmélet teljességén.