Gödels ufuldstændighedssætninger

Østrigeren Kurt Gödel slukkede i 1931 definitivt lyset for Hilberts drøm om et formelt grundlag for matematikken med sine ufuldstændighedssætninger. Nogle mennesker har fejlagtigt tolket resultaterne (udtryk for ønsketænkning ?) som, at matematikken afgik ved en brat og uventet død i 1931. Havde Gödel bevist, at de reelle tal udgjorde et inkonsistent system, ville jeg overveje at skrive dødsattesten under, men jeg ville først forsøge genoplivning ved at skifte aksiomerne ud. Tallene kom trods alt først, så de har krav på at være her. Nu var det jo trods alt ikke det, Gödel viste, og jeg har det med matematikken, som jeg har det med mit sommerhus. Huset er fra 1896. Det ser sundt og godt ud, det har stået så længe, at hvis det skulle brase sammen pga. skjulte mangler, så var det såmænd allerede sket. Jeg regner med, at det nok skal stå min tid ud.

Løst sagt siger Gödels sætninger:

Et formelt system, som omfatter de naturlige tal, er enten inkonsistent eller for svagt til, at alle sande påstande om de naturlige tal kan udledes fra aksiomerne.

Konsistensen af et sådant formelt system, kan hverken vises eller modbevises inden for systemet.

Et formelt system består af:

Symboler (herunder variable)

Syntaks, som er regler for, hvilke symbolstrenge, der er læsbare. Disse kaldes formler.

Aksiomer, som er formler, der tages for givne.

Slutningsregler, som er regler for, hvordan formler kan omformes.

Teoremerne er formler som fremkommer ved anvendelse af slutningsreglerne på aksiomerne. Systemet kaldes inkonsistent, hvis der findes en formel f, således, at både f og ~f er teoremer. 

Et bevis for et teorem i et formelt system er en streng af formler,

Gödels ide er at nummerere symboler, variable, formler og beviser. For at gøre beviset lidt enklere anvender Gödel færre logiske tegn, end vi andre bruger til dagligt. Disse tildeles numrene 1,3,..13. For eksempel har en venstreparenteser (  Gödeltallet 11.

Gödel tillader tællelig mange variable x1, x2, x3,.. og disse tildeles Gödeltal af formen p, hvis de er af type1 (tal) p2, hvis de er af type 2, p3, hvis de er af type 3.. , hvor p er primtal større end 13,

Gödeltallet for en formel defineres som , hvor n1, n2, n3,.., nk er Gödeltallene for de symboler, der indgår i formlen, og 2, 3, 5,.., pk er de første k primtal.

Gödeltallet for et bevis defineres på præcis samme måde som , hvor n1, n2, n3,.., nk er Gödeltallene for de formler, der indgår i beviset, og 2, 3, 5,.., pk er de første k primtal.

Ifølge entydigheden af primfaktoropløsningen af et naturligt tal er tildelingen af Gödeltal en injektiv afbildning af det formelle system ind i de naturlige tal. Men ikke nok med det. Vi kan angive den omvendte afbildning: Foretag primfaktoropløsningen af Gödeltallet (for bevisernes vedkommende skal eksponenterne i primfaktoropløsningen også opløses), og så har vi rekonstrueret symbolerne, formlerne og beviserne. Vi bemærker, at vi kan se, om et Gödeltal stammer fra et symbol, en formel eller et bevis:

Det formelle systems slutningsregler kan nu oversættes til regneregler for Gödeltal.

Og resultater for Gödeltal opnået vha. disse regneregler kan oversættes tilbage til udsagn om det formelle system. Det er nærliggende at sammenligne Gödels aritmetisering af metamatematikken med den analytiske geometris algebraisering af geometrien. 

Det følgende bliver meget teknisk, men grundideen er, at Gödel kan formulere en kretenser (som siger, at alle kretensere lyver) inden for det formelle system. Læseren kan overveje om følgende udsagn kan bevises: Denne sætning kan ikke bevises!

Mere præcist: Lad P(x,y) være udsagnet: Der findes et x, så x er Gödeltallet for et bevis for den formel y er Gödeltal for.

Bemærk, at vi ikke på forhånd antager, at y er et teorem. Det er altså ikke sikkert, at der til et givent y findes x, så P(x,y). Vi kan opfatte P(x,y) som et udsagn i det formelle system som følge af korrespondancen mellem det formelle system og Gödeltallene.

En af slutningsreglerne for det formelle system er, at man kan substituere et tal for en variabel. Tricket består i at substituere en (ligegyldig hvilken, bare den er af type1) variabel i en formel med Gödeltallet for formlen. Lad Q(z,y) være udsagnet: y er Gödeltallet for den formel vi får ved at indsætte z i den formel z er Gödeltal for. Lige som før kan vi opfatte kan vi opfatte Q(z,y) som et udsagn i det formelle system.

Betragt nu udsagnet i det formelle system. Det har et Gödeltal, som vi passende kan kalde g. Det er tilladt at substituere z med g, og vi får.

Dette udsagn er en matematisk version af Kretenseren , vi er nemlig ikke i stand til at afgøre, om påstanden er et teorem (uafgørbar med Gödels betegnelse) :

For ifølge definitionen af Q(z,y) er y Gödeltallet for påstanden. Hvis den var et teorem, ville det stride mod ~P(x,y). Vi er ikke så glade for selvmodsigelser, så vi forsøger igen: På den anden side, hvis y ikke er (Gödeltallet for) et teorem, så er påstanden sand. Altså findes der sande sætninger, vi ikke kan bevise.

Ovenstående skulle gøre det ud for en bevisskitse til den første af de anførte ufuldstændighedssætninger. Gödel går videre og viser, at en af de uafgørbare påstande er: Dette system er konsistent.

Idet vi undertrykker vor kvalme over de ideologiske undertoner på web-stedet, henleder vi læserens opmærksomhed på den fremragende web-udgave af Gödels On Formally Undecidable Propositions of Principia Mathematica and Related Systems 1 på www.ddc.net/ygg/etext/godel. Gödels noter er klikbare, så man ikke skal sidde og bladre. Oversætteren forord og introduktionen er ligeledes forsynet med links til de relevante steder i artiklen og til baggrundsoplysninger i Stanford Encyclopedia of Philosophy.