Methode Meta-Logica:
Beslisbaarheid
Het Onvolledigheidsbewijs van Gödel
[Eerste website versie 08-06-2005;
herziene versie 16-08-2006]
herziene versie 16-08-2006]
Inhoudsopgave
Inleiding.
Een beknopte samenvatting.
(1)
De twee onderdelen van Gödel's onvolledigheidsbewijs.
(2) Mogelijke consequenties van Gödel's bewijs.
(3) Het gebruikte tegenvoorbeeld in Gödel's bewijs.
(4) Een meer formele lezing van Gödel's zin.
(5) Positieve bewijsvoering.
(6) Het probleem van de vicieuze cirkel.
(7) Negatieve bewijsvoering.
(8) De kracht van Gödel's codering.
(9) Het verloop van het formele bewijs
(10) Vraagtekens bij Gödel's bewijs.
(12) Gödel's bewijs en bewustzijn.
(2) Mogelijke consequenties van Gödel's bewijs.
(3) Het gebruikte tegenvoorbeeld in Gödel's bewijs.
(4) Een meer formele lezing van Gödel's zin.
(5) Positieve bewijsvoering.
(6) Het probleem van de vicieuze cirkel.
(7) Negatieve bewijsvoering.
(8) De kracht van Gödel's codering.
(9) Het verloop van het formele bewijs
(10) Vraagtekens bij Gödel's bewijs.
(I) Is Gödel's zin waar?
(II) Is Gödel's zin formaliseerbaar?
(III) Leidt Gödel's nummering tot valide conclusies?
(IV) Past 'bewijsbaar' in het systeem?
(V) Interpretatie van de contradictie.
(11) Gödel's bewijs als weerlegging van A.I..(II) Is Gödel's zin formaliseerbaar?
(III) Leidt Gödel's nummering tot valide conclusies?
(IV) Past 'bewijsbaar' in het systeem?
(V) Interpretatie van de contradictie.
(12) Gödel's bewijs en bewustzijn.
(a) Zijn meta-oordelen afhankelijk van bewustzijn?
(b) Is bewustzijn afhankelijk van meta-oordelen?
(c) Kan een mens wčl over zijn eigen bewijsmogelijkheden oordelen?
(13) Conclusie over Gödel's bewijs en bewustzijn(b) Is bewustzijn afhankelijk van meta-oordelen?
(c) Kan een mens wčl over zijn eigen bewijsmogelijkheden oordelen?
Inleiding.
Het blijkt lastig om een verklaring voor het verschijnsel bewustzijn te vinden - vooral een verklaring die onder wetenschappers algemeen aanvaard wordt. Zou er een absoluut beletsel zijn om de bewuste verklaring te kunnen vinden? Misschien ligt dit probleem in het feit dat we als mensen voor het begrijpen van het bewustzijn hoe dan ook aangewezen zijn op dat zelfde bewustzijn. Om een realistisch beeld te kunnen vormen van het bewustzijn, zou het misschien nodig zijn om er van buitenaf tegenaan te kunnen kijken - om dus tijdelijk 'buiten bewustzijn' te stappen. Maar dan hebben we niet meer het bewustzijn om wat dan ook gewaar te kunnen worden. Dus daarmee komen we niet verder.
Het bewustzijn heeft wel bepaalde zelf-reflexieve vermogens, het kan bijvoorbeeld het besef bevatten: 'ik ben bij bewustzijn'. Maar het kan zichzelf niet volledig 'overzien' of 'doorgronden'. Met een vergelijking: de slang kan zichzelf wel bijten, maar "The snake cannot completely swallow itself by the tail " (John S. Bell, 1973, pp. 687-690; 1987, pp. 41-42).
Kortom, het is misschien wel so wie so onmogelijk om met onze geest, vanuit ons bewustzijn, datzelfde bewustzijn te verklaren. De laatste opvatting wordt vaak geschraagd met een beroep op het zgn. 'onvolledigheidsbewijs' van Kurt Gödel (1931). We zullen hieronder bespreken wat dit bewijs op hoofdlijnen inhoudt, en wat hiervan de conclusies en consequenties kunnen zijn voor het 'bewustzijnsbewijs'.
Een beknopte samenvatting.
Gödel's onvolledigheidsbewijs heeft betrekking op de mogelijkheden en beperkingen van formele systemen, met name bepaalde combinaties van logica en wiskunde. Eerste eis aan een formeel systeem is dat het geen strijdige uitkomsten oplevert. Dan noemen we het consistent. In dat geval zijn de uitkomsten van het systeem voldoende betrouwbaar om stellingen in de 'taal' van dat systeem te toetsen op waarheid of logische geldigheid.
Kurt Friedrich Gödel (1906-1978) heeft in 1931 echter bewezen dat een formeel systeem van de rekenkunde, ook al is het consistent, niet kan beslissen over člke zin die in de taal van dat systeem kan worden geformuleerd - zelfs niet als van zo'n zin vaststaat dat ze waar is. Dat wil zeggen, in elk formeel systeem zijn er welgevormde beweringen mogelijk die waar zijn en tegelijk onbewijsbaar zijn. En dus is zo'n systeem per definitie in logische zin onvolledig.
Bij zijn bewijsvoering maakt Gödel gebruik van een speciaal soort zinnen: nl. formele notaties van stellingen die direct een uitspraak doen over de bewijsbaarheid van zichzelf binnen het formele systeem waarin ze geformuleerd zijn. Zulke zinnen staan dus voor zelf-reflexieve meta-oordelen, en die zijn in het algemeen erg lastig om tot een oplossing te brengen. Het bijzondere van Gödel's aanpak is dat hij een wiskundige techniek heeft gevonden om zelfreflexieve meta-oordelen over een formeel rekenkundig systeem te coderen in de taal van datzelfde systeem: via zijn zgn. 'Gödel-nummering'. Met behulp van deze speciale getalscodering is het Gödel gelukt om formeel aan tonen, in de taal van de rekenkunde, dat de waarheidswaarde van een bepaald type meta-oordeel niet in een formeel rekenkundig systeem kan worden bewezen.
(1)
Kurt Gödel heeft aangetoond dat er onontkoombare (definiete) beperkingen zijn aan formele systemen van de rekenkunde. In zulke systemen wordt een rekenkundige theorie opgebouwd als een zuiver logisch systeem van basisaannamen (axioma's) en afleidingsregels. Gödel's bewijs geldt al voor de meest simpele formaliseringen van de elementaire rekenkunde voor natuurlijke getallen: first-order theory of natural numbers.
De waarde van een formeel systeem ligt in zijn betrouwbaarheid en zijn toepasbaarheid - en die zijn in het algemeen afhankelijk van twee wezenlijke eigenschappen:
In zijn bewijs levert Gödel twee stellingen tegen de mogelijkheid dat formele rekenkundige systemen volledig kunnen zijn - ook al zijn ze consistent.
Deze stelling houdt in, dat elk formeel systeem van de rekenkunde dat consistent is - dus geen onderling tegenstrijdige beweringen oplevert - niet tegelijk volledig is. Dat betekent dat het niet zo is dat elke bewering die in de taal van zo'n systeem geformuleerd kan worden, en waarvan de waarheidswaarde bekend is, ook binnen dat systeem kan worden bewezen (als waar) - of kan worden weerlegd (als onwaar).
Er blijven dus altijd vragen die binnen de taalregels (syntax) van zo'n systeem gesteld kunnen worden, maar waarvan de antwoorden buiten de afleidingsregels (semantiek) van het systeem liggen.
Dit wil zeggen dat een formeel rekenkundig systeem dat consistent is ook niet een bewijs kan leveren voor zijn eigen consistentie.
Beide conclusies gelden ongeacht de mogelijke uitbreidingen, modificaties en innovaties van het systeem: zolang het een formeel rekenkundig systeem is, blijven de verbeteringen beperkt tot een toename in complexiteit, dat is een uitbreiding van combinaties. Ze leiden niet tot een volledige bewijscapaciteit van het systeem: er blijven ware zinnen mogelijk in de taal van het systeem die niet bewijsbaar zijn in het systeem. Dit geldt in ieder geval voor beweringen over het systeem zčlf: die vereisen meta-oordelen (oftewel meta-inferentie ).
(2)
Met name het eerste onvolledigheidstheorema wordt wel aangevoerd om bepaalde opvattingen te schragen over de relatie tussen formele systemen en menselijke cognitieve capaciteiten zoals intelligentie en bewustzijn (zie bijv. R. Penrose, 1994).
Voor deze drie stellingen zijn vele argumenten aan te voeren, waarvan een aantal redelijk steekhoudend zijn. Maar daarbij lijkt Gödel's bewijs niet het meest relevante bewijsmiddel. Hieronder zullen we Gödel's bewijs voering toelichten.
(3)
Het bewijs van Gödel zit nogal ingewikkeld in elkaar maar voor het doel van deze bespreking is het vooral belangrijk dat de hoofdlijn van zijn betoogtrant duidelijk wordt. Gödel voert zijn bewijs in grote lijnen als volgt.
Laten we uitgaan van een denkbeeldig systeem,
De vraag is nu:
Gödel betwist de volledigheid van consistente systemen door naar de 'fatale' uitzondering hierop te zoeken. Het tegenvoorbeeld dat Gödel gebruikt voor zijn bewijs is een heel specifieke zin, de bekende 'zin van Gödel' (zeg Gd [0]), die luidt: 'Deze zin is niet bewijsbaar in dit systeem'.
[2a] Gd[0] : "The system (
Of korter;
[2b] Gd[0] : 'Gd[0] is not provable in
Met andere woorden:
[2c] Gd[0] : 'Gd[0] is niet bewijsbaar in
In meta-logische termen:
[2d] Gd[0] : '¬(
Gd[0])'.
We zien dat zin Gd[0] van dezelfde categorie lijkt als de bekende klassieke Kretenzer paradox, of paradox van de leugenaar, die luidt: 'Ik lieg', of anders gezegd: 'Wat ik zeg is onwaar', of nog preciezer: 'De zin die dit stelt is onwaar'. Deze zin heeft een tweeledige consequentie: Als de zin waar is dan volgt dat zij onwaar is, en als zij onwaar is dan volgt dat zij waar is; beide uiteraard paradoxaal.
Gödel's zin Gd[0] zegt iets soortgelijks, maar niet over waarheid, alleen over bewijsbaarheid. Ook deze zin heeft een tweeledige consequentie: Als de zin waar is dan volgt dat zij niet bewijsbaar is, dus niet als waar kan worden aangenomen, maar als zij onwaar is dan volgt dat zij bewijsbaar is, en dus als waar moet worden aangenomen;
beide eveneens paradoxaal.
Daarbij verwijst ze naar zichzelf (ze is zelf-referentieel) en doet bovendien een bewering óver zichzelf (ze is zelf-reflexief), in ontkennende zin (ze is negatief) met betrekking tot haar bewijsbaarheid in relatie tot systeem
Toch lijkt het paradoxale voorkomen van Gd[0] niet per se tot een contradictie te leiden. Dit blijkt als we kort nagaan welke waarheidswaarde zin Gd[0] kan hebben. Stel dat Gd[0] een zin is die welgevormd is in een systeem
Met andere woorden, de enige logische mogelijkheid is hier dat Gd[0] waar is. Volgens een simpele, intuďtieve lezing lijkt zin Gd[0] als inhoudelijke bewering dus waar te zijn voor elk formeel systeem dat consistent is.
Gödel toetst echter op een formele manier of een willekeurig consistent formeel systeem, te noemen
(4)
In een simpele, 'semi-formele' vorm kunnen we Gödel's zin Gd[0] als volgt weergeven:
In de vergelijking van [3] verwijst de tweede 'Gd[0]' naar de eerste, maar is daarbij ook van een andere orde. Eigenlijk impliceert Gödel met zijn definitie van Gd[0] een nevenstelling van twee formules:
Het verschil tussen Gd[1] en '
Uit deze opsplitsing van Gd[0] wordt duidelijk dat het verschil tussen de eerste Gd[0] (d.i. Gd[1]) en de tweede Gd[0] (d.i. Gd[2]) wezenlijk is. We zullen zien dat dit verschil een cruciale rol speelt in de opzet van Gödel's bewijs.
(5)
De vraag is of het mogelijk is om een formeel bewijs te leveren van de (on)volledige bewijskracht van formele rekenkundige systemen die consistent zijn. Voor dit doel kunnen we onderzoeken of er een zin mogelijk is die welgevormd is in zo'n systeem en waar is, maar tegelijk in datzelfde systeem niet bewijsbaar. Als we hiervoor Gödel's zin (Gd[0]) nemen, dan gaat het er om een formeel bewijs te leveren van de (on)mogelijkheid om voor de ware zin Gd[0] in het betreffende systeem een bewijs te construeren.
Voor een formeel bewijs van een stelling kunnen we in het algemeen twee kanten op: een positieve bewijsvoering of een negatieve. We zullen eerst nagaan of een positieve bewijsvoering iets oplevert voor zin Gd[0].
Een voor de hand liggende methode van bewijzen is zoeken naar positieve aanwijzingen en voorwaarden voor de waarheid van de te bewijzen stelling, deze 'bouwstenen' vervolgens te ordenen in een redeneerketen, en te toetsen of die als een 'bewijsreeks' kan dienen die de beoogde conclusie via logische afleiding oplevert.
Hoe kan zo'n bewijsreeks in elkaar steken? Als eerste kunnen we voorlopig aannemen dat zo'n bewijsreeks voor de te bewijzen stelling in een systeem
Een positieve bewijsreeks voor Gd[0] zal uiteraard minstens één element moeten bevatten, uit de axioma's of bewezen stellingen van
De eindconclusie - in dit geval hetzij 'Gd[0]', hetzij '¬Gd[0]' - zal dus moeten aansluiten op minstens één andere stelling in
De vraag is nu of we voor zin Gd[0] zo'n 'sleutelformule' in
We kunnen dus alleen afgaan op het begrip 'bewijsbaar', maar de waarheid hiervan is met name afhankelijk van de vraag of er al een bewijsreeks voor Gd[0] te vinden is, en daarvoor zoeken we juist aanwijzingen. Omdat we verder nog niets hebben onderzocht zal deze bewijsreeks so wie so leeg zijn.
Voor het overige is er in Gd[0] hoegenaamd géén betekenis, zin of inhoud aanwezig. De zin ontbeert een verwijzing naar inhoud, een 'aboutness' die kenmerkend is voor zinvolle beweringen. Door dit 'betekenis-vacuüm' wordt de zin afgezonderd van alle overige inhouden - axioma's of afgeleide stellingen - die in systeem
(6)
Het bovenstaande kunnen we ook in een meer formele vorm laten zien. Een vereiste voor het formele bewijs is natuurlijk dat een zelf-reflexieve zin als Gd[0] wel in de taal van een formeel systeem
Om te bereiken dat de zin Gd[0] naar zichzelf verwijst (zelf-referentieel is), moet het de mogelijkheid bieden dat we - in termen van de hier gebruikte symbolen - de vermelding van de tekencombinatie '
Uit het voorgaande werd duidelijk dat de zin Gd[0] in feite een klein redeneerschema inhoudt, een algoritme: telkens als we Gd[0] bekijken kunnen we op de plaats van '
Dankzij subformule [5b] kan elke vermelding van '
Om de toepassing van operatie [5b] op Gd[1] uit te drukken, noteren we kortweg:
[6a] Gd[1] ·[(5b)];
[6b] Gd[1] ·['
Op dezelfde manier kunnen we de subformules { (5a),(5b) } van de probleemstelling Gd[0] nu in meta-logische termen formuleren:
(met symbolen '' voor 'formeel bewijsbaar', '¬' voor 'niet'):
Vervolgens kunnen we kijken wat er gebeurt als operatie [6b] wordt geactiveerd.
We zien dat de oorspronkelijke tekenreeks Gd[1] bij elke activatie van operatie [6b] explosief - nl. kwadratisch - wordt uitgebreid. Na elke uitbreiding bevat Gd[1] echter nog steeds dezelfde onbekende bevat, nl. symbool
Overigens zien een vergelijkbaar beeld wanneer we een positieve variant van Gd[0] nemen, zeg H0, waarin de ontkenning ('¬') is weggelaten.
De conclusie is dat Gd[0] niet (rechtstreeks) bewijsbaar is in
Het probleem is alleen dat het laatste een inhoudelijke conclusie achteraf is, die gebaseerd is op een zinvolle, dus 'betekenisvolle', dus interpretabele inhoud van Gd[0] - en daarvoor konden we nu juist geen formele elementen vinden in
Om een voorbeeld te noemen: een computerprogramma zou na een onderzoek van Gd[0] wel kunnen concluderen: (1) 'Gd[0] is niet te interpreteren', bijvoorbeeld door voor elke lus die geactiveerd wordt te testen of het daarvoor een ontsnappingstest kan vinden. Op basis daarvan kan het dan ook antwoorden: (2) '(dus) Gd[0] is niet bewijsbaar'. Maar het kan vervolgens niet tot de conclusie komen: (3) 'Gd[0] is waar', omdat het immers geen materiaal heeft gevonden om Gd [0] te 'begrijpen'. Dan kan het systeem ook niet aannemen dat Gd[0] inhoudelijk waar is. De aanname van een ware Gd[0] moet echter binnen het systeem mogelijk zijn om de vraagstelling van Gödel formeel te kunnen beantwoorden.
De weg van positieve bewijsvoering levert dus niets op.
(7)
De andere mogelijkheid is om, zoals Gödel doet, niet naar de mogelijke premissen maar naar de mogelijke consequenties van de aanname van Gd[0] als waar of onwaar te kijken.
Een 'secundaire' methode van bewijzen bestaat uit het systematisch testen en uitsluiten van alternatieve mogelijkheden, net zolang totdat de beoogde conclusie als enige logische mogelijkheid overblijft. De bedoeling is hierbij om het bewijs te leveren via negatieve bewijsvoering (falsificatie, refutatie): door weerlegging van het tegendeel of 'omgekeerde' van de te bewijzen stelling, middels afleiding van een contradictie ( reductie ad absurdum).
Het is bij deze methode dus voldoende om twee tegengestelde beweringen af te leiden op de hoofdlijn van redenering. Deze hoeven niet per se geďnterpreteerd te zijn in termen van basiselementen van systeem
Deze benadering lijkt bij uitstek geschikt voor de beoordeling van zin Gd[0] en haar afleidbaarheid uit
Deze aanpak is wel afhankelijk van diverse andere vooronderstellingen.
Eerste aanname is dat het waarheidsoordeel van systeem
(8)
Gödel omzeilt het probleem van de oneindige interpretatie (als gevolg van eindeloze recursieve uitbreiding) door de eerdergenoemde substitutie-operatie grondig te wijzingen. Om in bovenstaande terminologie te spreken: met Gödel's substitutie wordt het symbool '
Gödel bereikt dit door de syntactische structuur van zijn zin Gd[0] - die in feite een inhoudelijke logische bewering is - om te zetten in de vorm van een getallencombinatie. Hij gebruikt hiervoor een speciale coderingsprocedure, de zgn. 'Gödel nummering'. Deze nummering werkt met priemgetallen, oneven getallen, en machten van priemgetallen. Voorbijgaand aan alle rekenkundige details, kunnen we stellen dat dit indexeringsalgoritme bijzondere mogelijkheden biedt. Door deze techniek kan elke logische expressie - elk symbool, elke tekenreeks, en elke bewijsreeks - met een één-op-één correspondentie worden gekoppeld aan een unieke index (een zgn. 'Gödel getal'). De toekenning van Gödel-getallen aan expressievormen is volkomen arbitrair. Het blijkt nu mogelijk om de Gödel-nummering voor zin Gd[0] en zijn onderdelen zó te kiezen dat de volgende resultaten worden bereikt:
In het bewijs van Gödel beginnen we met het toekennen van een waarheidswaarde aan Gd[0]. Deze waarde van Gd[0] wordt direct toegekend aan tekenreeks Gd[1], in de vorm van een Gödel-getal
Bij de eerste interpretatie van tekenreeks Gd[1] kan symbool '
Is aan Gd[0] eenmaal een waarheidswaarde toegekend - waar of onwaar - dan zorgt het negatie-teken in tekenreeks Gd[1] in beide gevallen voor de contradictie: analoog aan de 'gewone' Kretenzer paradox van de leugenaar. De aanwezigheid van het 'bewijsbaar' predicaat maakt daarbij geen verschil. Het resultaat is dat
(9)
Het gevolg is dat we nu kunnen onderzoeken of zin Gd[0] in systeem
Dit resultaat betekent allereerst dat er in de taal van de rekenkunde kennelijk een formele 'route' bestaat om te bewijzen dat het consistente systeem niet elke ware bewering kan bewijzen die zijn eigen bewijs mogelijkheden betreft. Inhoudelijk lijkt deze uitkomst niet erg verwonderlijk, maar de consequenties zijn verstrekkend: in elk formeel systeem dat consistent is zijn er beweringen mogelijk en die in de taal van dat systeem geformuleerd kunnen worden - inclusief een coderingstechniek als 'Gödel's nummering' - maar die niet door dat zelfde systeem bewezen kunnen worden. Daarmee is het bewijs geleverd dat zo'n formeel systeem niet tegelijk consistent en volledig kan zijn.
Andere consequenties van Gödel's bewijs waren, naar de mening van Gödel, dat de menselijke rede creatief is (in plaats van louter lineair-mechanisch), en dat 'synthetische a priori waarheden' mogelijk zijn.
(10)
Het staat buiten kijf dat Gödel's bewijs binnen de kaders van een formeel rekenkundig systeem 'werkt', als een programma van getalsbewerkingen via Gödel's nummering. Anders gezegd, de procedure is formeel correct.
Toch blijven er vragen over de precieze betekenis en geldigheid van de aannamen en de conclusies. Het is duidelijk welke betekenis Gödel bedoelt te leggen in zijn coderingen. Maar kunnen we in de 'mechanische' getalsbewerkingen van Gödel wel een inhoud 'teruglezen', d.i. decoderen naar een betekenis die voldoende zinvol en eenduidig is? Of worden hierbij betekenisaspecten geďntroduceerd die eigenlijk niet inherent zijn aan het standaard concept van een formeel rekenkundig systeem dat consistent is?
Deze vraag komt op diverse manieren tot uiting in meerdere aspecten van Gödel's bewijsvoering.
Zoals we zagen is Gödel's onvolledigheidsbewijs mede afhankelijk van de aanname dat zin Gd[0] waar is, omdat ze niet bewijsbaar is. Maar weten we wel zo zeker dat zin Gd[0] waar is?
Als ze waar is dan moet ze op zijn minst zinvol zijn. Het blijft echter een zeer merkwaardige zin, die nogal vergezocht is wat betreft zinsbouw, en dan ook zeer zeldzaam is in het gewone taalgebruik, misschien zelfs als taaluiting niet helemaal serieus kan worden genomen.
Kan ze dan wel waar zijn? Het is lastig voor te stellen dat deze vraag anders kan worden beantwoord dan enigszins arbitrair: de natuurlijke taal kent, anders dan de formele logica en wiskunde, geen sluitende, strikt eenduidige definities en regels.
Het is vervolgens de vraag of Gödel's zin wel kan worden gecodeerd in de taal van een formeel systeem, vooral wanneer we aannemen dat dit geen 'inherente' betekenis of interpretatie kent. Dit probleem werd door Gödel ook onderkend:
"How indeed could one think of expressing metamathematics [i.e. rules about mathematics] in the mathematical systems themselves, if the latter are to be considered to consist of meaningless symbols which acquire some substitute of meaning only through [that same] metamathematics?." (Kurt Gödel, in: Feferman, S., 1984, 'Kurt Gödel: Conviction and Caution').
Een volgend punt kan zijn dat het Onvolledigheidsbewijs van Gödel afhankelijk is van een heel specifieke codering, een kunstmatige vertaling van de zin Gd[0] via Gödel's nummering. De 'gewone' codering van Gd [0] leidt echter tot een oneindig decoderingsproces, en dus so wie so niet tot een beoordeling door het systeem, en dus al helemaal niet tot een einduitkomst. We staan dus voor een dilemma:
Het punt is echter dat een volledig formeel systeem over elke bewering die een toelaatbare codering in de taal van dat systeem heeft, correct moet kunnen beslissen. Nummercodering is in de taal van een elementair rekenkundig systeem in ieder geval toelaatbaar. Als we aannemen dat Gödel's zin Gd[0] verder ook toelaatbaar is in de taal van het systeem, dan faalt het systeem op het criterium van beslisbaarheid langs minstens één route, namelijk onder Gödel's codering. Dit is voldoende om op het criterium volledig te falen. En hieruit volgt dat Gödel's bewijs wel degelijk noodzakelijk en algemeen geldig is.
Verder is er nog de vraag of Gödel's zin Gd[0] inderdaad toelaatbaar is in de syntax van het type formeel systeem (
'Bewijsbaar' is in feite een meta-logisch predicaat, dat in Gödel's bewijs als functie recursief wordt toegepast. Gödel erkent zčlf al dat deze functie niet zonder meer recursief kan worden gebruikt. Hij presenteert [in 1931, pp.162-171] een lijst van 46 formele notities voor elementen en operaties die hij gebruikt bij zijn bewijsvoering, en plaatst daarbij de opmerking: "Bew(x) [=Beweisbar x] is the only one of the notions 1-46 of which we cannot assert that it is recursive."
We kunnen hiermee weer twee kanten op:
Het ingewikkelde formalisme van Gödel kan dus alleen onder de eerste aanname een voldoende bijdrage leveren aan de toetsing van de Volledigheid van formele systemen als
Een ander probleem ligt in de strategie van 'negatieve bewijsvoering'. Deze wordt hier toegepast op zin Gd [0] in de context van formeel en consistent systeem
Een andere mogelijkheid is om de methode te volgen die aan Koning Solomon wordt toegeschreven, de zgn. ' Solomonische methode': de contradictie in beide takken van Gödel's bewijs gebruiken als bewijs voor de ongeldigheid van de aanname dat Gödel's zin tot de welgevormde zinnen van het formele systeem behoort ..
(11)
De theorema's van Gödel worden wel gebruikt om de uitgangspunten van de Kunstmatige Intelligentie (AI) te weerleggen, met name het streven om een computer te ontwikkelen die tenminste kan presteren wat de menselijke geest door de bank genomen kan.
Zo'n simulatie-systeem vraagt echter om vereisten die afwijken van de voorwaarden voor de systemen in Gödel's theorema's. Een AI systeem dat het menselijke denken simuleert dient in het ideale geval te voldoen aan bepaalde capaciteiten van de menselijke psyche, zodat het bepaalde menselijke, intelligente taken kan uitvoeren. Het hoeft niet per se alle capaciteiten te hebben die de menselijke geest doorgaans heeft. Nog minder hoeft het alle capaciteiten te hebben van een formeel rekenkundig systeem. Het hoeft dus niet logisch consistent te zijn, en het hoeft ook niet logisch volledig te zijn - omdat deze twee eigenschappen door de menselijke geest gewoonlijk in hoge mate worden gemist.
Verder wordt wel gesteld dat een 'echt' AI systeem dat menselijke intelligentie kan nabootsen in staat moet zijn tot allerlei vormen van creatief denken. Het zou daarvoor een niet-eindige verzameling axioma's moet kunnen hebben, die bijvoorbeeld recursief kan worden gedefinieerd met 'meta-axioma's'. Maar omdat geheugens meestal eindig zijn, zullen die meta-axioma's wel van een eindig aantal moeten zijn. Bovendien roept dit in herinnering wat axioma's eigenlijk zijn: namelijk, elementaire en niet verder reduceerbare aannamen in het systeem. Dat wil zeggen, waar zgn. meta-axioma's worden gehanteerd, zijn dat in feite de eigenlijke axioma's. Deze benadering draagt dus niets bij aan inzicht in een AI systeem.
(12)
Voor zover valt te overzien gaat Gödel's betoog hoogstens over de relatie tussen formele systemen en menselijke intelligentie. Dat wil zeggen, tussen (a) enerzijds het domein van abstracte patronen, informatie en logica; en (b) anderzijds het domein van psychische capaciteiten, activiteiten en prestaties.
Zegt dit alles nu iets over de positie van bewustzijn?
(13)
Het bewijs van Gödel gaat over een specifieke categorie van systemen: consistente formele systemen van de rekenkunde. Het past een uitzonderingscategorie toe van een nogal bizar soort zinnen: globale, negatieve zelf-reflexieve meta-oordelen. Het is verder gebaseerd op een zeer speciale en complexe methode van codering: de Gödel-nummering. En globaal genomen heeft Gödel's bewijs voering enkel betrekking op 'kale' syntactische constructies, abstracte patronen die geen specifieke 'inherente' betekenis of interpretatie hebben.
Het verschijnsel bewustzijn houdt daarentegen bij uitstek verband met de meest gevarieerde en variabele betekenis die we ons - in de meest letterlijke zin - kunnen voorstellen. Het domein van Gödel's bewijs vormt daarvan hoogstens een uiterst select en beperkt deel.
Daarom kunnen we niet aannemen dat het bewijs van Gödel iets zegt over de 'bewijsbaarheid' van bewustzijn.
De twee onderdelen van Gödel's onvolledigheidsbewijs.
Kurt Gödel heeft aangetoond dat er onontkoombare (definiete) beperkingen zijn aan formele systemen van de rekenkunde. In zulke systemen wordt een rekenkundige theorie opgebouwd als een zuiver logisch systeem van basisaannamen (axioma's) en afleidingsregels. Gödel's bewijs geldt al voor de meest simpele formaliseringen van de elementaire rekenkunde voor natuurlijke getallen: first-order theory of natural numbers.
{Nb. Met name van de rekenkunde van Sorites (Sorites arithmetic, SA),
die gebaseerd is op de predicatenlogica, PDL, en de eerste vier postulaten van de rekenkunde
volgens Guiseppe Peano (1858-1932; 1891), de PA. Een voorbeeld van zo'n systeem, of calculus,
werd beschreven door Bertrand Russell en Alfred N. Whitehead (Principia Mathematica, 1910-1913 resp. 1962).}
De waarde van een formeel systeem ligt in zijn betrouwbaarheid en zijn toepasbaarheid - en die zijn in het algemeen afhankelijk van twee wezenlijke eigenschappen:
(I)
Correctheid van een systeem betreft de omzetting van vormkenmerken (syntactische structuur) naar betekenis (semantisch e structuur).
Het voordeel van correctheid is: wat formeel afleidbaar is binnen het systeem, is ook inhoudelijk correct - dat wil zeggen, waar of logisch geldig. Dat betekent dat de logische structuur van het systeem tenminste logisch vervulbaar is (algemeen geldig of contingent), en daarmee consistent: het systeem produceert in ieder geval geen tegenstrijdige uitkomsten.
Formele afleidbaarheid impliceert in dat geval inhoudelijke betrouwbaarheid van conclusies.
(II)
Volledigheid van een systeem betreft de omzetting van betekenis (semantische structuur) naar vormkenmerken (syntactisch e structuur).
Het voordeel van volledigheid is: wat inhoudelijk correct is - dat wil zeggen, waar of logisch geldig - dat is ook formeel afleidbaar binnen het systeem.
Inhoudelijke betrouwbaarheid impliceert in dat geval formele afleidbaarheid, en dus voldoende kwantitatieve bewijs capaciteit.
Correctheid.
Correctheid van een systeem betreft de omzetting van vormkenmerken (syntactische structuur) naar betekenis (semantisch e structuur).
Het voordeel van correctheid is: wat formeel afleidbaar is binnen het systeem, is ook inhoudelijk correct - dat wil zeggen, waar of logisch geldig. Dat betekent dat de logische structuur van het systeem tenminste logisch vervulbaar is (algemeen geldig of contingent), en daarmee consistent: het systeem produceert in ieder geval geen tegenstrijdige uitkomsten.
Formele afleidbaarheid impliceert in dat geval inhoudelijke betrouwbaarheid van conclusies.
{Correctheid van een systeem:
'CORRECT(
Systeem
Wat afleidbaar is uit het systeem, is geldig binnen het systeem;
'Afleidbaarheid (van F, uit
i ( (
F[i]) (
F[i]) );
Voor elke afleidbare welgevormde (wff) formule F in T* geldt,
dat deze in
( (T* =WFF*(( (K* 
T*)
i ( (K*
F[i]) (K*
F[i]) ) ) ) }.
S
)' :Systeem S
is correct;Wat afleidbaar is uit het systeem, is geldig binnen het systeem;'Afleidbaarheid (van F, uit S
)' impliceert 'geldigheid (van F, inS
)';i ( (S
F[i]) (S
F[i]) );Voor elke afleidbare welgevormde (wff) formule F in T* geldt,
dat deze in S
geldig, dus waar is:( (T* =WFF*(S
))( (K* T*)
i ( (K*
F[i]) (K*
F[i]) ) ) ) }.(II)
Volledigheid.
Volledigheid van een systeem betreft de omzetting van betekenis (semantische structuur) naar vormkenmerken (syntactisch e structuur).
Het voordeel van volledigheid is: wat inhoudelijk correct is - dat wil zeggen, waar of logisch geldig - dat is ook formeel afleidbaar binnen het systeem.
Inhoudelijke betrouwbaarheid impliceert in dat geval formele afleidbaarheid, en dus voldoende kwantitatieve bewijs capaciteit.
{Volledigheid van een systeem:
'COMPLET(
Systeem
Wat geldig is binnen het systeem, is afleidbaar uit het systeem;
'Geldigheid (van F, in
i ( ( F[i]) ( F[i]) );
Voor elke ware/ geldige welgevormde (wff) formule F in T*
geldt, dat deze in
( (T* =WFF*(( (K* T*)
i ( (K*
F[i]) (K*
F[i]) ) ) ) }.
S
)' :Systeem S
is volledig;Wat geldig is binnen het systeem, is afleidbaar uit het systeem;'Geldigheid (van F, in S
)' impliceert 'Afleidbaarheid (van F, uitS
)';i ( (S
F[i]) (S
F[i]) );Voor elke ware/ geldige welgevormde (wff) formule F in T*
geldt, dat deze in S
bewijsbaar is:( (T* =WFF*(S
))( (K* T*)
i ( (K*
F[i]) (K*
F[i]) ) ) ) }.In zijn bewijs levert Gödel twee stellingen tegen de mogelijkheid dat formele rekenkundige systemen volledig kunnen zijn - ook al zijn ze consistent.
I. Het eerste onvolledigheidstheorema
Deze stelling houdt in, dat elk formeel systeem van de rekenkunde dat consistent is - dus geen onderling tegenstrijdige beweringen oplevert - niet tegelijk volledig is. Dat betekent dat het niet zo is dat elke bewering die in de taal van zo'n systeem geformuleerd kan worden, en waarvan de waarheidswaarde bekend is, ook binnen dat systeem kan worden bewezen (als waar) - of kan worden weerlegd (als onwaar).
Er blijven dus altijd vragen die binnen de taalregels (syntax) van zo'n systeem gesteld kunnen worden, maar waarvan de antwoorden buiten de afleidingsregels (semantiek) van het systeem liggen.
II. Het tweede onvolledigheidstheorema.
Dit wil zeggen dat een formeel rekenkundig systeem dat consistent is ook niet een bewijs kan leveren voor zijn eigen consistentie.
Beide conclusies gelden ongeacht de mogelijke uitbreidingen, modificaties en innovaties van het systeem: zolang het een formeel rekenkundig systeem is, blijven de verbeteringen beperkt tot een toename in complexiteit, dat is een uitbreiding van combinaties. Ze leiden niet tot een volledige bewijscapaciteit van het systeem: er blijven ware zinnen mogelijk in de taal van het systeem die niet bewijsbaar zijn in het systeem. Dit geldt in ieder geval voor beweringen over het systeem zčlf: die vereisen meta-oordelen (oftewel meta-inferentie ).
(2)
Mogelijke consequenties van Gödel's bewijs.
Met name het eerste onvolledigheidstheorema wordt wel aangevoerd om bepaalde opvattingen te schragen over de relatie tussen formele systemen en menselijke cognitieve capaciteiten zoals intelligentie en bewustzijn (zie bijv. R. Penrose, 1994).
(a) Gödel's bewijs wordt bijvoorbeeld gebruikt om te onderstrepen
dat de menselijke intelligentie altijd superieur zal zijn aan formele systemen.
(b) Ook wordt gesteld dat Gödel's bewijs betekent dat de standaardwetenschappelijke methode - die werkt met eerste orde logica, algoritmische wiskunde, en klassieke fysica - niet toereikend is om een model te kunnen vormen van menselijke mentale processen zoals intelligentie, maar ook bewustzijn.
(c) Bovendien zou daaruit volgen dat we in een mechanisch apparaat, waarvan de fysische werking te beschrijven is met een formeel systeem - zoals een automaat, computer of robot - niet een volledige en adequate versie van de menselijke 'geest' kunnen afbeelden - laat staan programmeren. Elke vorm van 'Kunstmatige Intelligentie' zal daarom achterblijven bij de gewone natuurlijke intelligentie.
(b) Ook wordt gesteld dat Gödel's bewijs betekent dat de standaardwetenschappelijke methode - die werkt met eerste orde logica, algoritmische wiskunde, en klassieke fysica - niet toereikend is om een model te kunnen vormen van menselijke mentale processen zoals intelligentie, maar ook bewustzijn.
(c) Bovendien zou daaruit volgen dat we in een mechanisch apparaat, waarvan de fysische werking te beschrijven is met een formeel systeem - zoals een automaat, computer of robot - niet een volledige en adequate versie van de menselijke 'geest' kunnen afbeelden - laat staan programmeren. Elke vorm van 'Kunstmatige Intelligentie' zal daarom achterblijven bij de gewone natuurlijke intelligentie.
Voor deze drie stellingen zijn vele argumenten aan te voeren, waarvan een aantal redelijk steekhoudend zijn. Maar daarbij lijkt Gödel's bewijs niet het meest relevante bewijsmiddel. Hieronder zullen we Gödel's bewijs voering toelichten.
(3)
Het gebruikte tegenvoorbeeld in Gödel's bewijs.
Het bewijs van Gödel zit nogal ingewikkeld in elkaar maar voor het doel van deze bespreking is het vooral belangrijk dat de hoofdlijn van zijn betoogtrant duidelijk wordt. Gödel voert zijn bewijs in grote lijnen als volgt.
Laten we uitgaan van een denkbeeldig systeem,
S
. Stel datS
een formeel rekenkundig systeem is dat logisch consistent is, dat wil zeggen, enkel ware beweringen oplevert, dus zeker geen tegenstrijdige conclusies.De vraag is nu:
[1a] 'Kan een formeel rekenkundig systeem
Of, anders gesteld:
[1b] 'Kan
Wat neerkomt op:
[1c] 'Kan
S
dat logisch consistent is, tegelijk logisch volledig zijn?'Of, anders gesteld:
[1b] 'Kan
S
voor elke zin F die welgevormd is in de taal vanS
čn die waar is, een geldig bewijs leveren van haar waarheid?'Wat neerkomt op:
[1c] 'Kan
S
elke ware zin F die welgevormd is inS
bewijzen?'Gödel betwist de volledigheid van consistente systemen door naar de 'fatale' uitzondering hierop te zoeken. Het tegenvoorbeeld dat Gödel gebruikt voor zijn bewijs is een heel specifieke zin, de bekende 'zin van Gödel' (zeg Gd [0]), die luidt: 'Deze zin is niet bewijsbaar in dit systeem'.
[2a] Gd[0] : "The system (S
) cannot prove that this statement (Gd[0]) is true".Of korter;
[2b] Gd[0] : 'Gd[0] is not provable in S
'.Met andere woorden:
[2c] Gd[0] : 'Gd[0] is niet bewijsbaar in S
'.In meta-logische termen:
[2d] Gd[0] : '¬(S
Gd[0])'.We zien dat zin Gd[0] van dezelfde categorie lijkt als de bekende klassieke Kretenzer paradox, of paradox van de leugenaar, die luidt: 'Ik lieg', of anders gezegd: 'Wat ik zeg is onwaar', of nog preciezer: 'De zin die dit stelt is onwaar'. Deze zin heeft een tweeledige consequentie: Als de zin waar is dan volgt dat zij onwaar is, en als zij onwaar is dan volgt dat zij waar is; beide uiteraard paradoxaal.
Gödel's zin Gd[0] zegt iets soortgelijks, maar niet over waarheid, alleen over bewijsbaarheid. Ook deze zin heeft een tweeledige consequentie: Als de zin waar is dan volgt dat zij niet bewijsbaar is, dus niet als waar kan worden aangenomen, maar als zij onwaar is dan volgt dat zij bewijsbaar is, en dus als waar moet worden aangenomen;
beide eveneens paradoxaal.
Daarbij verwijst ze naar zichzelf (ze is zelf-referentieel) en doet bovendien een bewering óver zichzelf (ze is zelf-reflexief), in ontkennende zin (ze is negatief) met betrekking tot haar bewijsbaarheid in relatie tot systeem
S
(ze is van een meta-niveau) wat het systeem is waarin zij zelf nota bene is gedefinieerd. De zin kijkt als het ware van buiten het systeem naar zichzelf binnen de schil van dat systeem, in relatie tot die schil, en beweert dat er binnen die schil geen enkel bewijs voor zichzelf te vinden is! Het type zin Gd[0] is dus een globaal, negatief zelf-reflexief meta-oordeel. Dat moet haast wel tot problemen leiden ..Toch lijkt het paradoxale voorkomen van Gd[0] niet per se tot een contradictie te leiden. Dit blijkt als we kort nagaan welke waarheidswaarde zin Gd[0] kan hebben. Stel dat Gd[0] een zin is die welgevormd is in een systeem
S
dat consistent is maar niet per se volledig. Dan zijn er maar twee mogelijke antwoorden dieS
over zin Gd[0] kan geven:(a) Als Gd[0] waar is dan geldt haar inhoudelijke strekking
die stelt dat ze niet bewijsbaar is. Dit zou kunnen: waarheid impliceert niet noodzakelijk bewijsbaarheid.
(b) Maar als Gd[0] onwaar is dan is haar inhoud ongeldig wat betekent dat Gd[0] niet onbewijsbaar is en dus mogelijk bewijsbaar. Maar voor een onware zin is het in ieder geval onmogelijk om bewijs baar te zijn in een consistent systeem - zodat de mogelijkheid van een onware zin Gd[0] hier is uitgesloten.
(b) Maar als Gd[0] onwaar is dan is haar inhoud ongeldig wat betekent dat Gd[0] niet onbewijsbaar is en dus mogelijk bewijsbaar. Maar voor een onware zin is het in ieder geval onmogelijk om bewijs baar te zijn in een consistent systeem - zodat de mogelijkheid van een onware zin Gd[0] hier is uitgesloten.
Met andere woorden, de enige logische mogelijkheid is hier dat Gd[0] waar is. Volgens een simpele, intuďtieve lezing lijkt zin Gd[0] als inhoudelijke bewering dus waar te zijn voor elk formeel systeem dat consistent is.
Gödel toetst echter op een formele manier of een willekeurig consistent formeel systeem, te noemen
S
, in staat is om deze zin Gd[0] te bewijzen. Hij laat zien dat elke poging om de zin Gd[0] via een systeemS
te bewijzen of te weerleggen, vastloopt in tegenstrijdigheden. Dit gebeurt, niet verwonderlijk, op analoge wijze als in het geval van de leugenaarparadox. Het wordt alleen wat ingewikkelder vanwege het speciale coderingssysteem dat Gödel gebruikt om zijn bewijs voor systemen alsS
geldig te laten zijn.(4)
Een meer formele lezing van Gödel's zin.
In een simpele, 'semi-formele' vorm kunnen we Gödel's zin Gd[0] als volgt weergeven:
[3] Gd[0]
=
'Gd[0] is niet bewijsbaar inS
'.In de vergelijking van [3] verwijst de tweede 'Gd[0]' naar de eerste, maar is daarbij ook van een andere orde. Eigenlijk impliceert Gödel met zijn definitie van Gd[0] een nevenstelling van twee formules:
[4] {3} { (4a) 
(4b) };
{ (4a) (4b) };[4a] Gd[1]
[4b]
=
'Gd[2]
is niet bewijsbaar inS
';[4b]
Gd[2]
=
Gd[1].Het verschil tussen Gd[1] en '
Gd[2]
' ligt zowel op syntactisch niveau als op semantisch niveau:(a)
(b)
Daarmee verwijst ze naar '
Syntactisch verschil
(a1) Gd[1] is een naam van een bepaalde tekenreeks;
(a2) '
Dat wil zeggen, Gd[1] vormt als tekenreeks de syntactische omgeving, of bedding, van
de minderomvattende tekenreeks '(a2) '
Gd[2]
' is zčlf een tekencombinatie binnen de tekenreeks die door Gd [1] wordt aangeduid.Gd[2]
'.Semantisch verschil
(b1) Gd[1] is een aanduiding voor een zin of stelling,
een inhoudelijke bewering (nl. de betekenis van zin Gd[0]);
(b2)
Dat wil zeggen, Gd[1] zegt als bewering ook iets inhoudelijks over (de bewijsbaarheid van) '(b2)
Gd[2]
is zčlf een letterlijke inhoud binnen de bewering die door Gd [1] wordt aangeduid.Gd[2]
'.Daarmee verwijst ze naar '
Gd[2]
', maar dat is van secundaire orde.Uit deze opsplitsing van Gd[0] wordt duidelijk dat het verschil tussen de eerste Gd[0] (d.i. Gd[1]) en de tweede Gd[0] (d.i. Gd[2]) wezenlijk is. We zullen zien dat dit verschil een cruciale rol speelt in de opzet van Gödel's bewijs.
(5)
Positieve bewijsvoering.
De vraag is of het mogelijk is om een formeel bewijs te leveren van de (on)volledige bewijskracht van formele rekenkundige systemen die consistent zijn. Voor dit doel kunnen we onderzoeken of er een zin mogelijk is die welgevormd is in zo'n systeem en waar is, maar tegelijk in datzelfde systeem niet bewijsbaar. Als we hiervoor Gödel's zin (Gd[0]) nemen, dan gaat het er om een formeel bewijs te leveren van de (on)mogelijkheid om voor de ware zin Gd[0] in het betreffende systeem een bewijs te construeren.
Voor een formeel bewijs van een stelling kunnen we in het algemeen twee kanten op: een positieve bewijsvoering of een negatieve. We zullen eerst nagaan of een positieve bewijsvoering iets oplevert voor zin Gd[0].
(I) Positief bewijs: reconstructie van de complete afleiding.
Een voor de hand liggende methode van bewijzen is zoeken naar positieve aanwijzingen en voorwaarden voor de waarheid van de te bewijzen stelling, deze 'bouwstenen' vervolgens te ordenen in een redeneerketen, en te toetsen of die als een 'bewijsreeks' kan dienen die de beoogde conclusie via logische afleiding oplevert.
Hoe kan zo'n bewijsreeks in elkaar steken? Als eerste kunnen we voorlopig aannemen dat zo'n bewijsreeks voor de te bewijzen stelling in een systeem
S
al bestaat en alleen maar hoeft te worden 'ontdekt'. Als we uitgaan van de opbouw en samenstelling van de te bewijzen stelling kunnen we kijken of we het gevolgde redeneerpad inS
kunnen reconstrueren. De bedoeling is dan om het bewijs op te bouwen via positieve bewijsvoering of bevestiging (verificatie, affirmatie): op grond van logische afleiding (derivatie). De bewijsreeks heeft dan de vorm van een complete stap-voor-stap afleidingsreeks, die vanaf uitgangspunten (axioma's) vanS
rechtstreeks en expliciet leidt naar de eindconclusie.{Nb. Bijvoorbeeld het systeem van natuurlijke deductie,
volgens Gerhard Gentzen (1934), Frederic B. Fitch (1952).}
Een positieve bewijsreeks voor Gd[0] zal uiteraard minstens één element moeten bevatten, uit de axioma's of bewezen stellingen van
S
, die rechtstreeks een voldoende logische voorwaarde vormt (een premisse) voor de eindconclusie.De eindconclusie - in dit geval hetzij 'Gd[0]', hetzij '¬Gd[0]' - zal dus moeten aansluiten op minstens één andere stelling in
S
.De vraag is nu of we voor zin Gd[0] zo'n 'sleutelformule' in
S
kunnen vinden. De inhoud van Gd[0] biedt hiervoor niet veel aangrijpingspunten. Ze bevat immers maar vier verwijzingen naar samenstellende componenten:· het symbool voor ontkenning (negatieteken), dat een éénplaatsige
logische waarheidsfunctie is die zelf vraagt om een inhoudelijk argument;
· de relatieterm 'bewijsbaar', die zelf eveneens vraagt om inhoud, namelijk minstens één bewijsreeks;
· het symbool '
· het symbool 'Gd[0]', dat staat voor dezelfde zin die te bewijzen staat.
· de relatieterm 'bewijsbaar', die zelf eveneens vraagt om inhoud, namelijk minstens één bewijsreeks;
· het symbool '
S
' dat we kunnen weglaten omdat we enkel binnen systeemS
zoeken;· het symbool 'Gd[0]', dat staat voor dezelfde zin die te bewijzen staat.
We kunnen dus alleen afgaan op het begrip 'bewijsbaar', maar de waarheid hiervan is met name afhankelijk van de vraag of er al een bewijsreeks voor Gd[0] te vinden is, en daarvoor zoeken we juist aanwijzingen. Omdat we verder nog niets hebben onderzocht zal deze bewijsreeks so wie so leeg zijn.
Voor het overige is er in Gd[0] hoegenaamd géén betekenis, zin of inhoud aanwezig. De zin ontbeert een verwijzing naar inhoud, een 'aboutness' die kenmerkend is voor zinvolle beweringen. Door dit 'betekenis-vacuüm' wordt de zin afgezonderd van alle overige inhouden - axioma's of afgeleide stellingen - die in systeem
S
kunnen voorkomen. Daardoor kunnen so wie so geen bouwstenen worden gevonden inS
om een positieve bewijsreeks op te bouwen met betrekking tot de waarheid of de onwaarheid van zin Gd[0].(6)
Het probleem van de vicieuze cirkel.
Het bovenstaande kunnen we ook in een meer formele vorm laten zien. Een vereiste voor het formele bewijs is natuurlijk dat een zelf-reflexieve zin als Gd[0] wel in de taal van een formeel systeem
S
geformuleerd moet kunnen worden.Om te bereiken dat de zin Gd[0] naar zichzelf verwijst (zelf-referentieel is), moet het de mogelijkheid bieden dat we - in termen van de hier gebruikte symbolen - de vermelding van de tekencombinatie '
Gd[2]
' binnen de tekenreeks van Gd[1] moeten kunnen 'herkennen' als een aanduiding van Gd[1] zčlf.Uit het voorgaande werd duidelijk dat de zin Gd[0] in feite een klein redeneerschema inhoudt, een algoritme: telkens als we Gd[0] bekijken kunnen we op de plaats van '
Gd[2]
' in de tekenreeks van Gd[1], opnieuw de inhoud van Gd[0] invullen: dat wil zeggen, dezelfde tekenreeks van Gd[1]. Elke vermelding van 'Gd[2]
' binnen Gd[1] wordt dan vervangen door de gehele Gd[1]. Die 'lezing' kunnen we weergeven met behulp van het formele symbool voor een substitutie operatie: ':=' voor 'is vervangbaar door'. Dan kan inS
zin Gd[0] worden gelezen als:[5] { (4a),(4b) } { (5a)
(5b) };
{ (5a)
(5b) };[5a] Gd[1]
[5b] '
=
'Gd[2]
is niet bewijsbaar inS
';[5b] '
Gd[2]
' := Gd[1].Dankzij subformule [5b] kan elke vermelding van '
Gd[2]
' binnen Gd[1] worden vervangen door de gehele tekenreeks Gd[1].Om de toepassing van operatie [5b] op Gd[1] uit te drukken, noteren we kortweg:
[6a] Gd[1] ·[(5b)];[6b] Gd[1] ·['Gd[2]
' :=Gd[1]].Op dezelfde manier kunnen we de subformules { (5a),(5b) } van de probleemstelling Gd[0] nu in meta-logische termen formuleren:
(met symbolen '
' voor 'formeel bewijsbaar', '¬' voor 'niet'):[7] { (5a),(5b),(6b) } { (7a)
(7b) };
{ (7a)
(7b) };[7a] Gd[1] = '¬(
[7b] '
S
Gd[2]
)';[7b] '
Gd[2]
' := Gd[1].Vervolgens kunnen we kijken wat er gebeurt als operatie [6b] wordt geactiveerd.
[8] { (6b,7a,) }
[8a] Gd[1] = '¬(
[6b]: Gd[1] ·['
[8b] Gd[1] = '¬( ¬(
[6b]: Gd[1] ·['
[8c] Gd[1] = '¬(¬( ¬(¬(
[6b]: Gd[1] ·['
[8d] Gd[1] = '¬(¬(¬(¬(
¬(¬(¬(¬(
etc. ..
S
Gd[2]
)';[6b]: Gd[1] ·['Gd[2]
' :=Gd[1]];[8b] Gd[1] = '¬(S
¬(S
Gd [2]
) )';[6b]: Gd[1] ·['Gd[2]
' :=Gd[1]];[8c] Gd[1] = '¬(S
¬(S
¬(S
¬(S
Gd [2]
) ) ) )';[6b]: Gd[1] ·['Gd[2]
' :=Gd[1]];[8d] Gd[1] = '¬(S
¬(S
¬(S
¬(S
¬(
S
¬(S
¬(S
¬(S
Gd[2]
) ) ) ) ) ) ) )';etc. ..
We zien dat de oorspronkelijke tekenreeks Gd[1] bij elke activatie van operatie [6b] explosief - nl. kwadratisch - wordt uitgebreid. Na elke uitbreiding bevat Gd[1] echter nog steeds dezelfde onbekende bevat, nl. symbool
Gd[2]
. Hierdoor kan de uitvoering van operatie [6b] in principe eindeloos doorgaan - de bekende 'oneindige lus' (oneindige recursie ). Het gevolg is een onafzienbare, automatische uitbreiding van de symbolenrij Gd[1] (de syntactische inhoud) - zonder dat ooit een definitieve betekenis van Gd[0] (semantische inhoud) kan worden vastgesteld. Anders gezegd: het zoekproces in de interpretatiefase eindigt niet (d.i. termineert niet). Het gevolg is dat (a) de te bewijzen stelling Gd[0] in het systeem geen formele 'betekenis' krijgt en dus ook geen waarheidswaarde kan krijgen, en (b) het systeem nooit aan het zoekproces naar een bewijs toekomt.Overigens zien een vergelijkbaar beeld wanneer we een positieve variant van Gd[0] nemen, zeg H0, waarin de ontkenning ('¬') is weggelaten.
De conclusie is dat Gd[0] niet (rechtstreeks) bewijsbaar is in
S
. We kunnen nu natuurlijk redeneren: het lukt niet om inS
een positieve bewijsreeks voor Gd [0] op te bouwen, dus is Gd[0] niet bewijsbaar. Dus de inhoud van Gd[0], luidend 'Gd[0] is niet bewijsbaar inS
', klopt - en dus is Gd[0] waar!Het probleem is alleen dat het laatste een inhoudelijke conclusie achteraf is, die gebaseerd is op een zinvolle, dus 'betekenisvolle', dus interpretabele inhoud van Gd[0] - en daarvoor konden we nu juist geen formele elementen vinden in
S
. Daardoor hebben we nog steeds geen eindige formele interpretatie van zin Gd[0], weten we niet wat Gd[0] letterlijk, in formele termen, 'betekent' en kunnen we haar dus ook geen waarheidswaarde toekennen als welgevormde formule.Om een voorbeeld te noemen: een computerprogramma zou na een onderzoek van Gd[0] wel kunnen concluderen: (1) 'Gd[0] is niet te interpreteren', bijvoorbeeld door voor elke lus die geactiveerd wordt te testen of het daarvoor een ontsnappingstest kan vinden. Op basis daarvan kan het dan ook antwoorden: (2) '(dus) Gd[0] is niet bewijsbaar'. Maar het kan vervolgens niet tot de conclusie komen: (3) 'Gd[0] is waar', omdat het immers geen materiaal heeft gevonden om Gd [0] te 'begrijpen'. Dan kan het systeem ook niet aannemen dat Gd[0] inhoudelijk waar is. De aanname van een ware Gd[0] moet echter binnen het systeem mogelijk zijn om de vraagstelling van Gödel formeel te kunnen beantwoorden.
De weg van positieve bewijsvoering levert dus niets op.
(7)
Negatieve bewijsvoering.
De andere mogelijkheid is om, zoals Gödel doet, niet naar de mogelijke premissen maar naar de mogelijke consequenties van de aanname van Gd[0] als waar of onwaar te kijken.
(II) Negatief bewijs: uitsluiten van mogelijkheden die tegenstrijdigheid opleveren
Een 'secundaire' methode van bewijzen bestaat uit het systematisch testen en uitsluiten van alternatieve mogelijkheden, net zolang totdat de beoogde conclusie als enige logische mogelijkheid overblijft. De bedoeling is hierbij om het bewijs te leveren via negatieve bewijsvoering (falsificatie, refutatie): door weerlegging van het tegendeel of 'omgekeerde' van de te bewijzen stelling, middels afleiding van een contradictie ( reductie ad absurdum).
{Nb. Bijvoorbeeld de methode van resolutie, volgens John Alan Robinson (1965).}
Het is bij deze methode dus voldoende om twee tegengestelde beweringen af te leiden op de hoofdlijn van redenering. Deze hoeven niet per se geďnterpreteerd te zijn in termen van basiselementen van systeem
S
(axioma's of bewezen stellingen). Daarom kan de bewijsreeks zeer abstract blijven, zodat de opbouw ervan niet per se afhankelijk is van een nadere interpretatie of 'concretisering' van variabelenamen.Deze benadering lijkt bij uitstek geschikt voor de beoordeling van zin Gd[0] en haar afleidbaarheid uit
S
. We kunnen het doorS
gegeven antwoord over Gd[0] opnieuw 'invoeren' in de variabelenaam 'Gd[0]' die in zin Gd[0] zelf vermeld staat. Vervolgens kunnen we kijken wat hier uit volgt.Deze aanpak is wel afhankelijk van diverse andere vooronderstellingen.
Eerste aanname is dat het waarheidsoordeel van systeem
S
over zin Gd[0] in beide antwoordmogelijkheden - Gd[0] als waar of onwaar - kan worden toegepast op de inhoudelijke betekenis van zin Gd[0].(8)
De kracht van Gödel's codering.
Gödel omzeilt het probleem van de oneindige interpretatie (als gevolg van eindeloze recursieve uitbreiding) door de eerdergenoemde substitutie-operatie grondig te wijzingen. Om in bovenstaande terminologie te spreken: met Gödel's substitutie wordt het symbool '
Gd[2]
' in de tekenreeks Gd[1] nog steeds vervangen, maar het resultaat van de substitutie is nu niet meer een uitbreiding van de oorspronkelijke Gd[1] (met alle problematische consequenties van dien), maar enkel een exacte aanduiding van Gd[1], in zijn oorspronkelijke, ongewijzigde vorm.Gödel bereikt dit door de syntactische structuur van zijn zin Gd[0] - die in feite een inhoudelijke logische bewering is - om te zetten in de vorm van een getallencombinatie. Hij gebruikt hiervoor een speciale coderingsprocedure, de zgn. 'Gödel nummering'. Deze nummering werkt met priemgetallen, oneven getallen, en machten van priemgetallen. Voorbijgaand aan alle rekenkundige details, kunnen we stellen dat dit indexeringsalgoritme bijzondere mogelijkheden biedt. Door deze techniek kan elke logische expressie - elk symbool, elke tekenreeks, en elke bewijsreeks - met een één-op-één correspondentie worden gekoppeld aan een unieke index (een zgn. 'Gödel getal'). De toekenning van Gödel-getallen aan expressievormen is volkomen arbitrair. Het blijkt nu mogelijk om de Gödel-nummering voor zin Gd[0] en zijn onderdelen zó te kiezen dat de volgende resultaten worden bereikt:
(a) De tekenreeks Gd[1] krijgt een uniek Gödel nummer,
(b) Wanneer substitutie [6b] wordt toegepast dan volgt een getalsbewerking waarvan de uitkomst weer bestaat uit een Gödel getal:
Gn
[1]. Binnen dit nummerGn
[1] van tekenreeks Gd[1] wordt het symbool 'Gd[2]
' vervangen door het Gödel-getalGn
[2] dat hoort bij een substitutie-operatie als [6b]: Gd[1] ·['Gd[2]
' :=Gd [1]].(b) Wanneer substitutie [6b] wordt toegepast dan volgt een getalsbewerking waarvan de uitkomst weer bestaat uit een Gödel getal:
Gn
[1]. Dat getal is identiek aan het getal van de tekenreeks Gd[1], in zijn oorspronkelijke, ongewijzigde vorm. Het verwijst dan ook naar de waarheidwaarde van Gd[1] die in een eerder stadium is toegekend (en is opgeslagen op het geheugenadres vanGn
[1]).In het bewijs van Gödel beginnen we met het toekennen van een waarheidswaarde aan Gd[0]. Deze waarde van Gd[0] wordt direct toegekend aan tekenreeks Gd[1], in de vorm van een Gödel-getal
Gn
[1] (respectievelijk het computer-geheugenadres vanGn
[1]). Vervolgens wordt tekenreeks Gd[1] in de vorm van Gödel-getalGn
[1] inhoudelijk geëvalueerd, waarbij symbool 'Gd[2]
', via een Gödel-getalGn
[2], substitutie-operatie [6b] activeert, die getalGn
[1] oproept, en daarmee de waarheidswaarde van Gd[0] (bewaard op het geheugenadres vanGn
[1]).Bij de eerste interpretatie van tekenreeks Gd[1] kan symbool '
Gd[2]
' dus al worden 'gelezen' als de aanduiding van Gd[0], en kan het worden geduid volgens de waarheidswaarde van Gd[0]. Dit betekent dat de zin Gd[0] in de taal vanS
in eindige tijd kan worden geďnterpreteerd. Het betekent ook dat de codering voor de toestand ' Gd[0] is niet bewijsbaar' formeel kan worden vergeleken met de codering voor de toestand 'Gd [0] is waar'.Is aan Gd[0] eenmaal een waarheidswaarde toegekend - waar of onwaar - dan zorgt het negatie-teken in tekenreeks Gd[1] in beide gevallen voor de contradictie: analoog aan de 'gewone' Kretenzer paradox van de leugenaar. De aanwezigheid van het 'bewijsbaar' predicaat maakt daarbij geen verschil. Het resultaat is dat
S
zin Gd[0] noch kan bewijzen, noch kan weerleggen.(9)
Het verloop van het formele bewijs
Het gevolg is dat we nu kunnen onderzoeken of zin Gd[0] in systeem
S
formeel bewijsbaar is als waar, of weerlegbaar als onwaar.Onvolledigheid van de elementaire rekenkunde volgens Gödel.
Bewijs:
(I)
(II)
(III)
Eerste aanname:
Stel dat Gd[0] waar is.
(I.1) Gd[0];
(I.2) Bepaal de syntactische inhoud van Gd[0].
(I.3) Doe semantische interpretatie van Gd[0].
(I.4) Stel dat
(I.5) Levert contradictie.
(I.1) Gd[0];
(I.2) Bepaal de syntactische inhoud van Gd[0].
(I.2a) (Gd[0] :=Gd[1]);
(I.2b)(Gd[1]
(Gd[0] :=Gd[1]);(I.2b)
(Gd[1] =
'¬(S
Gd[2]
)');(I.3) Doe semantische interpretatie van Gd[0].
(I.3a) {I.1,I.2a} Gd[1];
(I.3b) {I.3a,I.2b}'¬(
(I.3c)('
(I.3d) {I.3b,I.3c}{I.3b} · ['
(I.3e) {I.3d}'¬( Gd
[1])';
(I.3f) {I.3e} · [semantische inhoud]¬( Gd[1]);
Gd[1];(I.3b) {I.3a,I.2b}
'¬(S
Gd[2]
)';(I.3c)
('Gd[2]
' := Gd[1]);(I.3d) {I.3b,I.3c}
{I.3b} · ['Gd[2]
':=Gd[1]];(I.3e) {I.3d}
'¬(S
Gd
[1])';(I.3f) {I.3e} · [semantische inhoud]
¬(S
Gd[1]);(I.4) Stel dat
S
Volledig is:(I.4a) {I.3a} ( Gd[1]);
(S
Gd[1]);(I.5) Levert contradictie.
(I.5a) {I.3f,I.4a} 
;
(I.5b) {I.5a}¬MOGELIJK(I.1).
(I.5c) {I.5b}¬(Gd[0]).
;(I.5b) {I.5a}
¬MOGELIJK(I.1).(I.5c) {I.5b}
¬(Gd[0]).(II)
Tweede aanname:
Stel dat Gd[0] onwaar is.
(II.1) ¬Gd[0];
(II.2) Bepaal de syntactische inhoud van Gd[0].
(II.3) Doe semantische interpretatie van Gd[0].
(II.4) Stel dat
(II.5) Levert contradictie.
(II.1) ¬Gd[0];
(II.2) Bepaal de syntactische inhoud van Gd[0].
(II.2a) (Gd[0] :=Gd[1]);
(II.2b) (Gd[1] = '¬(
(Gd[0] :=Gd[1]);
(II.2b)
(Gd[1] = '¬(S
Gd[2]
)');(II.3) Doe semantische interpretatie van Gd[0].
(II.3a) {II.1,II.2a} ¬Gd[1];
(II.3b) {II.3a,II.2b}¬'¬(
(II.3c)('
(II.3d) {II.3b,II.3c}{II.3b} · ['
(II.3f) {II.3d}¬'¬( Gd
[1])';
(II.3e) {II.3d}·[semantische inhoud]¬¬( Gd[1]);
(II.3f) {II.3e}( Gd
[1]);
¬Gd[1];(II.3b) {II.3a,II.2b}
¬'¬(S
Gd[2]
)';(II.3c)
('Gd[2]
' := Gd[1]);(II.3d) {II.3b,II.3c}
{II.3b} · ['Gd[2]
':=Gd[1]];(II.3f) {II.3d}
¬'¬(S
Gd
[1])';(II.3e) {II.3d}·[semantische inhoud]
¬¬(S
Gd[1]);(II.3f) {II.3e}
(S
Gd
[1]);(II.4) Stel dat
S
Volledig is:(II.4a) {II.3a} ( ¬Gd[1]);
(S
¬Gd[1]);(II.5) Levert contradictie.
(II.5a) {II.3f,II.4a}
;
(II.5b) {II.5a}¬MOGELIJK(II.1).
(II.5c) {II.5b}¬(¬Gd[0]).
;(II.5b) {II.5a}
¬MOGELIJK(II.1).(II.5c) {II.5b}
¬(¬Gd[0]).(III)
Resultaat:
(III.1) {I.5c,II.5c} (¬Gd[0]
¬(¬Gd[0]));
(III.2) {III.1}(¬Gd[0] Gd
[0]);
(III.3) {III.2};
(III.4) {III.3}¬COMPLET(
(¬Gd[0]
¬(¬Gd[0]));(III.2) {III.1}
(¬Gd[0] Gd
[0]);(III.3) {III.2}
;(III.4) {III.3}
¬COMPLET(S
).Conclusie:
Dit resultaat betekent allereerst dat er in de taal van de rekenkunde kennelijk een formele 'route' bestaat om te bewijzen dat het consistente systeem niet elke ware bewering kan bewijzen die zijn eigen bewijs mogelijkheden betreft. Inhoudelijk lijkt deze uitkomst niet erg verwonderlijk, maar de consequenties zijn verstrekkend: in elk formeel systeem dat consistent is zijn er beweringen mogelijk en die in de taal van dat systeem geformuleerd kunnen worden - inclusief een coderingstechniek als 'Gödel's nummering' - maar die niet door dat zelfde systeem bewezen kunnen worden. Daarmee is het bewijs geleverd dat zo'n formeel systeem niet tegelijk consistent en volledig kan zijn.
Andere consequenties van Gödel's bewijs waren, naar de mening van Gödel, dat de menselijke rede creatief is (in plaats van louter lineair-mechanisch), en dat 'synthetische a priori waarheden' mogelijk zijn.
(10)
Vraagtekens bij Gödel's bewijs.
Het staat buiten kijf dat Gödel's bewijs binnen de kaders van een formeel rekenkundig systeem 'werkt', als een programma van getalsbewerkingen via Gödel's nummering. Anders gezegd, de procedure is formeel correct.
Toch blijven er vragen over de precieze betekenis en geldigheid van de aannamen en de conclusies. Het is duidelijk welke betekenis Gödel bedoelt te leggen in zijn coderingen. Maar kunnen we in de 'mechanische' getalsbewerkingen van Gödel wel een inhoud 'teruglezen', d.i. decoderen naar een betekenis die voldoende zinvol en eenduidig is? Of worden hierbij betekenisaspecten geďntroduceerd die eigenlijk niet inherent zijn aan het standaard concept van een formeel rekenkundig systeem dat consistent is?
Deze vraag komt op diverse manieren tot uiting in meerdere aspecten van Gödel's bewijsvoering.
(I) Is Gödel's zin waar?
Zoals we zagen is Gödel's onvolledigheidsbewijs mede afhankelijk van de aanname dat zin Gd[0] waar is, omdat ze niet bewijsbaar is. Maar weten we wel zo zeker dat zin Gd[0] waar is?
Als ze waar is dan moet ze op zijn minst zinvol zijn. Het blijft echter een zeer merkwaardige zin, die nogal vergezocht is wat betreft zinsbouw, en dan ook zeer zeldzaam is in het gewone taalgebruik, misschien zelfs als taaluiting niet helemaal serieus kan worden genomen.
Kan ze dan wel waar zijn? Het is lastig voor te stellen dat deze vraag anders kan worden beantwoord dan enigszins arbitrair: de natuurlijke taal kent, anders dan de formele logica en wiskunde, geen sluitende, strikt eenduidige definities en regels.
(II) Is Gödel's zin formaliseerbaar?
Het is vervolgens de vraag of Gödel's zin wel kan worden gecodeerd in de taal van een formeel systeem, vooral wanneer we aannemen dat dit geen 'inherente' betekenis of interpretatie kent. Dit probleem werd door Gödel ook onderkend:
"How indeed could one think of expressing metamathematics [i.e. rules about mathematics] in the mathematical systems themselves, if the latter are to be considered to consist of meaningless symbols which acquire some substitute of meaning only through [that same] metamathematics?." (Kurt Gödel, in: Feferman, S., 1984, 'Kurt Gödel: Conviction and Caution').
(III) Leidt Gödel's nummering tot valide conclusies?
Een volgend punt kan zijn dat het Onvolledigheidsbewijs van Gödel afhankelijk is van een heel specifieke codering, een kunstmatige vertaling van de zin Gd[0] via Gödel's nummering. De 'gewone' codering van Gd [0] leidt echter tot een oneindig decoderingsproces, en dus so wie so niet tot een beoordeling door het systeem, en dus al helemaal niet tot een einduitkomst. We staan dus voor een dilemma:
(a) de 'vergezochte' route van Gödel's codering opent voor zin Gd[0]
een formele weg naar de conclusie van Onvolledigheid: een sluitend bewijs uit het ongerijmde;
(b) maar de weg van de 'gewone', voor de hand liggende codering van zin Gd[0] leidt tot oneindig zoeken, en blijft dus onbeslist.
Dit roept de vraag op of Gödel's bewijs wel sluitend is: noodzakelijk en algemeen geldig. Lijkt er niet sprake
van een 'open einde': contingentie?(b) maar de weg van de 'gewone', voor de hand liggende codering van zin Gd[0] leidt tot oneindig zoeken, en blijft dus onbeslist.
Het punt is echter dat een volledig formeel systeem over elke bewering die een toelaatbare codering in de taal van dat systeem heeft, correct moet kunnen beslissen. Nummercodering is in de taal van een elementair rekenkundig systeem in ieder geval toelaatbaar. Als we aannemen dat Gödel's zin Gd[0] verder ook toelaatbaar is in de taal van het systeem, dan faalt het systeem op het criterium van beslisbaarheid langs minstens één route, namelijk onder Gödel's codering. Dit is voldoende om op het criterium volledig te falen. En hieruit volgt dat Gödel's bewijs wel degelijk noodzakelijk en algemeen geldig is.
(IV) Past 'bewijsbaar' in het systeem?
Verder is er nog de vraag of Gödel's zin Gd[0] inderdaad toelaatbaar is in de syntax van het type formeel systeem (
S
) waar Gödel's bewijs voor bedoeld is. Die vraag geldt met name voor het begrip 'Bewijsbaar'.'Bewijsbaar' is in feite een meta-logisch predicaat, dat in Gödel's bewijs als functie recursief wordt toegepast. Gödel erkent zčlf al dat deze functie niet zonder meer recursief kan worden gebruikt. Hij presenteert [in 1931, pp.162-171] een lijst van 46 formele notities voor elementen en operaties die hij gebruikt bij zijn bewijsvoering, en plaatst daarbij de opmerking: "Bew(x) [=Beweisbar x] is the only one of the notions 1-46 of which we cannot assert that it is recursive."
We kunnen hiermee weer twee kanten op:
(a) Beslissen we dat 'Bewijsbaar' tot de syntax van
(b) Beslissen we dat 'Bewijsbaar' niet tot de syntax van
S
behoort - ook en zelfs in een recursieve toepassing - dan volgt via Gödel's nummering inderdaad datS
onvolledig is met betrekking tot de beoordeling van Gd[0].(b) Beslissen we dat 'Bewijsbaar' niet tot de syntax van
S
behoort dan valt Gd[0] per definitie buiten de reikwijdte van het 'oordeelsvermogen' vanS
, en kan ze dus niet in verband worden gebracht met de Volledigheid vanS
. Het laatste geldt ongeacht codering van Gd[0] via Gödel-nummering.Het ingewikkelde formalisme van Gödel kan dus alleen onder de eerste aanname een voldoende bijdrage leveren aan de toetsing van de Volledigheid van formele systemen als
S
.(V) Interpretatie van de contradictie.
Een ander probleem ligt in de strategie van 'negatieve bewijsvoering'. Deze wordt hier toegepast op zin Gd [0] in de context van formeel en consistent systeem
S
: op een gemengde compositie dus van enerzijds bewezen feiten en anderzijds meerdere onbewezen gegevens - bestaande uit aannamen, afspraken of 'spelregels'. Als blijkt dat alle consequenties van zo'n 'hybride' compositie uitlopen op contradicties, dan mogen we concluderen dat minstens één van de aannamen of 'spelregels' ongeldig is. De vraag is echter welke. Is het per se de aanname datS
behalve consistent ook volledig zou kunnen zijn, die moet sneuvelen?Een andere mogelijkheid is om de methode te volgen die aan Koning Solomon wordt toegeschreven, de zgn. ' Solomonische methode': de contradictie in beide takken van Gödel's bewijs gebruiken als bewijs voor de ongeldigheid van de aanname dat Gödel's zin tot de welgevormde zinnen van het formele systeem behoort ..
(11)
Gödel's bewijs als weerlegging van A.I..
De theorema's van Gödel worden wel gebruikt om de uitgangspunten van de Kunstmatige Intelligentie (AI) te weerleggen, met name het streven om een computer te ontwikkelen die tenminste kan presteren wat de menselijke geest door de bank genomen kan.
Zo'n simulatie-systeem vraagt echter om vereisten die afwijken van de voorwaarden voor de systemen in Gödel's theorema's. Een AI systeem dat het menselijke denken simuleert dient in het ideale geval te voldoen aan bepaalde capaciteiten van de menselijke psyche, zodat het bepaalde menselijke, intelligente taken kan uitvoeren. Het hoeft niet per se alle capaciteiten te hebben die de menselijke geest doorgaans heeft. Nog minder hoeft het alle capaciteiten te hebben van een formeel rekenkundig systeem. Het hoeft dus niet logisch consistent te zijn, en het hoeft ook niet logisch volledig te zijn - omdat deze twee eigenschappen door de menselijke geest gewoonlijk in hoge mate worden gemist.
Verder wordt wel gesteld dat een 'echt' AI systeem dat menselijke intelligentie kan nabootsen in staat moet zijn tot allerlei vormen van creatief denken. Het zou daarvoor een niet-eindige verzameling axioma's moet kunnen hebben, die bijvoorbeeld recursief kan worden gedefinieerd met 'meta-axioma's'. Maar omdat geheugens meestal eindig zijn, zullen die meta-axioma's wel van een eindig aantal moeten zijn. Bovendien roept dit in herinnering wat axioma's eigenlijk zijn: namelijk, elementaire en niet verder reduceerbare aannamen in het systeem. Dat wil zeggen, waar zgn. meta-axioma's worden gehanteerd, zijn dat in feite de eigenlijke axioma's. Deze benadering draagt dus niets bij aan inzicht in een AI systeem.
(12)
Gödel's bewijs en bewustzijn.
Voor zover valt te overzien gaat Gödel's betoog hoogstens over de relatie tussen formele systemen en menselijke intelligentie. Dat wil zeggen, tussen (a) enerzijds het domein van abstracte patronen, informatie en logica; en (b) anderzijds het domein van psychische capaciteiten, activiteiten en prestaties.
Zegt dit alles nu iets over de positie van bewustzijn?
(a)
Dit lijkt een redelijke aanname. Het omgekeerde is weinig waarschijnlijk: dat een mens in staat zou zijn om Gödel's bewijs ook volledig onbewust te kunnen uitvoeren. Voor zo'n niveau van intelligentie zal een bewuste toestand van het mentale proces nodig zijn. Maar dat is niet bijzonder, het geldt voor veel taken en activiteiten. De meeste mensen zijn ook niet goed in volslagen bewusteloos autorijden, enzovoorts. Goed, in theorie kan een machine het ook, maar in de praktijk hebben we voorlopig toch liever een bewuste, alerte menselijke bestuurder die de weg volgt.
(b)
Het is niet aannemelijk dat veel mensen elke keer eerst bepaalde meta-oordelen moeten vellen over hun eigen bewijs capaciteit, voordat ze tot hun gewone, alledaagse (waak)bewustzijn komen - bijvoorbeeld 's-morgens bij het ontwaken. En zeker zijn voor de bewuste toestand geen meta-algoritmische inzichten nodig die het verschil uitmaken tussen de waarheidstoekenning aan Gödel's zin, en het formele bewijs van de onmogelijkheid om die waarheid formeel te bewijzen.
(c)
Dit kan in ieder geval in negatieve zin. We weten immers dat we een heleboel niet kunnen bewijzen. Dus voorlopig kunnen we uitgaan van een beperkte bewijscapaciteit, die dus zeker onvolledig zal zijn.
Wel is het lastig om aan onze mentale bewijscapaciteit op alle fronten specifieke, absolute grenzen te stellen. We weten immers nooit wat we vandaag of morgen nog zullen aantreffen, ontdekken of leren.
Het laatste geldt echter niet voor vele andere 'harde' resultaten uit de meta-logica, afgezien van Gödel's bewijs: bijvoorbeeld de volledigheid van de propositie- en predikatenlogica, en de onbeslisbaarheid van de predikatenlogica. Dat zijn mogelijkheden en beperkingen die wel heel ondubbelzinnig zijn vastgesteld. De grenzen van onze menselijke bewijscapaciteit blijken dan ook in veel gevallen gebonden aan die van logische systemen. Dat dit zelden wordt erkend doet daar niets aan af.
Zijn meta-oordelen afhankelijk van bewustzijn?
Dit lijkt een redelijke aanname. Het omgekeerde is weinig waarschijnlijk: dat een mens in staat zou zijn om Gödel's bewijs ook volledig onbewust te kunnen uitvoeren. Voor zo'n niveau van intelligentie zal een bewuste toestand van het mentale proces nodig zijn. Maar dat is niet bijzonder, het geldt voor veel taken en activiteiten. De meeste mensen zijn ook niet goed in volslagen bewusteloos autorijden, enzovoorts. Goed, in theorie kan een machine het ook, maar in de praktijk hebben we voorlopig toch liever een bewuste, alerte menselijke bestuurder die de weg volgt.
(b)
Is bewustzijn afhankelijk van meta-oordelen?
Het is niet aannemelijk dat veel mensen elke keer eerst bepaalde meta-oordelen moeten vellen over hun eigen bewijs capaciteit, voordat ze tot hun gewone, alledaagse (waak)bewustzijn komen - bijvoorbeeld 's-morgens bij het ontwaken. En zeker zijn voor de bewuste toestand geen meta-algoritmische inzichten nodig die het verschil uitmaken tussen de waarheidstoekenning aan Gödel's zin, en het formele bewijs van de onmogelijkheid om die waarheid formeel te bewijzen.
(c)
Kan een mens wčl over zijn eigen bewijsmogelijkheden oordelen?
Dit kan in ieder geval in negatieve zin. We weten immers dat we een heleboel niet kunnen bewijzen. Dus voorlopig kunnen we uitgaan van een beperkte bewijscapaciteit, die dus zeker onvolledig zal zijn.
Wel is het lastig om aan onze mentale bewijscapaciteit op alle fronten specifieke, absolute grenzen te stellen. We weten immers nooit wat we vandaag of morgen nog zullen aantreffen, ontdekken of leren.
Het laatste geldt echter niet voor vele andere 'harde' resultaten uit de meta-logica, afgezien van Gödel's bewijs: bijvoorbeeld de volledigheid van de propositie- en predikatenlogica, en de onbeslisbaarheid van de predikatenlogica. Dat zijn mogelijkheden en beperkingen die wel heel ondubbelzinnig zijn vastgesteld. De grenzen van onze menselijke bewijscapaciteit blijken dan ook in veel gevallen gebonden aan die van logische systemen. Dat dit zelden wordt erkend doet daar niets aan af.
(13)
Conclusie over Gödel's bewijs en bewustzijn
Het bewijs van Gödel gaat over een specifieke categorie van systemen: consistente formele systemen van de rekenkunde. Het past een uitzonderingscategorie toe van een nogal bizar soort zinnen: globale, negatieve zelf-reflexieve meta-oordelen. Het is verder gebaseerd op een zeer speciale en complexe methode van codering: de Gödel-nummering. En globaal genomen heeft Gödel's bewijs voering enkel betrekking op 'kale' syntactische constructies, abstracte patronen die geen specifieke 'inherente' betekenis of interpretatie hebben.
Het verschijnsel bewustzijn houdt daarentegen bij uitstek verband met de meest gevarieerde en variabele betekenis die we ons - in de meest letterlijke zin - kunnen voorstellen. Het domein van Gödel's bewijs vormt daarvan hoogstens een uiterst select en beperkt deel.
Daarom kunnen we niet aannemen dat het bewijs van Gödel iets zegt over de 'bewijsbaarheid' van bewustzijn.
C.P. van der Velde, augustus 2006.