> Mat.'s ufuldstændighed > Gödels bevis (2) Udskriv denne side
     
Matematikkens ufuldstændighed
         
Se også:
Index og søg
Udskriv siden
         

Gödels bevis (2)

Gödels strategi
Gödels bevis og resultat trin for trin
Kommentarer

Især baseret på: Douglas R. Hofstadter: "Gödel, Escher, Bach - an Eternal Golden Braid", Basic Books, Inc., Publishers, New York, 1979.

Flere kilder

 

Sidens topGödels strategi

Hvis Gödels bevis alene havde været baseret på det selvrefererende udsagn G: "Udsagnet G kan ikke  bevises i det formelle system F"  samt de efterfølgende logiske slutninger (som fremstillet i "Gödels bevis (1)"), så ville beviset for matematikkens ufuldstændighed let have kunnet afvises. For de forskellige skridt i ræsonnementet bevæger sig temmelig vilkårligt mellem flere forskellige niveauer, såvel indenfor som udenfor det formelle system F. Og vi blev jo netop belært om i MU pusleriet at det er vigtigt at skelne mellem, om vi arbejder i M-mode (indenfor) eller i I-mode (udenfor) det formelle system. Man kan jo som vist i "Paradokser" lave masser af sære selvrefererende sproglige konstruktioner, men hvis de ikke kan importeres i det indre af de matematiske formelle systemer, så kan disse leve videre uanfægtet.

Det geniale i Gödels arbejde er, at han ikke blot tager udgangspunkt i selvrefererende udsagn, men at han ved hjælp af et sindrigt afbildningssystem viser, at man kan importere disse udsagn, så de kommer indenfor det formelle system F. Herved repræsenterer disse udsagn både strenge indenfor F, samtidig med at de udtaler sig om F.

Gödels strategi omfatter ethvert formelt system F som er "tilstrækkelig kraftigt". MIU-systemet opfylder ikke dette, men kan alligevel bruges til at illustrere nogle af trinene i strategien.

Kriteriet for det formelle system F, at det skal være "tilstrækkelig kraftigt", skal naturligvis specificeres - og bliver det i moderne udgave ved at kræve at de såkaldte "primitive rekursive funktioner" i alt fald skal være repræsenteret i F.

Gödels strategi præsenteres her og uddybes derefter trin for trin:

  1. Gödel-nummerering. Gödel laver en slags "kode" som kan bruges i F. Til hver(t) symbol, streng, aksiom, teorem og bevis for teorem lader man entydigt svare et positivt heltal.
  2. Aritmetisering. Gödel viser, at slutningsreglerne i F kodet ved Gödel-nummerering entydigt svarer til aritmetiske regler, dvs. regler om tal indenfor talteori.
  3. "F-numre" er de tal som er dannet ved de aritmetiske regler, og netop disse tal (Gödel-numre) svarer til teoremerne i F. F.eks. vil "MIU-numrene" svare til de strenge vi har i "MIU-posen", altså teoremerne i MIU-systemet.
  4. Udsagn om det formelle system (f.eks. om MU er et teorem i MIU-systemet, dvs. findes i "MIU-posen") kan så entydigt omformes til et talteoretisk spørgsmål om egenskaber ved bestemte tal (f.eks. om Gödel-nummeret svarende til MU er et MIU-nummer).
  5. Egenskaber ved tal svarer til strenge i det formelle system TTT (Typografisk Teori for Tal). Derfor kan udsagn om det formelle system F via spørgsmålet om tals egenskaber omformes videre til spørgsmål om bestemte strenge er eller ikke er teoremer indenfor TTT.
    Samlet fører punkterne 1 - 5 til at et udsagn om MIU-systemet er ækvivalent med et talteoretisk udsagn som igen er ækvivalent med en bestemt streng indenfor TTT.
  6. Da TTT jo selv er et formelt system, kan også TTT kodes ved Gödel-nummerering. Men så kan udsagn om TTT (f.eks. om en bestemt streng er et teorem eller ej i TTT) omformuleres til et talteoretisk spørgsmål om egenskaber ved bestemte tal (f.eks. om Gödel-nummeret svarende til en bestemt streng i TTT er et "TTT-nummer"). Og disse talteoretiske egenskaber kan igen omformes videre til bestemte strenge i TTT. På denne måde kan strenge indenfor TTT svare til udsagn om TTT. TTT "taler i kode" om sig selv.
  7. Gödel konstruerer nu en streng i TTT, kaldet G, som svarer til en bestem egenskab ved tal, og som samtidig svarer til et udsagn om TTT, nemlig: "G er ikke et teorem i TTT".
  8. Ved at følge de logiske slutninger fra "Gödels bevis (1)" kommer Gödel frem til følgende resultat:
    Forudsat af det formelle system TTT er konsistent, findes der i TTT en streng G som entydigt svarer til et udsagn om bestemte aritmetiske egenskaber ved hele positive tal. Ved logiske ræsonnementer udenfor systemet finder vi desuden at denne streng ikke er et teorem i TTT (dvs. ikke kan bevises indenfor TTT) og at det tilsvarende udsagn er sandt.
    Dette er en formulering af Gödels første ufuldstændighedsteorem.
  9. Gödel viser dernæst, at selv om vi har gode grunde til at tro på at TTT er konsistent, gælder:
    Der findes ikke indenfor TTT et bevis for at TTT er konsistent.
    Dette er en formulering af Gödels andet ufuldstændighedsteorem.

 

Sidens topGödels bevis, trin for trin

Vi benytter MIU-systemet som eksempel på et formelt system.

1. Gödel-nummerering

Symbolerne i MIU-systemet kan f.eks. entydigt nummereres således:

3
  1
0

Slutningsreglerne (x og y står for streng af tal, 0, 1 og 3):

  1. Af  x1       kan dannes  x10
  2. Af  3x      kan dannes  3xx
  3. Af  x111y  kan dannes  x0y
  4. Af  x00y  kan dannes xy

Aksiom:

MI  31

Bevis for teoremet MUIIU ( 30110):

31 311 31111 301 3010 3010010 30110

Hele udledningen, bevis samt endeligt resultat, tildeles Gödel-nummeret:
31311311113013010301001030110
Bemærk at nummeret er entydigt, idet 3-tallerne sikrer adskillelsen mellem de enkelte MIU-numre for strengene.

 

2. Aritmetisering

De fire slutningsregler kan omformes til aritmetiske regler for tal. Her vist for MIU-systemet:.

m, k og n er vilkårlige hele positive tal og n er mindre end 10m:

  1. Af  10m + 1   kan dannes   10•(10m + 1)
    Eks.: med m = 30 fås: 301 3010

  2. Af  3•10m + n   kan dannes   10m •(3•10m + n) + n
    Eks.: med m = 1 og n = 1 fås: 31 311
    Eks: med m = 3 og n = 10 fås: 3010 3010010

  3. Af k•10m+3 + 111•10m + n   kan dannes   k•10m+1 + n
    Eks.: med m = 1, n = 1 og k = 3 fås: 31111 301

  4. Af k•10m+2 + n   kan dannes   k•10m + n
    Eks.: med m = 2, n = 10 og k = 301 fås: 3010010 30110

Det centrale princip som her er demonstreret ved et eksempel, siger:

Typografiske regler for manipulationer af Gödel-numre
kan altid repræsenteres ved aritmetiske regler for operationer med tal.

 

3. "MIU-numre"

Med udgangspunktet i aksiomet 31 (MI) og brug af de aritmetiske regler kan vi danne nye tal (f.eks. tallet 30110), og disse tal svarer til teoremerne i det formelle system (f.eks. MUIIU).

I MIU-systemet kaldes tal som er Gödel-numre for aksiom eller teoremer for "MIU-numre".

F.eks. er 30110 et MIU-nummer, men 30 er ikke et MIU-nummer.

 

4. Teoremhed i MIU og egenskaben MIU-nummer

Et spørgsmål om MIU-systemet, f.eks: "Er MU et teorem i MIU-systemet?"
kan omformes til et
talteoretisk spørgsmål: "Er 30 et MIU-nummer?".

Der spørges altså om en egenskab ved tallet 30, nemlig om det er muligt ved hjælp af de fire slutningsregler i aritmetisk form at komme fra tallet 31 til tallet 30.

 

5. Egenskaben MIU-nummer og MUgnr-strengen i TTT

Den talteoretiske egenskab "30 er et MIU-nummer" kan omformes til en streng indenfor det formelle system TTT (Typografisk Teori om Tal).
Da denne streng er resultat af Gödel-nummerering kalder vi den "
MUgnr-strengen".

Det er en lang og kompliceret procedure udenfor rammerne af dette skrift at finde frem til denne streng i TTT.

Spørgsmålet "Er 30 et MIU-nummer?"
kan så omformes til: "Er MUgnr-strengen et teorem indenfor TTT"?
eller tilsvarende: "Kan MUgnr-strengen bevises indenfor TTT?"

Samles punkt 4 og 5 kan vi sige:

Udsagnet om MIU-systemet: "MU er et teorem i MIU-systemet"
er ved hjælp af Gödel-nummerering blevet "kodet over"
i en
talteoretisk egenskab "30 er et MIU-nummer",
og denne er igen blevet udskrevet
som
MUgnr-strengen ved hjælp af symbolerne i TTT.

Svaret "ja" til spørgsmålet "Er MU et teorem i MIU-systemet" er ækvivalent til svaret "ja" til spørgsmålet "30 er et MIU-nummer" og dette er igen ækvivalent til at MUgnr-strengen er et teorem i TTT. Tilsvarende svarer "nej" til de to første spørgsmål til at MUgnr-strengen ikke er et teorem i TTT (dvs. ikke kan bevises indenfor TTT).

 

6. Samme procedure med TTT

Hele processen i punkterne 1-5 kan lige så vel gennemføres på det formelle system TTT, Typografisk Teori for Tal, omend det detaljerne bliver meget mere komplicerede:

  1. Gödel-nummerering af TTT.
  2. Aritmetisering af slutningsreglerne.
  3. Definition af "TTT-numre" som de tal det er muligt at frembringe ved hjælp af de aritmetiserede slutningsregler ud fra Gödel numrene for aksiomerne og tidligere frembragte TTT-numre.
  4. Teoremhed i TTT svarer til en egenskab ved TTT-numre. Hvis A står for en streng i TTTog a for det tilsvarende Gödel-nummer, svarer egenskaben om TTT: "A et teorem i TTT" til den talteoretiske egenskab "a er et TTT-nummer".
  5. Den talteoretiske egenskab "a er et TTT-nummer" kan omformes til en streng i TTT, kaldet "Agnr-strengen". Nu er spørgsmålet om "A er et teorem i TTT?" ækvivalent med spørgsmålet om "a er et TTT-nummer?" og dette er igen ækvivalent med spørgsmålet om Agnr-strengen er et teorem i TTT.
    Bemærk at de to strenge i TTT, A og Agnr, ikke er identiske. A var den oprindelige streng i TTT, mens Agnr er en streng skabt ved Gödel-nummerering af TTT. Tager vi processen baglæns kan vi sige:
    • Agnr er en streng indenfor TTT
    • som er kode for en talteoretisk egenskab ("a er et TTT-nummer")
    • som igen er kode for et udsagn om TTT ("A er et teorem i TTT").

 

7. Opbygning af strengen G

Vejen til Gödels streng G i TTT som skal svare til udsagnet om TTT, "G er ikke et teorem" går via to egenskaber ved tal: "Bevispar" og "Substitutionstriple".

 

7A. På vej til opbygning af strengen G: "Bevispar"

I punkt 1 vistes at vi ved hjælp af Gödel-nummerering af MIU-systemet ikke blot kan nummerere de enkelte symboler og strenge, men også hele beviser for teoremer.

F.eks. svarer nummeret 31311311113013010301001030110 til beviset for MUIIU.

Dette tal kan deles i to dele:

  1. m = 313113111130130103010010 svarende udledningen i beviset minus konklusionen
  2. n = 30110 svarende til konklusionen i beviset, nemlig at MUIIU er et teorem.

Dette fører til følgende definition:

To hele positive tal, m og n respektive, udgør et "MIU-bevispar" hvis og kun hvis m er Gödel-nummeret for udledningen i beviset for strengen med Gödel-nummeret n.

Da slutningsreglerne i MIU-systemet svarer til aritmetiske operationer, vil egenskaben at to tal m og n udgør et MIU-bevispar svare til en talteoretisk egenskab som betegnes således:

MIU-bevispar(m,n)

Men talteoretiske egenskaber kan repræsenteres ved strenge i TTT.
For ikke at komplicere fremstillingen yderligere vil vi tillade os at lade betegnelsen MIU-bevispar(m,n) også stå for den tilsvarende streng i TTT.

En tilsvarende definition kan laves i TTT-systemet med den talteoretiske egenskab

TTT-bevispar(m,n)

og denne kan tilsvarende repræsenteres ved en streng i TTT som netop er et teorem i TTT hvis den talteoretiske egenskab er opfyldt.

Det er faktisk ikke en selvfølge at den talteoretiske egenskab TTT-bevispar(m,n) kan repræsenteres ved en streng i TTT. En tilstrækkelig betingelse for at dette kan lade sig gøre er, at den talteoretiske egenskab er "primitiv rekursiv". Det kan vises at TTT-bevispar(m,n) opfylder denne betingelse.

For et givet m og n er det muligt at undersøge om de har egenskaben TTT-bevispar(m,n). Vi skal jo "blot" checke om den udledning som m svarer til, fører til konklusionen som n svarer til.

Det er en ganske anden sag med følgende udsagn om et givet tal b:

Der eksisterer et a så: TTT-bevispar(a,b).

Udtrykt i almindelige vendinger:

"Der findes et bevis (m. Gödel-nummer a) for TTT-strengen med Gödel-nummer b".

Eller:

"TTT-strengen med Gödel-nummer b er et teorem i TTT" .

Også dette udsagn om TTT svarer til en talteoretisk egenskab, og den kan udtrykkes i TTT ved en streng. Men det er absolut ikke trivielt at afgøre om udsagnet er sandt eller at strengen er et teorem i TTT. For dette svarer jo til at finde frem til at bevis (eller modbevis) for en talteoretisk sætning - den centrale og vanskelige opgave i matematik.

 

7B. På vej til opbygning af strengen G: "Substitutiontriple"

Her bliver det lidt sværere, men vi kaster os hovedkuls ud i definitionen:

Tre hele positive tal, m, k og n respektive, udgør et "TTT-substitutionstriple" netop hvis vi kan komme fra strengen med Gödel-nummeret m til strengen med Gödel-nummeret n ved at erstatte alle frie variable i m-strengen med tallet k.

Den tilsvarende talteoretiske egenskab skrives således:

TTT-sub(m,k,n)

og denne kan tilsvarende repræsenteres ved en streng i TTT.

Med 'fri variabel' menes et bogstav, f.eks. x, som endnu ikke er fastlagt til at være noget bestemt.
Et talteoretisk udsagn med en fri variabel kaldes et "åbent udsagn".

 

Eksempel:
Det talteoretiske udsagn som repræsenteret som streng i TTT har Gödel-nummer m:

"Der findes ikke to hele positive tal, a og b, således at ab = x"

indeholder den frie variabel x. Hvis vi erstatter x med tallet 4 fås det talteoretiske udsagn som repræsenteret som streng i TTT har Gödel-nummer n:

"Der findes ikke to hele positive tal, a og b, således at ab = 4"

Der gælder så:

TTT-sub(m,4,n)

og som streng i TTT vil dette være et teorem i TTT.

Bemærk at det her ikke har betydning om strengen med Gödel-nummeret n svarer til en sand talteoretisk egenskab. (I dette eksempel er egenskaben falsk, for a = b = 2 opfylder jo at ab = 4).

 

7C. Opbygning af strengen G: brug af "Bevispar" og "Substitutiontriple"

For at nå frem til strengen G opstiller vi først en streng U svarende til følgende udsagn ('tal' står for hele positive tal):

U: "Der findes ikke to tal, a og b, således at TTT-bevispar(a,b) og TTT-sub(x,x,b)"

Også dette udsagn om TTT svarer til en talteoretisk egenskab, og den kan udtrykkes i TTT ved en streng som vi for nemheds skyld også vil kalde U.

Husk at TTT-bevispar(a,b) svarer til at "slutnings-kæden af strenge med Gödel-nummer a udgør et bevis for strengen med Gödel-nummer b".

Bemærk at U indeholder en fri variabel x og at x spiller en dobbelt rolle i TTT-sub(x,x,b):

  1. x står for Gödel-nummeret for en streng
  2. x står for det tal som alle frie variable i x-strengen skal erstattes med for at frembringe b-strengen.

TTT-sub(x,x,b) siger med andre ord:

strengen med Gödel-nummer b frembringes ved at erstatte alle frie variable i strengen med Gödel-nummer x med x-strengens eget Gödel-nummer!

Nu bliver det endnu sjovere:

Strengen U har naturligvis et Gödel-nummer, lad os kalde det u.

Vi frembringer nu en ny streng, kaldet G, ved at erstatte alle frie variable i strengen U med u, altså med U's eget Gödel-nummer. Da x er den frie variable fås at strengen G svarer til udsagnet:

G: "Der findes ikke to tal, a og b, således at TTT-bevispar(a,b) og TTT-sub(u,u,b)".

Og dette svarer minsandten til den eftertragtede streng (også kaldet G) i Gödels bevis.

Lad os prøve at forstå hvorfor ved at spørge:

  1. Hvad er G's Gödel-nummer?
  2. Hvordan kan G fortolkes?

ad A:
Lad os kalde G's Gödel-nummer for g. G blev skabt ved at erstatte alle frie variable i strengen U med U's eget Gödel-nummer u. Denne proces kan beskives ved TTT-sub(u,u,g). Tallet g er Gödel-nummeret for den resulterende streng G, derfor er tallet g resultatet af denne proces.

ad B:
Fortolkningen eller "oversættelsen" til mere almindeligt dansk af G kan nu skrives i en række stadig mere forståelige trin:

  1. G: "Der findes ikke to tal, a og b, således at (a,b) udgør et TTT-bevispar og (u,u,b) udgør et TTT-substitutionstriple."

  2. G: "Der findes ikke to tal, a og b, således at a er Gödel-nummeret for den kæde af strenge som udgør beviset for strengen med Gödel-nummeret b, og således at b er Gödel-nummeret for den streng som fås ved i strengen med Gödel-nummeret u at erstatte alle frie variable med u."

    Men strengen med Gödel-nummeret u er jo U. Så vi ved allerede hvad b er. For vi kender den streng som fås ved i strengen U at erstatte alle frie variable med u. Det er jo G med Gödel-nummeret g. Altså er b = g. Vi kan så "oversætte" G til:

  3. G: "Der findes ikke et tal a, således at a er Gödel-nummeret for den kæde af strenge som udgør beviset for strengen med Gödel-nummeret g."

  4. G: "Der findes ikke noget bevis for strengen G"

  5. G: "G er ikke et teorem i TTT"

 

8. Gödels første ufuldstændighedsteorem

Strengen G er bygget op indenfor det formelle system TTT. Derefter har vi udenfor TTT foretaget en fortolkning af G. Stadig udenfor TTT kan vi nu foretage den videre logiske undersøgelse af konsekvenserne. Det blev gjort i "Gödels bevis (1)", men gentages her i lidt andre vendinger:

G: "G er ikke et teorem i TTT"

  • Vi antager for hele det følgende ræsonnement:
    K: "TTT er konsistent (modsigelsesfrit)"

 

  • Vi antager at G er et teorem i TTT.
  • Da G siger det modsatte, må G være falsk.
  • I et konsistent formelt system er alle teoremer sande, og så må G være sand.
  • Men G kan ikke både være falsk og sand, så vi er kommet til en modstrid.
  • Derfor må vores antagelse, at G er et teorem i TTT, være forkert.
  • Altså er G ikke et teorem i TTT.

 

  • Vi ved nu at G ikke er et teorem i TTT.
  • Men det er jo netop hvad G siger.
  • Altså må G være sand.

 

  1. Vi ved nu at G ikke er et teorem i TTT, men alligevel sand.
  2. Det formelle system TTT er ufuldstændigt.

Dette er Gödels første ufuldstændighedsteorem.

Da hele dette ræsonnement blev gennemført under antagelsen at TTT er konsistent, kan resultatet også formuleres:

  • Det formelle system TTT er enten inkonsistent eller ufuldstændigt.

Kunne det tænkes at non G (at G ikke gælder) er et teorem i TTT?

  • Nej, for vi ved hvis G er sand, og så må non G være falsk.
  • Da teoremer i et konsistent formelt system altid er sande, kan non G ikke være et teorem i TTT.

Kunne man så ikke tilføje G til aksomerne for TTT?

  • Det kan man godt, men det nye formelle system, TTT', vil på samme måde som TTT give mulighed for en streng, G', af samme type som G, og så er vi lige vidt.

 

9. Gödels andet ufuldstændighedsteorem

Hvordan kan man formulere at et formelt system, f.eks. TTT, er inkonsistent?
Man konstaterer inkonsistens ved at vise, at det formelle systems aksiomer og slutningsregler gør det muligt at bevise både at noget gælder og ikke gælder. Eller lidt mere korrekt udtrykt:
At der findes mindst én streng S, således at både S og non S er teoremer.

Udsagnslogikken er en del af TTT og dette omfatter bl.a. også symboler svarende til 'non' ('ikke' - benægtelse af noget), 'og', 'medfører' ().

Det er muligt at vise teoremet:

"(P og non P) Q" for vilkårlige P og Q.

Det får den konsekvens at man i et inkonsistent formelt system kan bevise, at "hvad som helst" er teoremer. For hvis både S og non S er teoremer fås: (S og non S) Q for vilkårlige Q.

For at udtrykke at TTT er konsistent, skal vi altså blot finde én streng som ikke er et teorem.
Vi kan derfor udtrykke konsistens ved udsagnet (og strengen):

K: Der findes et tal y, således at der for alle tal x gælder: non TTT-bevispar(x,y)

K udtrykker jo netop at der i TTT findes mindst én streng y som ikke kan bevises og derfor ikke kan være et teorem.

Det er desuden muligt indenfor TTT at bevise et teorem svarende til udsagnet:

"K G"

I ord:

"Hvis TTT er konsistent, så er G et teorem i TTT".

Der findes i udsagnslogikken (som er en del af TTT) et teorem svarende til udsagnet:

"(P og (P Q)) Q"

eller i ord:

"Hvis vi ved at P gælder og at P medføre Q, så gælder også Q".

Dette teorem kaldes i udsagnslogikken 'modus ponens' eller 'rule of detachment'.

Samlet har vi nu:

  • "K G" er et teorem i TTT
  • Antag at K er et teorem i TTT
    altså at det er muligt at bevise at TTT er konsistent.
  • Af 'modul ponens' fås så at G er et teorem.
  • Vi har så indenfor TTT gennemført et bevis for at G er et teorem.
  • Men dette strider mod at vi i Gödels bevis for første fuldstændighedsteorem som resultat fandt at G ikke er et teorem i TTT.
  • Altså må antagelsen være forkert: Konsistensen af TTT kan ikke bevises.

Dette er Gödels andet ufuldstændighedsteorem.

 

Sidens topKommentarer

Vores tro på TTT som formelt system er blevet rystet. TTT skulle jo gerne "indfange" talteorien og logikken, dvs. give resultater i form af teoremer som stemmer overens med hvad vi mener er sandt på disse områder. Det gør TTT særdeles godt. Men alligevel viser det sig at TTT indeholder mindst én streng (G) som ikke er et teorem og hvis tilsvarende fortolkning alligevel er et sandt udsagn. TTT kan ikke "nå ud til" alle sande udsagn om tal. Hvis TTT antages konsistent, kan TTT ikke samtidig være fuldstændigt.

Man kunne forestille sig at problemet med TTT er, at det bare ikke er "godt nok". Men Gödel viser at problemet opstår i alle formelle systemer som er "stærke nok" til at beskrive tal. Og det hjælper ikke engang at ophøje den fundne streng G til et aksiom, for så affødes blot en ny problemstreng G'.

Selv om konsistensen af TTT ikke kan bevises indenfor TTT, har vi dog gode grunde til at tro på at TTT er konsistent, fordi dette formelle system ser ud til at stemme godt overens med vores forventninger til tallenes egenskaber. Talteorien udgør en "model" for TTT. Så vi tror på at TTT er konsistent, men ved at vi ikke kan bevise dette indenfor TTT.

Det kan nok undre, at det skulle være så svært at bevise konsistensen af et formelt system, hvis man blot skal finde én streng som ikke er et teorem. Men det viser sig at dette problem hænger sammen  med om der findes en afgørlighedsprocedure for teoremhed (som omtalt under "MU pusleriet").

For udsagnslogikken (som udgør en underafdeling af TTT) findes en afgørlighedsprocedure for teoremhed baseret på den teknik som kaldes "sandhedstavler" som tildeler '0' for falskheder og '1' for sandheder. Teoremerne er netop de strenge som svarer til udsagn hvis sandhedstavle kun indeholder 1'er, også kaldet 'tautologier'. Derfor kan konsistensen af udsagnslogikken bevises.

For TTT som helhed kan man bevise, at hvis TTT antages konsistent, så er strengen for konsistens, K, ikke et teorem indenfor TTT.  Temmelig aparte. Der findes ingen afgørlighedsprocedure for teoremhed i TTT - hvis der gjorde, ville vi kunne bruge den til at bevise at TTT er konsistent.

Det konkrete problem, at finde en streng, y,for hvilken man vil bevise at y ikke er et teorem i TTT, hænger sammen med at vi skal sikre os, at der ikke findes nogen slutningskæder af strenge, x, således at (x,y) er et bevispar. Og dette problem er uafgørligt. Det hænger sammen med at problemet ikke kan løses som en 'primitiv rekursiv procedure', og dette igen vil sige en procedure som med garanti kan løses i et endeligt antal skridt.

Strengen G og dens tilsvarende talteoretiske udsagn er jo temmelig speciel. Men der er dukket andre mere "meningsfulde" (omend komplicerede) eksempler op på talteoretiske udsagn om egenskaber ved tal, som må være sande, men som ikke kan bevises. Det berømteste eksempel er den såkaldte "kontinuums-hypotese".

 

Sidens topSe videre: To citater om matematik

Opdateret 5-11-2011 , TM

 
Sidens top