Limes rovat

A matematikai szigorúságról

Grolmusz Vince
matematika, axiómarendszer, Russell paradoxona, Georg Cantor, Cantor paradoxona, logicizmus, Gottlob Frege, Bertrand Russell, Alfred North Whitehead, konstruktivista, intuicionizmus, Luitzen Egbertus Jan Brouwer, David Hilbert, formalizmus, konzisztencia, ellentmondás-mentesség, Fermat-sejtés, Artúr–Merlin-féle bizonyítás, Kurt Gödel, Gödel-tétel

„Ha a matematikai gondolkodás tökéletlen,
akkor hol találjunk igazságot és bizonyosságot?”

A matematika deduktív tudomány, így állításait szigorú bizonyításokkal kell – nemcsak alátámasztania vagy megokolnia, mint más tudományok esetében, hanem – érvényessé tennie. Éppen a bizonyítás szigorúságával szemben támasztott követelményei különböztetik meg más tudományoktól. A matematikai érvelések szigorúságával foglalkozunk a következő fejtegetésekben.

I. A szigorúság forradalma

A XIX. század matematikusai úgy gondolták, hogy bebizonyított tételeik abszolút igazak, érvényességükhöz kétség sem férhet, s így a matematika a maga abszolút biztonságával kivételes helyzetben van a tudományok között. Arra a kérdésre, hogy mikor nevezhetünk egy tételt bebizonyítottnak, azt a választ adták, hogy akkor, ha a bizonyítás „szigorúan logikus”. Azonban a szigorúan logikus bizonyítás kritériumai sehol sem voltak explicite meghatározva, a helyzet olybá tűnt, hogy a matematikusok intuíciójára van bízva: egy bizonyítást elfogadnak-e „szigorúan logikusnak”, vagy sem. Megjegyezzük, hogy ez az intuíció – már Eukleidésztől kezdve – általában jól működik, és kétségtelenül szabatos bizonyításokat eredményez.

A XIX. század vége felé, a matematika fejlődésével, lehetőség nyílt rá, hogy Eukleidész axiomatikus módszerét a következtetési sémákra is alkalmazzák. Lehetőség nyílt rá, hogy száműzzék a homályos „szigorúan logikus” követelményt: Gottlob Frege volt az első, aki az összes általa használt következtetési szabályt formalizálta, s axiómáiból ezen következtetési szabályok segítségével, az élő nyelv kiiktatásával írta le bizonyításait (az aritmetika – ezen belül a természetes szám fogalmának – matematikai logikai alapokból történő levezetését) [F]. Munkájának célja a matematika végső, szilárd – logikai – alapokra való helyezése volt.

Frege formalizált bizonyításainak ellenőrzése mechanikus tevékenység, ma már azt mondanánk, hogy számítógéppel könnyen elvégezhető lenne. Frege abszolút szigorúságra való törekvése azonban nem járt sikerrel: a századfordulón fölfedezett paradoxonok mind Frege munkáját, mind a századforduló matematikáját megrengették. Így például Russell paradoxona:

Nevezzük nem-tartalmazkodóknak azokat a halmazokat, amelyek nem elemük önmaguknak. Tekintsük ekkor az összes nem tartalmazkodó halmaz A halmazát. Ekkor, ha A∈A, akkor A nem lehet eleme A-nak, mivel A tartalmazkodó. Ha azonban A nem eleme A-nak, akkor A∈A teljesül, mivel A nem-tartalmazkodó. Tehát az A∈A állítás ekvivalens saját tagadásával. Vagy egy másik híres antinómia Cantor paradoxona: Ismeretes, hogy egy M halmaz hatványhalmazának számossága szigorúan nagyobb, mint M számossága. Ha M jelöli az összes halmazok halmazát, akkor, mivel M hatványhalmaza megegyezik saját magával, ezért azt kapjuk, hogy M számossága nagyobb M számosságánál.

Russell paradoxona Frege elméletében is föllépett, s ez Frege munkáját mint ellentmondást tartalmazó elméletet sokáig feledésre kárhoztatta. Azonban Frege igénye bizonyításainak „abszolút szigorúvá” tételére, s ennek általa kidolgozott eszközei mai „szabatos bizonyítás” fogalmunk alapjául szolgálnak. A századforduló táján fölmerült paradoxonok ugyanis az addigi matematikai logika és halmazelmélet tarthatatlanságára mutattak rá. Az is bizonyossá lett, hogy egy bizonyítás helyességének ismérve nem lehet annak csupán „szigorúan logikus” volta, hiszen ilyennek tűnt Cantor halmazelmélete és Frege munkája is. A paradoxonok kiküszöbölése azonban – mindenki által elfogadható módón – a mai napig sem sikerült.

Az alapok válságának megoldására három iskola vállalkozott: a logicisták, a konstruktivisták és a formalisták iskolája.

A logicisták (Frege, Russell, Whitehead és követőik) a halmazelmélet olyan átfogalmazására törekedtek, amely elkerüli Russell és Cantor paradoxonát, s átmenti a cantori naiv halmazelmélet lehető legnagyobb részét. Azt remélték, hogy az így megregulázott halmazelmélet segítségével már valóban szilárd alapokra helyezhetik a matematikát. Munkájuk talán legjelentősebb eredménye lett a halmazelmélet Zermelo–Fraenkel-féle axiómarendszere. Programjuk második része azonban nem vezetett eredményre, nem sikerült a matematika biztos alapokra való helyezése.

A Brouwer által alapított konstruktivista (intuicionista) iskola hívei úgy vélik, hogy csak azokat a matematikai objektumokat értelmes dolog létezőknek tekinteni, melyek – az intuíció által adott – természetes számokból véges sok lépésben megkonstruálhatók. Ha elfogadjuk Brouwer nézeteit, akkor a matematika sok-sok eredményétől búcsút kell vennünk. A konstruktivistákról Hilbert így vélekedett:

„Arra törekszenek, hogy oly módon mentsék meg a matematikát, hogy mindent kidobnak, ami csak bajt okozhat… Felaprítanák és összekaszabolnák a tudományt. Ha olyan reformot követnénk, melyet ők javasolnak, akkor azt kockáztatnánk, hogy legértékesebb kincseink nagy részét elveszítjük.”

Hilbert formalizációs programja szerint olyan „formális nyelvet” kell kifejleszteni, amely segítségével minden levezetést mechanikusan ellenőrizni lehet, bizonyos átalakítási szabályok helyességének vizsgálatával. Ha ezután sikerül tisztán véges érvekkel – tehát mindenki által elfogadhatóan – bebizonyítani, hogy ebben a formális rendszerben nem lehet ellentmondásra jutni, akkor a matematika biztos alapokra helyeztetett. A formalizációs program ígéretesnek tűnt egészen addig, amíg Kurt Gödel 1930-ban bebizonyította híres (második) nem-teljességi tételét, amely szerint ha egy ellentmondásmentes elméletben fölépíthető az aritmetika, akkor az elmélet konzisztenciája (ellentmondás-mentessége) nem bizonyítható. Ez az eredmény egyrészt végzetes csapást mért Hilbert formalizációs programjára, másrészt kiderült az is, hogy búcsút kell mondani a matematika abszolút csalhatatlanságába vetett illúzióknak. A helyzet tehát az, hogy a matematikában ma mindenkire az a veszély leselkedik, hogy kedvenc elméletében egy napon ellentmondásra bukkan (bár ezt a matematikusok közül szinte senki sem hiszi komolyan).

A válságnak pozitív következményei is voltak: a matematikai logika óriási fejlődésnek indult, s a matematikai köztudatba beférkőzött a – lényegében már Frege által kidolgozott – „szigorú bizonyítás” matematikai logikai definíciója. Megjegyezzük, hogy Gödel, említett tétele bizonyításában, a „bizonyítást” mint matematikai objektumot vizsgálja és alkalmazta.

II. „Bizonyításokról”, amelyek talán bizonyítanak, de mégsem győznek meg

Képzeljük el, hogy beállít szobánkba egy zavaros tekintetű úr, drámaian bejelenti, hogy sikerült bebizonyítania a nagy Fermat-sejtést, s lerak asztalunkra egy ötszáz-oldalas, tintafoltos, csaknem olvashatatlan kéziratot. Ha kételkedésünket legyőzve elkezdjük olvasni bizonyítását, akkor valószínűleg már az első, egyébként esetleg könnyen kijavítható pontatlanságnál vagy nehezen érthető következtetésnél megállapítjuk, hogy a bizonyítás hibát tartalmaz, s lelkiismeret furdalás nélkül az egészet hibásnak minősítjük. (Tény, hogy sok, ma megoldatlan problémára van forgalomban ilyen tekintélyes terjedelmű, ám kevésbé tekintélyes szerzővel rendelkező érthetetlen bizonyítás.) Mivel a potenciális bizonyítás leírásának külalakja, szerzőjének hajviselete és foglalkozása nem matematikai fogalmak, ezért eljárásunk matematikailag nem igazolt.

Tegyük föl, hogy a hozzánk beállító úr az algebrai geometria legfrissebb eredményeivel tisztában lévő, sok elismert cikkel rendelkező matematikus, aki szabatos bizonyításairól és eredeti ötleteiről ismert. Ha ő teszi le a nagy Fermat-sejtés bizonyítását asztalunkra, akkor nyilván nagyobb lelkesedéssel vetjük magunkat a bizonyítás ellenőrzésébe. Sőt, talán még azelőtt, hogy igazán meggyőződtünk volna a bizonyítás helyességéről, hajlamosak leszünk ilyen kijelentéseket tenni: „úgy tűnik, hogy XY bebizonyította a Fermat-sejtést”. E szituáció nem kitalált jellegű: 1988 elején elterjedt a híre, hogy az algebrai geometria új, nagyon mély – és csak specialisták által követhető – eredményeinek fölhasználásával sikerült a Fermat-sejtés bizonyítása. A bizonyításnak tekintélyes matematikusok is hitelt adtak: 1988 márciusában Ronald Graham a New York Timesnak pozitívan nyilatkozott az „eredményről”. Később azonban kiderült, hogy a bizonyítás hibát tartalmaz.

Mit tehetünk, ha előttünk van egy állítólagos bizonyítás, amelyet – kétséget kizáróan – ellenőrizni szeretnénk? A feladat megoldása – elvileg – egyszerű: soroljuk föl az axiómákat valamint az általunk valamilyen okból bizonyítottnak elfogadható tételeket (például a tárgy elismert kézikönyveiből), és – Frege „fogalomírásához” hasonlóan – formalizáljuk a bizonyítást, majd lépésről lépésre ellenőrizzük a következtetéseket. Ha megkapjuk a konklúziót, s föltesszük, hogy a következtetési szabályokat jól ellenőriztük, akkor elfogadhatjuk a bizonyítást.

A fönti eljárással elvileg mindenki egyetért, gyakorlatilag azonban senki nem követi ezt az utat, éspedig két okból: egyrészt a bizonyítás átírása és ennek ellenőrzése hihetetlenül munkaigényes eljárás lenne, másrészt legtöbbször úgy tűnik, hogy szükségtelen is, hiszen a bizonyítást érthetetlenné tenné, s a bizonyítás „úgyis” ennek a végtelenül precíz leírásnak elfogadott rövidítésekkel leírt változata. Azonban, amikor lemondunk a bizonyítás teljes formalizálásáról, egyszersmind annak mechanikus ellenőrizhetőségéről is lemondtunk; sőt valószínű, hogy a bizonyítás csak a specialisták számára lesz követhető.

Tegyük föl, hogy valaki teljesen formalizált, így mechanikusan ellenőrizhető bizonyítást tesz le az asztalunkra, 500 oldal terjedelemben. Ekkor helyzetünk abból a szempontból előnyösebb, hogy nem kell szakembernek lennünk az illető területen, csak mechanikusan kell verifikálnunk a következtetéseket. Ha eltekintünk attól, hogy tévedhetünk a verifikálásban, akkor néhány napi munka után dönthetünk az előttünk fekvő bizonyítás helyességéről. Használhatunk számítógépet is az ellenőrzéshez, azonban ekkor sem lehetünk teljesen biztosak az eredményben, mivel a számítógép is hibázhat.

Nem teljesen formalizált bizonyítás esetében azonban valószínűleg a legjobb, amit tehetünk, hogy a lehető legalaposabban megvizsgáljuk a bizonyítás helyességét, majd megkérjük a szakterület néhány jeles képviselőjét, hogy olvassák el a bizonyítást. Ha egybehangzóan mindenki helyesnek tartja a bizonyítást, akkor elfogadjuk helyesnek. Mai matematikai közéletünkben ez az elfogadott protokoll, amely természetesen nem elégíti ki a szigorúság követelményeit. Lényeges itt megjegyezni, hogy a hibás bizonyításokat jó hatásfokkal kiszűri ez a rendszer, amit az is alátámaszt, hogy nem derül ki a már régebben széles körben elfogadott bizonyításokról hibás voltuk.

Tegyük föl, hogy megbékültünk azzal a gondolattal, hogy csak a fentiekben vázolt eljárás áll rendelkezésünkre egy – közönséges, tehát nem teljesen formalizált – bizonyítás helyességének eldöntésére. Azonban még ezt az eljárást is megnehezíti vagy akár lehetetlenné teszi a bizonyítás terjedelme. Ide kínálkozik két híres példa az algebrából, a csoportelmélet területéről. Az egyik a híres Feith–Thompson-tétel, amely szerint minden véges (nem-ciklikus) egyszerű csoport rendje páros. Ennek az egyszerűen hangzó tételnek a bizonyítása több száz oldal terjedelmű, s még a specialisták részéről is óriási munkát igényel a végigkövetése. Másik, talán még híresebb példa a véges egyszerű csoportok osztályozása (Gorenstein, Conway és sok más szerző munkája). A bizonyítás megközelítőleg 15 000 oldal hosszú, azonban a véges egyszerű csoportok leírása, atlasza (ami lényegében a „tétel kimondása”) már egy könyvben elfér. Ha egy ilyen bizonyítást tesznek le az asztalunkra ellenőrzés céljából, akkor előbb vagy utóbb be kell jelentenünk, hogy nem tudunk megbirkózni a föladattal – ahogy valószínűleg senki sem tudna az ilyen feladattal egyedül megbirkózni. Ha a matematikusok egy csoportja próbál megbirkózni a föladattal, akkor a munkában részt vevők is kénytelenek lesznek megelégedni azzal a hittel, hogy az egyes fejezetek ellenőrzését végző kollégáik hibátlan munkát végeztek.

Az ilyen óriási terjedelmű bizonyítások ellenőrzése még a személyes ítéletalkotástól is megfosztja a matematikust: nemcsak abban kell bízni, hogy ő, hanem abban is, hogy kollégái nem tévedtek.

Az ilyen nagy terjedelmű és nehezen ellenőrizhető bizonyítások érvényességét helyes némi kételkedéssel fogadnunk. Hasonló a helyzet egy másik híres példával, a négyszín-sejtés bizonyításával. Appel és Haken 1976-ban megmutatta, hogy a bizonyítás visszavezethető néhány ezer alapkonfiguráció ellenőrzésére, így néhány ezer eset vizsgálatára. Az esetek vizsgálatát számítógéppel végezték el. (Megjegyezzük, hogy a térképek 5 színnel való színezhetősége néhány sorban bebizonyítható.) Szigorú bizonyítás-e Appel és Haken munkája? Egyrészt úgy tűnik, hogy nincs elvi akadálya annak, hogy a néhány ezer esetet is „kézzel” ellenőrizzük, csupán a munkára fordítható időnk korlátozott. Így a helyzet hasonló ahhoz, amikor egy terjedelmes bizonyítást kollégáinkkal együtt ellenőriztünk, de itt nem kollégáink tévedhetetlenségében, hanem a számítógép helyes működésében kell hinnünk. Másrészt pedig a helyzet egészen különbözik az előzőektől, hiszen ott legalább részletenként – a hagyományos módon – ellenőrizték a bizonyítást, itt pedig a számítógépet úgy ellenőrizték, hogy egy másik számítógépen, egy független program segítségével megismételték a számolást.

Azonban az ilyen érvelések: „a kísérlet többször megismételve is ugyanazt az eredményt adta, tehát következtetésünk helyes” a természettudományok és nem a matematika érveléséhez tartozik. De a matematikus szempontjából, aki tegyük föl, egy tétel bizonyításához föl akarja használni a négyszín-tételt vagy a véges egyszerű csoportok osztályozását (mivel nem tudja bizonyításukat maga ellenőrizni), mindkét tétel gyanús lesz, és saját bizonyított tételével szemben is – jó esetben – kétségei lesznek. A fönti bizonyítások ellenőrzésének elvi akadálya azonban nincs.

III. „Bizonyításokról”, amelyek talán meggyőznek, de mégsem bizonyítanak

E dolgozat írásának idején nem ismert (az input méretében) polinomiális idejű algoritmus a gráf-izomorfizmus problémára, azaz a következő probléma eldöntésére: adott két gráf, n csúcson: G és G’. Igaz-e az, hogy G’ csúcsait megfelelőképpen jelölve (a csúcsok neveit permutálva) pontosan G-t kapjuk meg?

Ehhez a problémához kapcsolódik példánk is. Tegyük föl, hogy Artúr király nem tudja eldönteni két kedvenc gráfjáról, G-ről és G’-ről, hogy izomorfak-e. Megkérdezi a kerekasztal lovagjait, de ők sem tudnak segíteni. Ekkor hívatja Merlint, a nagy varázslót, és nekiszögezi a kérdést: G izomorf-e G’-vel? Merlin – mivel nagy varázsló, s így olyan kérdésekre is könnyen tud válaszolni, amelyek eldöntésére nem ismert polinomiális algoritmus – elvonul szobájába, majd kisvártatva megjelenik és válaszol a királynak. Azonban Artúr nem hisz teljesen az öreg varázslónak, bizonyítékot is követel tőle. Merlinnek könnyű dolga van, ha G és G’ történetesen izomorfak: megadja az izomorfizmust, azaz a bizonyítását annak, hogy G és G’ izomorfak. Ennek a helyességét már Artúr is könnyen (polinom időben) ellenőrizni tudja. Tehát Melin izomorf gráfok esetében – polinom hosszúságú – bizonyítást tud adni állítására.

A baj akkor kezdődik, ha Merlin – varázslatai segítségével – megállapítja, hogy G és G’ nem izomorfak. Ugyanis ekkor – általános esetben – nem ismeretes az, hogy létezik-e polinom hosszú bizonyítás arra, hogy G és G’ nem izomorfak. (A polinom hosszúság itt természetesen föltétel, mivel már százpontú gráfokra is mondjuk az összes lehetséges G és G’ közötti leképezés felsorolása is már exponenciálisan hosszú, tehát ezek nem-izomorfizmus voltának megmutatása messze meghaladja Artúr életének hosszát.) Mit tehet ekkor Merlin? Babai [B], valamint Goldwasser, Micali és Rackoff [GMR] szerint – jelenlegi tudásunk szerint – az a legjobb, ha a következő játékot javasolja Artúrnak:

A játék több fordulóból áll. Egy forduló leírása a következő:

Artúr – Merlintől rejtve – feldob egy érmét, ha fej, akkor G’-t, ha írás, akkor G-t választja ki. Ezek után választ egy véletlen π permutáció, s ezt alkalmazza a kiválasztott gráf csúcsaira, majd az így kapott gráfot odaadja Merlinnek. Neki pedig ezek után azt kell megmondania, hogy G és G’ közül melyik volt a kiindulási gráf.

Ha G és G’ izomorfak, akkor Merlin nem tehet mást, mint hogy véletlenül találgat. Így t forduló után annak a valószínűsége, hogy mindig a helyes választ adta meg, csak 2t. Ha tehát t forduló után azt kapta Artúr király, hogy Merlin mindig helyesen válaszolt, akkor 2t a valószínűsége annak, hogy G és G’ izomorfak, és 1–2t a valószínűsége annak, hogy nem izomorfak. Az eljárás nyilván nem ad bizonyítást, csak bizonyos statisztikai érveléssel támasztja alá azt a hipotézist, hogy G és G’ nem izomorfak. Viszont Artúr számára a hiba valószínűsége könnyen kiszámítható és a valószínűségi verifikálási eljárás gyors. Ha viszont Merlin leírja egy óriási könyvbe az összes lehetséges, G és G’ közötti leképezést, annak bizonyításával együtt, hogy ezek nem izomorfizmusok, s a könyvet átadja Artúrnak, akkor Artúr kezében lesz egy – Frege által is elfogadható – bizonyítás, amelyet azonban – terjedelme miatt – nem tud verifikálni. Így annak a valószínűsége, hogy Merlin – ezt kihasználva – becsapja királyát, akár 1 is lehet.

A fönti Artúr–Merlin típusú „bizonyítás” a jól becsülhető hibavalószínűség miatt igen meggyőző, azonban Artúr sajnos semmivel sem kerül közelebb néhány forduló után ahhoz, hogy meg tudjon adni egy valódi bizonyítást.

Kellemetlen választás előtt áll a ma matematikusa. Vagy elveti – vagy legalábbis nem alkalmazza – mindazokat a tételeket, amelyek bizonyítását önmaga nem tudja elfogadható időn belül ellenőrizni, vagy elfogadja azokat, amelyeket emberek valamikor, valahol ellenőriztek, elfogadja a négyszín-tétel bizonyítását és – elég nagy t-re – akár a fönti Artúr–Merlin-féle bizonyítást is… Nehéz a választás a következetes szigorúság és amaz igény között, hogy igen nehéz problémákat is meg akarjunk és tudjunk közelíteni.

Gödel nem-teljességi tétele lerombolta azt az illúziót, hogy a matematika végső, biztos alapokra helyezhető, de úgy tűnt, hogy megmarad legalább a szigorú bizonyítás tudományának. A szigorú bizonyításokkal kapcsolatos fönti problémák tükrében úgy tűnik, hogy ez is csak egyre kevésbé valósítható meg.

Magyar Filozófiai Szemle
  • [B] Babai László: Trading Group Theory for Randomness. = Proceedings of 17th Symposium on the Theory of Computation. Providence/Rhode Island 1985.
  • [C] Haskell B. Curry: Foundations of Mathematical Logic. McGraw-Hill 1963.
  • [DH] Philip J. Davis – Reuben Hersh: A matematika élménye. Műszaki Könyvkiadó, Budapest 1984.
  • [F] Gottlob Frege: Logika, szemantika, matematika. Gondolat, Budapest 1980.
  • [GMR] Shafi Goldwasser – Silvio Micali – Charles Rackoff: The Knowledge Complexity of Interactive Proofs. = Proceedings of 17th Symposium on the Theory of Computation. Providence/Rhode Island 1985.

On Mathematical Rigorousness

Vince Grolmusz

It was a common view among 19. century mathematicians that a theorem is absolutely true and should have been regarded as proved if the proof had been “logically rigorous”. But the criteria of this rigorousness depend on the intuitions of the mathematicians. Paradox a such as those of Russell and Cantor undermined this view as well as Frege’s formalized system. As to the fact that there are “proofs” which prove but don’t convince us and there are ones which are convincing but don’t prove anything, the author argues it is an illusion to regard mathematics as a science of rigorous proofs.

Magyar Filozófiai Szemle 1992/1–2, 9–15. p.

Lovász László et al: Arthur király udvarában