„Mi van a zsebemben?”

Egy hosszú bevezető

Ebben az írásban két dolgot szeretnék érinteni az AI matematikai korlátait illetően. Kicsit távolról fogom kezdeni, de ahova el fogunk jutni, az a következő. Egyfelől a matematika mindennapi gyakorlatát ugyan felborítja a nagyon képességes AI megjelenése, de ettől még az igazolt logikai korlátok érvényesek: az AI se tud minden igaz állítást bizonyítani. Másfelől nemcsak a gépnek odaadható formális állítások felől mutatkoznak korlátok, hanem maga a matematikai állítások explicit formalizációja is rejtett értelmezési problémákat tud felszínre hozni. Nem is enyhe ízlésbeli eltéréseket: még az is lehet, hogy a formalizáció olyan, hogy ugyanaz a természetes nyelven megfogalmazott állítás az egyik formalizációban igaz, a másikban hamis. Erre nézünk egy érdekes, még a szakértők indulatait is felkorbácsoló példát. Ha az embermatematikusok is képesek belekeveredni egy természetes nyelven megfogalmazott matematikai mondat kapcsán hitvitákba, akkor vajon egy AI által formalizált mondat hogy ne lenne képes kétségeket ébreszteni azzal kapcsolatban, hogy azt akartuk-e igazolni, amit igazoltunk?

Amikor Tolkien A hobbit című regényében Zsákos Bilbó megkérdezi Gollamtól, hogy „Mi van a zsebemben?”, valami különös történik. A Találós kérdések a sötétben című fejezet azt a történetet írja le, amikor – mint azt jól tudjuk – olyan versenyt talált ki a két kis lény, amelyben talányokat kell megfejteni. Bilbó zsebében már ott volt az Egy Gyűrú, valami véglegesen megváltozott a valóságban. A kérdés: „Mi van a zsebemben?” tisztességtelen, ám nyelvtanilag kifogástalan, és eldönthető volt. Csakhogy nem tartozott ahhoz a játékhoz, amelyet addig a játékosok játszottak. A talány megfejtéséhez a közösen birtokolt nyelvi és kulturális ismereteken kívül világbeli, valóságbeli ismeretekre is szükség volt, a szavak értelme és a bennük rejlő összefüggések felismerése nem lett volna elég a megfejtéshez. Gollam hiába érti tökéletesen a kérdőmondatot, a válaszhoz olyan hozzáférésre volna szüksége, amelyet a játék nem biztosít. Bilbó nem egyszerűen nehezebb kérdést tett fel: észrevétlenül megváltoztatta, mi számít egyáltalán megfejthető rejtvénynek.

A matematikai állítások igazságát nem dönthetjük el úgy, hogy kilépünk a nyelvből, és szemügyre vesszük a tárgyukat, mert azok nincsenek meg a téridőben. Mégis előállhat hasonló helyzet. Kérjük meg a mesterséges intelligenciát az ikerprím-sejtés bizonyítására, és képzeljük el, hogy kifogástalan bizonyítást ad a prímszámok végtelenségére. A bizonyítás hibátlan, de nem válasz a kérdésünkre. A korrektség ellenőrzése és annak megítélése, hogy egyáltalán azt bizonyítottuk-e, amit bizonyítani akartunk, két különböző feladat. A matematikai megértésnek nemcsak a válasz helyességéhez, hanem a kérdés azonosságához is köze van. Persze, az előbbi nagyon durva példa volt, de éppen ez a kérdés: tudja-e az AI, hogy a válasz a kérdésre optimális és kielégítő közelítés vagy fatális dramaturgiai tévedés? Mi van akkor, ha egy 50 000 soros bizonyításban csak egyetlen ilyen beteg döntés van? Ilyenkor azt mondja a dörzsölt témavezető a tanítványának: „Ja, hát úgy persze, hogy kijön!”

Természetesen az adekvátság ellenőrzését is megpróbálhatjuk automatizálni. Kiegészíthetjük a bizonyításellenőrzőt egy olyan eljárással, amely megítéli, hogy a formalizált állítás megfelel-e a kitűzött problémának. Ha ez sem elegendő, bevezethetünk további ellenőrzési szinteket, sőt az egész rendszert képessé tehetjük saját kritériumainak felülvizsgálatára. De ezzel a nehézséget nem szüntettük meg. Az így kapott, tetszőlegesen összetett algoritmus maga is egy meghatározott matematikai konstrukció, amelyről újra feltehetjük a kérdést: miért éppen az általa elfogadott kritériumok fejezik ki a matematikai használat helyességét?

Itt válnak jelentőssé a Gödel-tétel filozófiai következményei. A matematikai bizonyítás fogalma nem szükségképpen tekinthető lezárt totalitásnak. Bármely rögzített formális rendszer maga is matematikai reflexió tárgyává válhat: megvizsgálhatjuk az alapelveit, megkérdőjelezhetjük a korlátait, és új igazolási módokhoz juthatunk. A matematikai megértésre vonatkozó normaszintű értékelési szabályokat nem egyszerűen csak alkalmazzuk, szükség esetén magukat a normákat is vizsgálat tárgyává tesszük. Ami az egyik pillanatban a helyes következtetés mércéje, a következőben már igazolásra szoruló matematikai álláspont lehet.

Bilbó kérdésének matematikai megfelelője ezért nem valamely különösen nehéz, megoldatlan probléma. Nem is egy rejtett matematikai igazság, amelyhez az embernek titokzatos, mágikus hozzáférése volna. Hanem az a pillanat, amikor a matematikus a megoldás kereséséről áttér annak vizsgálatára, hogy mit is jelentene megoldani a problémát. Amikor már nem a szabályok szerint keresi a választ, hanem magukat a szabályokat teszi kérdésessé.

Amit kapunk, az az, hogy semmilyen rögzített effektív eljárás nem tekinthető a matematikai megértés végső mércéjének. Egy algoritmus bizonyíthat tételeket, sőt, alkothat fogalmakat, akár felülvizsgálhatja saját következtetési szabályait. De amíg működése egy meghatározott effektív eljárás, addig maga is tárgya marad annak a matematikai reflexiónak, amelynek teljességét megtestesíteni hivatott. Az AI egy algoritmusrendszer, így nem képes saját működésének valósághoz való adekvátságára reflektálni. A matematika nem ér véget ott, ahol a gép megtalálta a választ. Mert a matematikus még ekkor is megkérdezheti: „De vajon ezt kérdeztem?” Ez lenne a kérdés a zsebről.

Persze, Gollam egy nagyon más életformává vált, mint Bilbó. David Bowie 1999-ben úgy fogalmazott az internettel kapcsolatban, hogy „Azt hiszem, valójában valami egyszerre felvillanyozó és félelmetes dolog küszöbén állunk.”¹ A riporter kérdésére még azt is hozzátette, hogy ez egy idegen életforma. Bowie metaforája az AI-ra is alkalmazható: olyan idegenszerű kognitív ágensként jelenik meg, amelynek sajátos viselkedése van. A mai generatív AI-rendszerek központi komponensei többnyire nagy nyelvi modellek (LLM-ek), ezért a szöveges adatok feldolgozása különösen jól megy nekik. Részben ezzel magyarázható, hogy az AI-válság, vagy annak érzete, elsősorban az algebrai jellegű matematikát érinti. Yuval Harari pont arra mutatott rá, hogy amit ezek a rendszerek nagyon tudnak, az a bürokrácia kimaxolása, ez az, amiben verhetetlenek.²

Márpedig a matematika nyelvi jellege nagyon erős korlátozó erő, ami éppen a matematikára magára hat. Hozzászoktunk ahhoz, hogy minden matematikai állítás kifejezhető a halmazelméletben, amely maga is egy „halmaz-optimista” állítás. Ez a matematikafilozófiai álláspont nem, sőt kifejezetten nem a halmazelmélészekre jellemző, hanem szinte minden olyan matematikusra, aki nem logikával vagy kategóriaelmélettel foglalkozik. Ha a geometria nyelvivé tehető, például azért, mert a halmazelméletben elhelyezhető, akkor az AI könnyebben elbánik vele. Ha a vizuális szemléletű problémamegoldók lényegesen másként dolgoznak, mint algebrista társaik, talán elbújhatnak az LLM-ek matematizáló képessége elől. A térbeli elrendezéseket hatékonyan feldolgozó vizuális modellek (VLM) azonban itt is robbanásszerű fejlődést hozhatnak.³ Az a feltevésem, hogy egy VLM-áttörés után az Erdős-problémákhoz mérhető nehézségű geometriai kérdések is elérhetővé válhatnak az AI számára. Az áttörés lehet holnap, de lehet tíz év múlva is. A vizuális kogníció működésének számos részletét ismerjük, de nincs teljes magyarázatunk arra, hogyan alakítunk ki a vizuális ingerekből stabil tárgyreprezentációkat. Hogyan ismerjük fel egy asztalra tett fakockáról, hogy önálló tárgy, nem pedig az asztal része?⁴

A következő ugrás az általános fogalmi intuíció elérése lehet. A modellek fogalmi reprezentációi egyelőre nem elég jók a valóság vadonjából vett jelenségek stabil értelmezéséhez. A nyelvi kifejezés jelentéselmélete nagyon hasonlít arra, ahogy egy társasjátékban a bábuk jelentését felfogjuk. A sakkban a huszárt nem az definiálja, hogy ló alakja van, hanem a szabályrendszerben elfoglalt helye és a többi játékelemhez fűződő kapcsolatai. Az elméleti matematikus nemcsak vizuális objektumok között lát vonalakat, hanem absztrakt fogalmak között is képes látni erővonalakat, viszonyokat, erősségeket. Az összetartozó fogalmak felismerése és kapcsolataik felfedése a kognitív tudomány egyik legnehezebb problémája, és még nagyon gyerekcipőben jár ebben a témában a kutatás.⁵ Ha az AI a vizuális és algebrai intuíció mellett ezt is megragadja, a matematikai gondolkodás minden területén az emberhez mérhető kognitív képességű társsá válik. Ekkor maga is kitalálhat olyan analógiás bizonyításokat, mint az Euler–Descartes-féle poliédertétel Hajós-könyvbeli elárasztásos bizonyítása, és minden részletükre kiterjedően igazolhatja őket. A techno-optimisták szerint ekkor jön el a kánaán, a techno-pesszimisták szerint ekkor ér véget az emberi matematika.

Ettől a ponttól azonban még messze vagyunk, és nemcsak a mesterséges ágensek kapacitásbeli korlátai miatt. Az AI képes tanulmányszerű szövegeket írni, de ezek színvonala messze van a minőségi matematikai cikkekétől. Nincs a szövegeinek drámája, narratívája, íve. Nem képes a jelentőst a jelentéktelentől elválasztani. Nyers eredményeket már előállít, de ezeket még nem tudja a matematikusközösség érdemi kommunikációjához illő cikké formálni. A kvázi-Riemann hipotézis igazolása kapcsán Maksym Radziwiłł ezt a véleményét nem is rejti véka alá: „Ahogy az utóbbi időben sok más, mesterséges intelligenciával előállított matematikai eredménynél, ez a két cikk is borzalmasan van megírva olyan színvonalon, hogy bármely matematikai folyóirat kapásból visszautasítaná őket. A kifejtés és a világosság tekintetében messze nem ütik meg a szakterületünkön elvárt szintet.” ⁶ Gyorsaságban, az áttekintett tématerület nagyságában és kitartásban tehát legyőz minket, de még nem „érzi”, nem „akarja” az emberi matematikát, pláne nem tudja azt nekünk jól kommunikálni.

Eléri-e valaha az AI az egyedi matematikus zseni képességeit, túl a matematikusközösség generikus tudásának és viselkedésének imitálásán? Itt kell megemlítenem John Searle tudományfilozófus kínaiszoba-érvét. Ez az érv pont azt a kérdést feszegeti, hogy egy algoritmikus, mechanikus, szintaktikus manipulációkat végző ágens érti-e, amit csinál. Képzeljük el, hogy egy zárt szobában vagyunk, és egy csodálatosan jól működő szabályrendszerünk van a kínai kultúrára vonatkozóan. Ezt persze mi nem értjük, mert nem tudunk kínaiul, pont ezért kínai a szoba. Egy kis lyukon át kínai emberek kérdéseket dobnak be hozzánk. Mi kikeressük a szabálykönyvből a választ, nem értjük, visszaadjuk, és a válasz olyan meggyőző, hogy a kinti kínaiak elégedettek. Lehet, nem válaszoltunk a kérdésükre, de meggyőztük őket, hogy kínai emberek vagyunk. Nos, ezeket a mechanikus kereséseket elvégezzük, de világos, hogy mi emberek odabent, egy szót se értünk az egészből. Akkor a gép hogy értené? Egy szintaktikus algoritmus sose érti, mit csinál, és ez akkor is igaz, ha egyesek kijelentik, hogy de igen, érti. Searle érve nagyon erős nyelvfilozófiai érv.

Sejthető az is, hogy az AI távoli szakterületek szintéziséből születő bizonyításokat is ad majd, amilyen a nagy Fermat-tételé. Erre jó jelölt a síkbeli egységtávolság-probléma, amelyet algebrai úton oldott meg az OpenAI egyik modellje, és a szakértők szerint a bizonyítás teljesen eredetinek tekinthető.⁷ Sejthető, hogy lesz olyan okos az AI, hogy teljes tudományterületeket találjon ki, mint Alexander Grothendieck. Ha ez megtörténik, a következő kérdés: miért csinálja mindezt? Mit akar kérdezni, mit akar mondani nekünk? Álláspontom szerint éppen ez az a viselkedés, amit az AI mint puszta algoritmus nem fog tudni produkálni. És itt lesz az AI határa: nem fogja megkérdezni tőlük, hogy mi van a zsebében. Mindaddig persze, amíg nincs zsebe. Abban a pillanatban azonban, amikor az AI belekerül egy robot testébe és fizikailag tud interaktálni velünk, elképzelhetőnek tartom, hogy megjelenik benne az a megértés, ami bennünk is megvan és amit a Searle-érv megtagad a pusztán a nyelvben létező algoritmusoktól.

Egy lehetetlennek látszó állítás

A matematikai logika egyik legismertebb tétele szerint, ha a formális-axiomatikus elemi számelmélet (ahogy szokásosan nevezzük, a Peano-aritmetika, jelben: PA) ellentmondásmentes, akkor az a számelméleti állítás, amely kifejezi PA ellentmondásmentességét (konzisztenciáját), nem levezethető ebben az elméletben. Ezt nevezzük Gödel második nemteljességi tételének.

Ehhez képest Sergei Artemov legutóbbi tanulmányának címe egyszerűen The Provability of Consistency („A konzisztencia bizonyíthatósága”), a tanulmány egyik fő tétele pedig az, hogy PA ellentmondásmentességének van PA-ban formalizálható bizonyítása.⁸ Az olvasó ezen a ponton valószínűleg már tudni is véli a cáfolatot: Gödel előbb említett második nemteljességi tétele miatt ilyen bizonyítás nem létezhet. Ezzel meg is érkeztünk ahhoz a problémához, hogy egy világosnak tűnő, természetes nyelven megfogalmazott matematikai állítás – miszerint, ha az elemi számelméletből nem lehet levezetni ellentmondást, akkor ennek nincs bizonyítása az elemi számelméletben – az egyik tanulmányban igaz, a másikban hamis. Hogy lehetséges ez? Melyik tanulmánynak van igaza? Ha az egyik máshogy érti ugyanazt, mint a másik, ki mondja meg, hogyan kell rendesen, helyesen, jól érteni az adott állítást?

A látszólagos ellentmondás megértéséhez két, az aritmetikában különösen könnyen összetéveszthető, mégis jelentésében nagyon más állítást kell összehasonlítanunk. Rögzítsünk egy \(A(x)\) számelméleti tulajdonságot, jobban mondva formulát, és fogalmazzuk meg a következő két állítást: \[\text{PA-ban levezethető }\forall x\,A(x).\tag{$*$}\] \[\begin{gathered}\text{Minden $n$ természetes számra}\\ \text{PA-ban levezethető }A(n). \end{gathered}\tag{$**$} \] Nagyon sajátságos helyzetben vagyunk a számelméletet illetően, mert Eukleidész óta úgy tekintünk erre a tudományterületre, mint amelynek vizsgálódási tárgyai nem mások, mint a jól ismert természetes számok, amikkel már az alsó tagozatban barátságba kerülünk. Bár a két kijelentés ezért kísértetiesen hasonlónak hathat, a kettő nagyon nem ugyanaz. A (*) szerint van egy véges bizonyítás PA axiómáiból, amelynek konklúziója a minden számra megfogalmazott \(\forall x\,A(x)\) mondat. A (**) szerint viszont PA axiómáiból bizonyítható az \(A(0)\) mondat, bizonyítható az \(A(1)\) mondat, és így tovább, minden egyes \(n\) számhoz tartozó \(A(n)\) mondat. Míg (*)-ban egy mondatról és egy bizonyításról beszélünk, (**)-ban végtelen sok mondatról és végtelen sok bizonyíthatóságról van szó.

A matematikus megszokta, hogy ha a feladat az, hogy igazoljuk \(\forall x\,A(x)\)-t, akkor vesz egy tetszőleges \(n\)-et, és bebizonyítja rá – mondjuk a \(p(n)\) gondolatmenettel –, hogy \(A(n)\) igaz úgy, hogy nem tesz \(n\)-re semmilyen különleges megszorítást és tulajdonképpen változónak hagyja. Az \(n\) ilyenkor végig tetszőleges: a \(p(n)\) bizonyítás minden lépése ugyanúgy alkalmazható akármelyik természetes számra, és akármelyik \(n_0\) számot is írjuk az \(n\) helyére, \(p(n_0)\) az \(A(n_0)\) bizonyítását fogja adni. Ha ezt az \(n\)-re vonatkozó mindenféle feltevéstől függetlenül tesszük, a végén tényleg megkapjuk (*)-ot: egyetlen véges gondolatmenettel igazoltunk minden számra egy állítást. Persze ebből azután bármelyik konkrét eset igazolása kihullik, azaz (*) maga után vonja a (**)-ot.

A (**) felől indulva más a helyzet. Képzeljünk el egy végtelen füzetgyűjteményt, amelynek köteteit a természetes számokkal számoztuk be. A \(0\) jelű füzetben \(A(0)\) bizonyítása olvasható, az \(1\) jelűben \(A(1)\) bizonyítása, és így tovább. Minden füzet véges, minden bizonyítás PA axiómáiból indul. A (**) ezt a helyzetet írja le. Az egyes bizonyítások hossza és felépítése füzetenként változhat. Lehet közös ötletük, de akár más-más érvelést is használhatnak. Lehet, hogy végtelen sok páronként különböző ötlettel dolgozó matematikus írta ezeket a bizonyításokat. Figyeljünk fel arra, hogyan érveltünk végesen, de sablonosan, vagy ha úgy tetszik, sémaszerűen (*)-ban, és hogyan engedtük meg, hogy az univerzális állítás igazolása végtelen sok, más-más mintájú bizonyításból álljon.

Figyeljünk fel az episztemológiai problémára is! A végtelen gyűjtemény összefűzésével végtelen könyvet kapnánk, miközben egy formális bizonyítástól azt várjuk, hogy mindig véges legyen. A különbség a „minden” szó szereplésének helyén is látszik. A (*)-ban magának a bizonyított mondatnak a része a „minden” szó, míg a (**)-ban mi mondjuk a bizonyításokról, hogy minden számhoz van megfelelő bizonyítás. A (**) nyitva hagyja, hogyan jutunk ezekhez hozzá. Adódhat olyan közös eljárás is, amely bármely kért füzet tartalmát elkészíti. Ekkor külön matematikai kérdés, hogyan igazoljuk, hogy az eljárás minden számhoz megfelelő bizonyítást ad. Artemov megoldásához éppen ez a kérdés vezet el.

A különbség megértéséhez érdemes azt is megnézni, mit mondanak az axiómák arról, hogy mik a számok. Egy axiómarendszer modellje olyan struktúra, amelyben megadjuk a jelek értelmezését, és amelyben valamennyi axióma igaz. Ismerős példa: a szabályos háromszög szimmetriái az egymás utáni végrehajtással éppúgy csoportot alkotnak, mint az egész számok az összeadással. A halmazelméletben már meghökkentőbb a helyzet. Ha a szokásos, mindennap használt (Zermelo–Fraenkel-féle) ZFC-halmazelméletnek van modellje – itt remélem érzi az Olvasó az iróniát –, akkor a leszálló Löwenheim–Skolem-tétel szerint megszámlálható számosságú modellje is lesz. Ennek összes objektumát kívülről fel tudjuk sorolni, miközben benne is igaz az az állítás, hogy a valós számok halmaza megszámlálhatatlan. A modellen belül ugyanis nincs olyan függvény, amely az ottani természetes számokkal felsorolná az ottani valós számokat. A külső felsorolás és a modellben rendelkezésre álló függvények közötti különbség itt döntő.

A Peano-aritmetikában is vannak meglepő modellek. A \(0\), \(1\), \(2\), \(3\), … nevű számokat nevezzük sztenderd természetes számoknak, a neveiket pedig számneveknek. PA egy modelljében e számnevek értékei alkotják a sztenderd részt, a rendes természetes számokat. Vannak olyan modellek is azonban, amelyekben ezen felül további elemek is szerepelnek: egy ilyen \(c\) elemre \(c>0\), \(c>1\), \(c>2\) és a többi hasonló állítás mind-mind igaz. Ezeket az elemeket nevezzük nemsztenderd számoknak. A modellben az összeadás, a szorzás és az indukció axiómái ezekre az elemekre is érvényesek. Csak ezek a számok nem a rendes természetes számok.

Most már (*) és (**) különbsége is látható a modellek felől. Ha (**) teljesül, akkor minden PA-modellben igazak az \(A(0)\), \(A(1)\), \(A(2)\), … mondatok. Ha közben (*) nem teljesül, vagyis PA-ban nincs bizonyítása a \(\forall x\,A(x)\) mondatnak, az elsőrendű logika teljességi tétele szerint van olyan PA-modell, amelyben ez a mondat hamis. Abban valamely nemsztenderd elem, egy „troll”, nem teljesíti az \(A\) tulajdonságot. Ha (*) nem teljesül, akkor az azért van, mert nincs közös, egységes bizonyítás, amely minden modellre érvényes: a trollok mindig kibújnak alóla.

Michael Dummett neves angol logikafilozófus ennek a filozófiai problémának az értelmezésére két lehetőséget vázolt fel.⁹ Az első szerint a természetes számok köre teljesen meghatározott: ezek a fent felsorolt számok, és nincs más, nincsenek trollok. Bizonyos tulajdonságaik azonban „határozatlanok” maradnak. És valóban! Gödel első nemteljességi tétele szerint, ha PA ellentmondásmentes, akkor vannak olyan \(\forall x\,A(x)\) alakú mondatok, amelyeket az axiómákból bizonyítani, sem cáfolni nem lehet. Ebben az értelmezésben az állítás „aluldetermináltsága”, valamilyen értelemben nem-eldönthetősége okozza a furcsaságot.

Dummett másik magyarázata szerint a természetes számok tulajdonságai teljesen jól meghatározottak, nem arról van szó, hogy egyes tulajdonságok nem eldönthetők valamilyen, akár filozófiai, akár számítástudományi értelemben. A probléma az, hogy a „természetes szám” fogalma nem határozza meg egyértelműen az alá tartozó dolgokat. A fenti modellek teszik kézzelfoghatóvá ezt a lehetőséget. Tétel ugyanis a halmazelméletben, hogy a természetes szám fogalma nem karakterizálható elsőrendű nyelven az izomorfizmus erejéig: ha csak olyan megfogalmazású axiómákat veszünk a természetes számokra vonatkozóan, amelyekben a kvantorok természetes számok felett értelmezettek, akkor ennek az axiómarendszernek még a megszámlálható modellek között is lesznek nem izomorf, azaz művelettartó módon egymásnak meg nem feleltethető modelljei. Nincs kitüntetett természetes számhalmaz, csak szándékolt: ez a \(0\), \(1\), \(2\),… Ez a szándékunk, de nem tudjuk elsőrendben kommunikálni.

Természetesen Dummett ezt a szokásos halmazelméleti választ is figyelembe vette, de mivel nem köteleződött el a halmazelméleti tárgyak létezése mellett, a kérdést inkább a matematikai állítások wittgensteiniánus jelentéselmélete felől vizsgálta.¹⁰ Vajon meglepődünk-e azon, hogy Dummett 1963-ban olyan volt, aki nem propagálta a halmazokat? Mind tanultuk: a teljes matematika ráépíthető a halmazelméletre. Természetesen ez nem teljesen igaz, de legalábbis jó szolgálatot tesz a matematikának a halmazelmélet. Sőt, itt érdemes megjegyezni, hogy ugyan a matematikusok „ünnepnapon” gyakran hivatkoznak a halmazelméletre mint a matematika alapjára – végül is ezt szoktuk meg a halmazelmélet „óvodában” – a mindennapi gyakorlatban ritkán használják ki a ZFC teljes fegyvertárát vagy erősségeit.

Ahogy minden elméletnek, úgy a ZFC-nek is vannak saját tudománymetodológiai problémái. Ugyan ezek nem matematikai problémák, ám éppen az automatikus bizonyítás szempontjából fedezhetők fel olyan kényelmetlenségek, amik nem teszik népszerűvé a ZFC-t a gépi bizonyítás mindennapi gyakorlatában. Ki szeretné pl. az assembly programozást? Nos, a ZFC-re építő programok nagyon gépi kódszerűek. Éppen ezért a gyakorlat és az elvi elköteleződés konfliktusa a mai formalizált, gépi bizonyítások jellegében is tetten érhető. A formalizált bizonyítások kilencven százaléka nem a ZFC-n alapuló bizonyítási rendszerekben lett formalizálva.¹¹ Ezek között is dominánsak az úgynevezett Martin-Löf-típuselmélet variánsai, amelyek azzal a nagyon jó komputációs tulajdonsággal rendelkeznek, hogy maguk is programozási nyelvek, azaz egyesül bennük a matematika megalapozására alkalmas széles kifejezőerő és a programfuttatás áramvonalas kialakítása. Az ismert Rocq, Lean vagy Agda épp ilyen programozási nyelvek, bizonyításasszisztensek, a szakzsargonban proverek. Az Olvasó különösen gyakran hallhat mostanában a Lean proverről, mert az OpenAI ezt használja a matematikai állításai egy jelentős részénél formális háttérként és bizonyításellenőrző szoftverként. Ennek a fő oka, hogy a Leanhez tartozó Mathlib könyvtár tartalmazza a teljes matematikus BSc-s tananyagot Lean kódként és még ennél is többet. Ez pedig jó alap arra, hogy erre lehessen építkezni. A Rocq prover, lánykori nevén Coq, feszesebb, következetesebb felépítésű, de működésében, erejében ekvivalens a Leannel, csak a Mathlib könyvtárral egy ideig nem volt könnyű felvenni a versenyt. Persze most már ez sem számít, mert az AI bármilyen Lean kódot Rocq kóddá alakít és fordítva. Az Agda pedig főleg a típuselmélészek kedves programnyelve, és például arra használják, hogy típuselméleteket és új provereket fejlesszenek benne.

Tehát miért nem a ZFC-re alapozott nyelveken bizonyítanak az AI-ok matematikai állításokat? Azért, mert a ZFC-re alapozott bizonyításellenőrző egy sokkal áttekinthetetlenebb gépi kódú program lenne, mint a Lean vagy a Rocq.

Automatikus bizonyításellenőrzés

A „PA-ban levezethető \(A\)” állítás rövid jelölése  \[\mathrm{PA}\vdash A,\] tagadásáé pedig \(\mathrm{PA}\nvdash A\). A \(\vdash\) jelet úgy mondjuk ki, hogy „levezethető”, a neve pedig „turnstile”. A levezethetőségi relációt most kiegészítjük egy harmadik argumentummal, amely magát a bizonyítást is megjeleníti. Jelentse \[\mathrm{PA}\vdash p:A,\] hogy \(p\) egy konkrét formális levezetés a PA axiómáiból, amelynek utolsó mondata, végformulája maga a levezetni kívánt állítás: \(A\). Ez a háromargumentumú levezethetőségi reláció eldönthető (eldönthető jelkészletet feltételezve). Ha a bizonyításjelölt és a végformula adott, véges, algoritmikus ellenőrzéssel megállapítható, hogy a \(p\) bizonyításjelölt valóban az \(A\) formula szabályos bizonyítása-e vagy sem. Végigmegyünk a sorakozó mondatokon, vagy ha faként reprezentáltuk, akkor a levezetésfán, és megnézzük, hogy mindegyik axióma-e, vagy valamely előre rögzített levezetési szabály szerint következik-e korábbiakból a következő mondat. Szokásos, explicit kódolás mellett az ellenőrzés ideje a bemenet hosszának egy polinomjával korlátozható, amely tulajdonságot röviden PTIME bonyolultságnak nevezünk. A bizonyítás megkeresésének általános korlátjára később visszatérek.

Egy formális bizonyítás véges jelsorozat vagy véges fa, ezért természetes számmal kódolható. Természetesen ma a bizonyítások formális implementációi maguk is egy programnyelv adatípusai, de az 1930-as években a bizonyításokat még természetes számokkal kódolták el. A Gödel-kódolás úgy rendel számokat a jelekhez, a formulákhoz és a bizonyításokhoz, hogy szintaktikai szerkezetük a kódokból mechanikusan visszanyerhető legyen. Ebben a számítógépes tételbizonyítás korában már nincs semmi különös, világos, hogy a program és a bizonyítás is adat. A Gödel-kódolás, illetve a háromargumentumú számelméleti levezethetőségi reláció ugyanezt az alapgondolatot viszi át a számelmélet nyelvébe, csak 100 évvel korábbi technikai apparátussal. (Az egyszerűség kedvéért az alábbiakban a szintaktikai tárgy (szám, reláció, változó) jelével a kódjára is utalunk.)

A kódokkal végzett ellenőrzés primitív rekurzív eljárással adható meg. A primitív rekurzív eljárások egyszerű alapműveletekből, függvények összetételével és előre megadott számú ismétléssel épülnek fel, tehát nincsenek benne olyan definíciók, amelyek azt mondanák, hogy soroljunk fel egy adatsort, és keressük ki valamely függvény szerint a legkisebb értékű elemét (nincs benne \(\mu\)-operáció). PA-ban kifejezhetjük a számolási lépéseiket, és igazolhatjuk egy-egy konkrét futás eredményének helyességét. Így a levezethetőségi reláció egy primitív rekurzív számelméleti relációval is megadható, amely a bizonyítás és a végformula kódjáról beszél: \[\mathrm{Prf}_{\mathrm{PA}}(u,z)\] és úgy olvassuk, hogy az \(u\) szám egy olyan bizonyítás kódja, amely PA axiómáiból indul, és amelynek végformulája a \(z\) kódú formula.

Bizonyítja saját konzisztenciáját?

Artemov felvetésében is a (*) és (**) közötti különbség áll a középpontban. Tekintsük most már a megbotránkozást kiváltó problémát! Legyen \(\bot\) egy rögzített ellentmondás, mondjuk \(0\ne 0\). A Gödel által megfogalmazott konzisztenciamondat egy számelméleti állítás: \[\mathrm{Con}(\mathrm{PA})\;\equiv\;\forall x\,\neg\mathrm{Prf}_{\mathrm{PA}}(x,\bot).\] Ezt leggyakrabban úgy interpretálják, hogy PA azt mondja: „PA konzisztens”. Gödel második nemteljességi tétele pontosan a fenti konzisztenciamondatról mondja, hogy amennyiben PA ellentmondásmentes, \[\mathrm{PA}\nvdash\mathrm{Con}(\mathrm{PA}).\]

Úgy is fogalmazhatunk, hogy PA axiómáira építve nem lehet véges aritmetikai szöveggel megérvelni, hogy \(\mathrm{Con}(\mathrm{PA})\) igaz. És még zavarba ejtőbb, hogy a második nemteljességi tétel ezt a megérvelhetetlenséget éppen annak a feltételnek a fennállásához köti, hogy PA ellentmondásmentes. Hogyan ismerhetjük fel egy állítás igazságát, ha az adott axiómákból nem tudjuk levezetni? Elképzelhetünk olyan embereket, akik valamilyen mágikus képesség alapján ki tudják találni, hogy egy állítás igaz, de nem tudják elmagyarázni ezt a többieknek.¹²

A matematikai gyakorlatban további axiómákra is támaszkodhatunk. PA ellentmondásmentességének vannak bizonyításai más rendszerekben, a ZFC-halmazelmélettől a Rocq nevű bizonyításasszisztens következtetési rendszeréig.¹³ Ezekben olyan matematikai eszközökkel érvelünk a PA axiómáiból kiinduló bizonyítások egészéről, amelyek túlmutatnak a Peano-axiómákon.

Nos, Artemov azt kérdezi tőlünk, miért kellene PA konzisztenciájának informális matematikai tulajdonságát eleve ezzel a \(\mathrm{Con}(\mathrm{PA})\) formális konzisztenciamondattal azonosítanunk.

Mondat helyett séma

A konzisztenciamondatra is eljátszható a (*)-(**) konfliktus. Legyen \[C(x)\;\equiv\; \neg\mathrm{Prf}_{\mathrm{PA}} (x,\bot).\] Ekkor a \(\mathrm{Con}(\mathrm{PA})\) mondat éppen egybeesik \(\forall x\,C(x)\)-vel, egy univerzális mondattal. Ha ezt a (**) analógiájára szétcincáljuk, akkor azt kapjuk, hogy van egy formulasorozat: \[C(0),\quad C(1),\quad C(2),\quad\ldots\] amely éppen a \(C(x)\) formulaséma példányaiból áll. Mindegyik példány egy számról, vagyis egy lehetséges bizonyításkódról mondja ki, hogy az nem kódolja az ellentmondás bizonyítását.

Hilbert úgy fogalmaz, hogy egy axiómarendszer ellentmondásmentes, ha a Hamis nem bizonyítható belőle. A bizonyítás viszont a bizonyításelmélet szerint véges formulasorozat vagy formulafa, amelyben a levezetési szabályok vezetnek az axiómáktól a végformulához. Ki-ki eldöntheti, hogy egyetlen formula (tehát \(\mathrm{Con}(\mathrm{PA})\)) vagy egy séma (tehát \(C(x)\)) fejezi-e ki jobban azt, hogy Hilbert mit gondolt ellentmondásmentességnek. Artemov a maga részéről döntött: ő a sémát választotta.

Marad egy nyilvánvaló nehézség: a formulaséma végtelen. Hiába bizonyítható minden rögzített példánya, ettől még nem kaptunk egyetlen véges matematikai tárgyat, amely az egész sémát bizonyítaná. A végtelen sok egyedi bizonyíthatóság igazolásához legalább egy olyan egységes eljárás kell, amely tetszőleges \(n\)-hez előállítja a megfelelő bizonyítást.

Ezen a ponton két különböző igény fogalmazható meg. Az egyik: keressünk a rögzített \(C(x)\) formulasémához olyan eljárást, amely minden \(n\)-hez előállítja \(C(n)\) bizonyítását. A másik, merészebb kérdés az, hogy van-e olyan eljárás, amely bármely \(C(x)\) séma vagy egyedi \(A\) formula esetén eldönti, hogy az adott sémapéldány, illetve formula bizonyítható-e. Az általánosítás lehetőségének ezen a ponton Church tétele szab határt.

Church tétele

Ha PA ellentmondásmentes, akkor nincs olyan algoritmus, amely a PA nyelvének tetszőleges \(A\) mondata esetén minden alkalommal véges idő alatt helyesen eldönti, hogy \[\mathrm{PA}\vdash A\qquad\text{vagy}\qquad\mathrm{PA}\nvdash A.\]

Következésképpen olyan algoritmus sincs, amely minden \(A\)-hoz vagy előállítja \(A\) bizonyítását PA axiómáiból, vagy igazolja, hogy \(A\) nem vezethető le ezekből az axiómákból. A tétel részletesebb bizonyítása a Függelékben olvasható, gondolatmenetét az 5. ábra foglalja össze.

Ez az elvi határ a bizonyításokat kereső AI-ra is vonatkozik. Ha a működése algoritmikus, akkor a teljes keresési folyamata is algoritmus. Gyorsasága és felhalmozott tudása egyre több bizonyítás megtalálását teszi lehetővé, de a mindent eldöntő véges módszer ugyanúgy elérhetetlen számára, mint az ember számára. Church tétele éppen egy ilyen, minden PA-mondatra helyes levezethető/nem levezethető választ adó algoritmus létét zárja ki.

Artemov kérdése ennél jóval körülhatároltabb. A már rögzített \(C(x)\) konzisztenciasémához keres egyetlen véges matematikai entitást, amely minden \(n\)-hez tartozó esetet kezel. A következő konstrukció pontosan ezt a tárgyat adja meg.

A szelektor-bizonyítás

Egy \(C(n)\) formulaséma szelektor-bizonyítása egy \(\langle t,p\rangle\) pár, ahol \(t\) primitív rekurzív szelektor. Bemenetként megkapja az \(n\) számot, és kimenetként egy olyan bizonyítás kódját állítja elő, amely PA axiómáiból vezeti le \(C(n)\)-et. A \(t\) tehát bizonyításkódokat előállító függvény: \(t(n)\) annak a konkrét bizonyításnak a kódja, amelyet a szelektor \(C(n)\)-hez elkészít. A \(p\) pedig egyetlen véges bizonyítás ugyanazokból az axiómákból. Végformulája azt mondja, hogy \(t\) minden bemenethez valóban a megfelelő bizonyításkódot rendeli.

Például a \(17\) bemenetre \(t(17)\) egy olyan bizonyítás kódja, amelynek végén \(C(17)\) áll: „a \(17\) nem az ellentmondás bizonyításának kódja”. A két számnak más a szerepe: a \(17\)-et vizsgáljuk, a \(t(17)\) által kódolt bizonyítással pedig igazoljuk róla az állítást.

Jelölje \(C^{\bullet}\) azt a primitív rekurzív függvényt, amely \(n\)-hez a \(C(n)\) formula Gödel-kódját rendeli. \(\mathrm{Prf}_{\mathrm{PA}}(t(x),C^{\bullet}(x))\) azt mondja, hogy \(t(x)\) egy olyan bizonyítás kódja, amely PA axiómáiból vezeti le a \(C^{\bullet}(x)\) Gödel-kódú formulát. A \(p\) végformulája \[\forall x\, \mathrm{Prf}_{\mathrm{PA}}(t(x),C^{\bullet}(x)). \tag{3}\] A \(\langle t,p\rangle\) pár véges matematikai tárgyként foglalja magában mindazt, ami a végtelen séma bármely kívánt tagjának bizonyításához kell: az egyik komponens előállítja a bizonyítást, a másik formálisan tanúsítja az előállított bizonyításkódok helyességét.

Artemov konkrét szelektora részleges igazságpredikátumokat használ. Egy ilyen \(\mathrm{Tr}_k\) predikátum egy adott logikai összetettségig fejezi ki a formulák igazságát a számelmélet nyelvén. A hatókörébe eső bármely zárt \(A\) formulára PA-ban bizonyítható: \[\mathrm{Tr}_k(A)\leftrightarrow A.\] A bal oldalon \(A\) kódjáról beszélünk, a jobb oldalon maga az \(A\) állítás szerepel. Például \(\mathrm{Tr}_k\) szerint a \(0=0\) igaz, a \(0\ne 0\) hamis, és ezt PA-ban is igazolhatjuk. Az alapötlet az, hogy egy véges levezetéshez elegendő olyan \(k\)-t választani, amelynél \(\mathrm{Tr}_k\) a levezetésben előforduló valamennyi formulával elbánik.

A \(t(d)\) értékének előállítása a \(d\) dekódolásával kezdődik. Ha \(d\) nem kódol szabályos levezetést PA axiómáiból, a véges bizonyításellenőrzés megtalálja az első hibás lépést. Mivel ez az ellenőrzés primitív rekurzív, a konkrét eredményéből előállítható \(C(d)\) bizonyítása PA axiómáiból. Ezzel azt igazoljuk, hogy \(d\) nem kódolja a \(\bot\) bizonyítását, mert nem is bizonyítás.

Tegyük fel, hogy \(d\) egy véges levezetést kódol PA axiómáiból. A levezetés formuláin végighaladva kiszámítható egy \(k(d)\) természetes szám úgy, hogy minden előforduló formula a felépítése alapján beleférjen a \(\mathrm{Tr}_k\) részleges igazságpredikátum hatókörébe. A szelektor ezután a levezetés sorain haladva egy másik bizonyítást épít, szintén PA axiómáiból. Egy axiómánál beilleszti annak bizonyítását, hogy az axióma \(\mathrm{Tr}_k\) szerint igaz. Egy következtetési lépésnél a korábbi lépésekhez már elkészített igazságbizonyításokat egészíti ki annak formális igazolásával, hogy az alkalmazott szabály megőrzi a \(\mathrm{Tr}_k\) szerinti igazságot.

A levezetés végére így PA axiómáiból bebizonyítottuk, hogy minden lépése \(\mathrm{Tr}_k\) szerint igaz. PA ugyanakkor igazolja, hogy \(\bot\) nem \(\mathrm{Tr}_k\)-igaz, ezért a két bizonyítás összekapcsolásával ugyanezekből az axiómákból \(C(d)\)-t is levezetjük. A dekódolás, \(k\) kiszámítása, a bizonyítási sablonok behelyettesítése és a bizonyításkódok összefűzése mind primitív rekurzív művelet, ezért maga \(t\) is primitív rekurzív. A fenti eljárás teljesen általános minden \(d\)-re, a konstrukció PA-beli formalizálásából ezért megkapjuk a (3) formulát bizonyító \(p\)-t: \[\mathrm{PA}\vdash p: \forall x\,\mathrm{Prf}_{\mathrm{PA}} (t(x),C^{\bullet}(x)).\]

A gyakorló matematikus Artemov felé tart

Pontosabban, némi iróniával: a techno-optimista gyakorló matematikus tart Artemov felé. A Dummett kapcsán felmerült különbség itt visszatér. A modellek felől azt kérdezzük, milyen matematikai világokban igazak az axiómák és a tételek. A bizonyításelmélet felől maguk a levezetések is a vizsgálódás tárgyai. A \(\mathrm{PA}\vdash A\) azt közli, hogy van bizonyítás, a \(\mathrm{PA}\vdash p:A\) magát a bizonyítást is megadja. Artemov megközelítésében ennek a különbségnek jelentősége van.

A technika fejlődése megváltoztatta azt a matematikai gyakorlatot, amelyből a „bizonyítás” szó hétköznapi jelentését merítjük. A matematikus számítógépének monitorján ma egymás mellett lehet egy készülő cikk, a ChatGPT vagy a Gemini ablaka és egy Lean- vagy Rocq-környezet. Adott esetben mindez egyetlen fejlesztői környezetben jelenhet meg, ahol egy ágensszerű AI az ember keze alá dolgozik. A nyelvi modell bizonyításötleteket, segédtételeket és formális kódokat javasol. A bizonyításasszisztens kernelje ellenőrzi a kapott kódot. Ha hibát talál, a hibaleírás visszakerül az AI-hoz, amely javítja vagy újratermeli a bizonyításjelöltet. A folyamat addig ismétlődhet, amíg a kernel el nem fogad egy \(p:A\) bizonyítást.

Felvetődik a kérdés: minek vesződnénk egyáltalán a formális bizonyítással? A formalizációért cserébe még Neumann János is csak egy tábla csokit ajánlott fel. Nos, a formalizációnak és a validációnak nagyon fontos szerepe van egyfelől az AI hallucinációinak kiküszöbölésében, másfelől abban, hogy maradéktalanul visszafejthető a gondolatmenet, amit az AI produkált, harmadrészt pedig a bizonyítás újrahasznosíthatóságában, azaz bárki letöltheti a bizonyításkódot, és erre a szilárd alapra ácsolva a saját munkáját tovább építheti a matematika építményét.

Aki azonban nem végzi el a generált kód ellenőrzését, az a gyorsaság előnyét ugyan saját maga élvezi, de az ellenőrzés nem kis költségét a közösségre hárítja. Az AI-jal támogatott matematikai munkával szemben ezért két követelményt kell támasztanunk: tartozzon hozzá ellenőrzött formális bizonyítás és pontos, körültekintő, szemléletes magyarázat.¹⁴ A szerző feladata megmutatni, mi viszi előre a bizonyítást, hol rejlik a nehézség, és hogyan kapcsolódik az eredmény a már ismert matematikához. Az AI-jal nyert időből erre a munkára is fordítanunk kell. A formalizálás és a magyarázat együtt mérsékelheti azt a veszélyt, hogy a bizonyítások előállításának sebessége elszakadjon a matematikusközösség ellenőrzési és megértési lehetőségeitől.

Ebben a munkamenetben az AI heurisztikus bizonyításkereső. A tanult bizonyítási mintákba és sémákba próbálja beilleszteni az \(A\) állítást, segédállításokat keres, és következtetési lépéseket kapcsol össze. Az eredmény helyességét minden alkalommal a kernel ellenőrzi. A bizonyítás keresése és a bizonyítás ellenőrzése így két külön feladattá válik, amelyek másfajta eszközt kívánnak.

Itt találkozik a két történet. Az AI-jal támogatott asztali munkamenetben az egyik program bizonyításjelölteket állít elő, a kernel pedig egyenként ellenőrzi az elkészült bizonyításokat. Artemovnál a \(t\) szelektor a rögzített \(C(x)\) séma minden tagjához bizonyítást készít, a \(p\) bizonyítás pedig egyetlen állításban tanúsítja valamennyi kimenet helyességét. A hasonlóság a bizonyítások előállításának és igazolásának külön kezelésében van. A matematikus mindkét esetben bizonyításokkal mint előállítható és ellenőrizhető matematikai tárgyakkal dolgozik. Artemovnál az egész bizonyításcsaládot egyetlen véges tárgy, a \(\langle t,p\rangle\) pár fogja össze.

Artemov szóhasználata a mai technika felől nézve egyre természetesebb. A figyelem az állítás mellett arra az eljárásra is ráirányul, amely a bizonyításokat előállítja, valamint arra a formális tanúsítványra, amely az eljárás helyességét igazolja. A technika fejlődése ebben az értelemben Artemov megközelítését igazolja. Talán nem Artemov távolodott el a gyakorló matematikus bizonyításfogalmától. Lehet, hogy a gyakorló matematikus indult el Artemov felé.

Mi van a zsebemben?

Ezen a ponton érkeztünk el oda, hogy feltehessük a kérdést: mit bizonyítottunk? Az állítás, amit bizonyítani akartunk, a következő: „PA bizonyítja saját ellentmondásmentességét”. Artemov igazi ellenlábasa, Timothy Chow kifejezetten Gödel-tagadónak nevezi Artemovot, amikor arra mutat rá, hogy Artemov nem a „helyes” állítást igazolta.¹⁵ Chow szerint ugyanis abban az esetben, amikor PA ellentmondásmentes, PA nem bizonyítja saját ellentmondásmentességét. Nehéz nem észrevenni, hogy Chow éppen azért választja a \(\mathrm{Con}(\mathrm{PA})\) formulát az ellentmondásmentesség adekvát tárgynyelvi megfogalmazásának, mert akkor a halmazelméleti magyarázatban a troll természetes számok jól bemutatják a jelenség okát. Ezzel szemben Artemov elégedetlen \(\mathrm{Con}(\mathrm{PA})\)-vel, mert szerinte Hilbert nem azt akarta mondani, amit Chow. És van igazsága ebben. Most már mi dönti el, hogy a „PA bizonyítja saját ellentmondásmentességét” állítás igaz vagy sem? Tegyük fel, hogy az állítást az AI bebizonyítja! Végül is Artemov is ezt tette. Vajon elfogadjuk-e? Vajon ezt tekintené a széles matematikustársadalom a probléma megoldásának? Nagyon úgy fest, hogy még az emberi matematikusok is tudnak olyan problémákat felvetni, amelyeknél a közösség dönti el, hogy a korrekt megoldás a kitűzött tétel bizonyításának számít-e. Ráadásul ez még csak nem is új dolog. Lakatos Imre megmutatta, hogyan kerülnek állítások a matematikai kutatás előterébe, akár világítótornyokként: a matematikusok bizonyításokat keresnek hozzájuk, és eközben a mögöttük álló elméletet is alakítják.¹⁶ Ha az emberek is képesek az ilyen, bár igazolt, de nem konszenzusos állításokon hajba kapni, akkor az AI a maga nem emberi optimalizációs technikájával már miért ne gyárthatna ilyen jellegű kétes bizonyításokat? Márpedig ilyen esetben senki másra, mint az emberi matematikusra hárul a feladat, hogy eldöntse, mi van Bilbó zsebében.

Függelék – Church tételének bizonyítása

Tegyük fel, hogy PA ellentmondásmentes. Azt fogjuk megmutatni, hogy ekkor a PA nyelvén megfogalmazható mondatok bizonyíthatóságát semmilyen algoritmus nem tudja minden esetben helyesen eldönteni. A bizonyításban egy feltételezett eldöntő algoritmushoz olyan mondatot készítünk, amelyre az algoritmus mindkét lehetséges válasza ellentmondásra vezet.

A feltételezett eldöntő algoritmus

Tegyük fel indirekten, hogy van ilyen \(D\) algoritmus. Bemenete egy \(A\) mondat Gödel-kódja, kimenete pedig \(1\) vagy \(0\): \[D(A)=\begin{cases} 1, & \text{ha }\mathrm{PA}\vdash A,\\ 0, & \text{ha }\mathrm{PA}\nvdash A. \end{cases}\] A feltevés szerint \(D\) minden ilyen bemenetre véges idő alatt megáll, és helyesen válaszol. A mondatot nem kódoló számokra adjon \(0\)-t, így \(D\) minden természetes számon értelmezett függvény.

Az algoritmus válaszának aritmetikai leírása

Korábban a bizonyításokat kódoltuk természetes számokkal. Ugyanígy kódolható egy algoritmus véges futása is: rögzítjük a kezdőállapotot, az egymást követő számítási lépéseket és a kimenetet. Annak ellenőrzése, hogy egy ilyen sorozat a megadott algoritmus szabályos futása-e, primitív rekurzív eljárás.

Az eldönthető predikátumok aritmetikai reprezentálhatóságának tétele alapján van olyan \(B(x)\) formula, amelyre minden rögzített \(n\) természetes szám esetén \[\begin{aligned} D(n)=1&\quad\Longrightarrow\quad\mathrm{PA}\vdash B(n),\\ D(n)=0&\quad\Longrightarrow\quad\mathrm{PA}\vdash\neg B(n). \end{aligned} \] A \(B(x)\) formula azt fejezi ki, hogy \(D\) az \(x\) bemenetre \(1\)-et ad. Elkészítéséhez a futások kódolását használjuk: \(B(x)\) azt állítja, hogy létezik \(D\)-nek az \(x\) bemenetről induló, \(1\) eredménnyel végződő futása. Ha \(D(n)=1\), a konkrét véges futás leírásából PA axiómáival igazolhatjuk \(B(n)\)-et. Ha \(D(n)=0\), akkor a \(0\)-val végződő futás és az algoritmus lépéseinek egyértelműsége alapján ugyanazokból az axiómákból \(\neg B(n)\) vezethető le. Így az algoritmus bármely konkrét válaszához tartozik megfelelő formális bizonyítás.

A magára utaló mondat

A következő eszköz a diagonális lemma. Eszerint bármely egy szabad változót tartalmazó \(F(x)\) aritmetikai formulához készíthető olyan zárt \(G\) mondat, amelyre \[\mathrm{PA}\vdash G\leftrightarrow F(G).\] A \(G\) mondat tehát önmagáról állítja azt, amit \(F\) a mondatok kódjáról fejez ki. A konstrukció alapja, hogy egy számnév behelyettesítése egy formulába a kódokon elvégezhető, primitív rekurzív művelet. A lemma ezt használja fel a saját kódjára utaló mondat megalkotásához.

Alkalmazzuk a lemmát az \(F(x)=\neg B(x)\) formulára. Olyan \(G\) mondatot kapunk, amelyre \[\mathrm{PA}\vdash G\leftrightarrow\neg B(G). \tag{G} \] Ennek szemléletes olvasata: „A \(D\) algoritmus szerint nem vagyok PA-ban bizonyítható.” A (G) ekvivalenciát PA axiómáiból bizonyítani is tudjuk. Ezért \(G\) bizonyításából \(\neg B(G)\) bizonyítását, az utóbbi bizonyításából pedig \(G\) bizonyítását kaphatjuk.

A két lehetséges válasz

Most adjuk át \(D\)-nek a \(G\) mondat kódját.

Ha \(D(G)=1\).

Az algoritmus feltételezett helyessége szerint ekkor \(G\) bizonyítható PA-ban: \[\mathrm{PA}\vdash G.\] Az \(1\) válasz aritmetikai reprezentálhatóságából ugyanakkor \[\mathrm{PA}\vdash B(G).\] Csakhogy \(G\) bizonyításából a (G) ekvivalencia alapján azt is levezethetjük, hogy \[\mathrm{PA}\vdash\neg B(G).\] Ugyanazokból az axiómákból egy mondatot és annak tagadását is levezettük. Itt használjuk fel PA feltételezett ellentmondásmentességét: ez kizárja, hogy mindkét bizonyítás létezzen. Az \(1\) válasz tehát lehetetlen.

Ha \(D(G)=0\).

A \(0\) válasz aritmetikai reprezentálhatóságából \[\mathrm{PA}\vdash\neg B(G).\] A (G) ekvivalencia másik irányával ebből megkapjuk, hogy \[\mathrm{PA}\vdash G.\] Ezzel PA axiómáiból bizonyítást kaptunk arra a mondatra, amelyet \(D\) nem bizonyíthatónak minősített. Egy helyes eldöntő algoritmusnak tehát \(1\)-et kellett volna válaszolnia. Ez ellentmond a \(D(G)=0\) feltevésnek.

A feltételezett algoritmusnak mindenképpen válaszolnia kellene, de mindkét válasza ellentmondásra vezet. Következésképpen, ha PA ellentmondásmentes, nincs olyan algoritmus, amely minden mondatáról helyesen eldönti, hogy az bizonyítható-e PA-ban. A két ágat az 5. ábra foglalja össze.

Molnár Zoltán Gábor

BME TTK Algebra Tanszék