Godels ofullständighetsteorem

Godels ofullständighetsteorem och Godels andra sats [~ 1]  är två matematiska logiska satser om de grundläggande begränsningarna för formell aritmetik och, som en konsekvens av detta, för alla formellt system där de grundläggande aritmetiska begreppen kan definieras: naturliga tal , 0 , 1 , addition och multiplikation .

Den första satsen säger att om formell aritmetik är konsekvent, så innehåller den en obestridlig och obestridlig formel.

Den andra satsen hävdar att om en formell aritmetik är konsekvent, så är någon formel icke härledbar i den som på ett meningsfullt sätt hävdar konsistensen av denna aritmetik.

Båda dessa satser bevisades av Kurt Gödel 1930 (publicerad 1931) och är direkt relaterade till det andra problemet i Hilberts berömda lista .

Historik

Redan i början av 1900-talet proklamerade David Hilbert målet att axiomatisera all matematik, och för att slutföra denna uppgift återstod det att bevisa konsekvensen och den logiska fullständigheten i aritmetiken av naturliga tal . Den 7 september 1930 hölls en vetenskaplig kongress om matematikens grunder i Königsberg och vid denna kongress publicerade den 24-årige Kurt Gödel först två grundläggande ofullständighetssatser, som visade att Hilberts program inte kan förverkligas: för ev. val av axiom för aritmetik, det finns satser som är omöjliga att varken bevisa eller motbevisa med enkla ( finita ) medel från Hilbert, och ett ändligt bevis för aritmetikens konsistens är omöjligt [6] .

Detta tal tillkännagavs inte i förväg och hade en fantastisk effekt, Gödel blev omedelbart en världskändis, och Hilberts program för att formalisera matematikens grunder krävde en brådskande översyn. Den 23 oktober 1930 presenterades Gödels resultat för vetenskapsakademien i Wien av Hans Hahn . En artikel med båda satserna (" On fundamentally undecidable propositions in Principia Mathematica and related systems ") publicerades i den vetenskapliga månadsskriften Monatshefte für Mathematik und Physik 1931. Även om Gödel gav beviset för den andra satsen endast i form av en idé, var hans resultat så tydligt och obestridligt att ingen tvivlade på det. Hilbert insåg genast värdet av Gödels upptäckter; de första fullständiga bevisen för båda satserna publicerades i Hilbert och Bernays Foundations of Mathematics (1938). I förordet till den andra volymen erkände författarna att finita metoder inte räcker för att uppnå sitt mål, och lade till transfinit induktion till listan över logiska medel ; 1936 lyckades Gerhard Gentzen bevisa aritmetikens konsistens med detta axiom, men logisk fullständighet förblev ouppnåelig [6]

Godels ofullständighetsteorem

I sin ursprungliga form

I sin formulering av ofullständighetssatsen använde Gödel begreppet ett ω-konsistent formellt system, ett starkare villkor än enbart konsistens. Ett formellt system kallas ω-konsistent om det för någon formel A ( x ) i detta system är omöjligt att samtidigt härleda formlerna A ( 0 ), A ( 1 ), A ( 2 ), ... och ∃ x ¬ A ( x ) (med andra ord, av det faktum att formeln A ( n ) är härledbar för varje naturligt tal n , följer att formeln ∃ x ¬ A ( x ) inte är härledbar). Det är lätt att visa att ω-konsistens innebär enkel konsistens (det vill säga alla ω-konsistenta formella system är konsekventa) [7] .

I processen att bevisa satsen konstrueras en sådan formel A för ett aritmetiskt formellt system S att [7] :

Om det formella systemet S är konsekvent, är formeln A inte härledbar i S ; om systemet S är ω-konsistent, är formeln ¬A inte härledbar i S . Således, om ett system S är ω-konsistent, så är det ofullständigt [~ 2] och A är ett exempel på en olöslig formel.

Formeln A kallas ibland Gödel olösliga formel [8] .

Tolkning av den olösliga formeln

I standardtolkningen [~ 3] betyder formeln A "det finns ingen härledning av formeln A ", det vill säga hävdar sin egen icke-deriverbarhet i S. Därför, med Gödels sats, om bara systemet S är konsekvent, då är denna formel verkligen icke-deriverbar i S och därför sann i standardtolkningen. Således, för naturliga tal är formeln A sann, men i S är den inte härledbar [9] .

I Rosser uniform

I processen att bevisa satsen konstrueras en sådan formel B för ett aritmetiskt formellt system S att [10] :

Om ett formellt system S är konsekvent, är både formler B och ¬B icke härledbara i det; med andra ord, om systemet S är konsekvent, så är det ofullständigt [~ 2] , och B är ett exempel på en olöslig formel.

Formeln B kallas ibland Rossers olösliga formel [11] . Denna formel är lite mer komplicerad än Gödels.

Tolkning av den olösliga formeln

I standardtolkningen [~3] betyder formel B "om det finns en härledning av formel B , så finns det en härledning av formel ¬B " . Men enligt Gödels teorem i form av Rosser, om ett formellt system S är konsekvent, så är formeln B i det icke-deriverbar; därför, om systemet S är konsekvent, då är formeln B korrekt i standardtolkningen [12] .

Generaliserade formuleringar

Beviset för Gödels sats utförs vanligtvis för ett specifikt formellt system (inte nödvändigtvis samma), och följaktligen visar sig satsens påstående vara bevisat endast för detta system. Studiet av tillräckliga villkor som ett formellt system måste uppfylla för att kunna bevisa dess ofullständighet leder till generaliseringar av satsen till en bred klass av formella system. Ett exempel på en generaliserad formulering [13] :

Varje tillräckligt stark rekursivt axiomatiserbar konsekvent första ordningens teori är ofullständig.

I synnerhet gäller Gödels teorem för varje konsekvent ändligt axiomatiserbar förlängning av ett aritmetiskt formellt system S.

Polynomform

Efter att Yuri Matiyasevich bevisat att vilken som helst uppräknbar mängd är diofant och exempel på universella diofantiska ekvationer hittades , blev det möjligt att formulera ofullständighetssatsen i polynom (eller diofantisk) form [14] [15] [16] [17] :

För varje konsekvent teori T kan man specificera ett heltalsvärde för parametern K så att ekvationen har inga lösningar i icke-negativa heltal, men detta faktum kan inte bevisas i teorin T . Dessutom, för varje konsekvent teori, är uppsättningen värden för parametern K som har denna egenskap oändlig och algoritmiskt omräknad .

Graden av denna ekvation kan reduceras till 4 till priset av att antalet variabler ökar.

Skiss av beviset

I sin artikel ger Gödel en översikt över bevisets huvudidéer [18] , som återges nedan med smärre modifieringar.

Varje primitiv symbol, uttryck och sekvens av uttryck för något formellt system [~ 4] S kommer att associeras med ett visst naturligt tal [~ 5] . Matematiska begrepp och påståenden blir alltså begrepp och påståenden om naturliga tal, och kan därför själva uttryckas i symboliken för systemet S. Det kan särskilt visas att begreppen "formel", "avledning", "deriverbar" formel" är definierbara inom systemet S, det vill säga det är möjligt att återställa till exempel en formel F ( v ) i S med en fri naturlig talvariabel v så att F ( v ), i en intuitiv tolkning, betyder: v  är en härledbar formel. Låt oss nu konstruera en obestämbar mening av systemet S, det vill säga en mening A för vilken varken A eller icke-A är icke- härledbara, enligt följande:

En formel i S med exakt en fri naturlig talvariabel kallas ett klassuttryck . Låt oss ordna klassuttryck till en sekvens på något sätt, beteckna n:te med R ( n ), och notera att begreppet "klassuttryck", såväl som ordningsrelationen R , kan definieras i systemet S. Låt oss definiera a vara ett godtyckligt klassuttrycksuttryck; genom [α; n ] beteckna formeln som bildas av klassuttrycket α genom att ersätta den fria variabeln med symbolen för ett naturligt tal n . Ternär relation x = [ y ; z ] visar sig också vara definierbar i S. Nu definierar vi klassen K för naturliga tal enligt följande:

n ∈ K ≡ ¬Bew[ R ( n ); n ] (*)

(där Bew x betyder: x  är den härledda formeln [~ 6] ). Eftersom alla definierande begrepp från denna definition kan uttryckas i S, gäller detsamma för begreppet K , som är konstruerat utifrån dem, det vill säga det finns ett sådant klassuttryck C att formeln [ C ; n ], vilket intuitivt tolkas, betyder att ett naturligt tal n tillhör K . Som klassuttryck är C identisk med något speciellt R ( q ) i vår uppräkning, d.v.s.

C = R ( q )

gäller för något bestämt naturligt tal q . Låt oss nu visa att meningen [ R ( q ); q ] är obestämbar i S. Således, om meningen [ R ( q ); q ] antas vara härledbart, då visar det sig vara sant, det vill säga enligt ovan kommer q att tillhöra K , det vill säga enligt (*), ¬Bew[ R ( q ); q ], vilket motsäger vårt antagande. Å andra sidan, om vi antar härledbar negationen [ R ( q ); q ], då kommer ¬ q ∈ K att äga rum , det vill säga Bew[ R ( q ); q ] kommer att vara sant. Därför [ R ( q ); q ] tillsammans med dess negation kommer att kunna härledas, vilket återigen är omöjligt.

Samband med paradoxer

I standardtolkningen [~3] betyder Gödels oavgjorda formel A "det finns ingen härledning av formeln A ", det vill säga hävdar sin egen icke-deriverbarhet i systemet S. Således är A analogen till lögnarparadoxen . Gödels resonemang påminner i stort sett mycket om Richards paradox . Dessutom kan vilken semantisk paradox som helst användas för att bevisa förekomsten av icke-deriverbara uttalanden [19] .

Det bör noteras att påståendet uttryckt av formel A inte innehåller en ond cirkel, eftersom det till en början bara hävdas att någon specifik formel, vars uttryckliga uttryck är lätt (om än besvärligt), är obevisbar. "Först senare (och så att säga av en slump) visar det sig att denna formel är exakt den som uttrycker detta påstående i sig" [19] .

Gödels andra sats

I formell aritmetik S kan man konstruera en formel som, i standardtolkningen [~ 3] , är sann om och bara om teorin S är konsekvent. För denna formel är påståendet i Gödels andra sats sant:

Om en formell aritmetisk S är konsekvent, så finns det ingen härledbar formel i den som på ett meningsfullt sätt hävdar konsistensen av S .

Med andra ord, konsistensen av formell aritmetik kan inte bevisas med hjälp av denna teori. Det kan dock finnas bevis på konsistensen av formell aritmetik med hjälp av medel som inte kan uttryckas i den.

Skiss av beviset

Först konstrueras en formel Con , som på ett meningsfullt sätt uttrycker omöjligheten att härleda någon formel i teorin S, tillsammans med dess negation. Då uttrycks påståendet av Gödels första sats med formeln Con ⊃ G , där G  är en Gödel olöslig formel. Alla argument för beviset för den första satsen kan uttryckas och utföras med hjälp av S, det vill säga formeln Con ⊃ G är härledbar i S. Därför, om Con är härledbart i S , så är G också härledbart i det . Men enligt Gödels första sats, om S är konsekvent, så är G icke-deriverbar i den. Därför, om S är konsekvent, är formeln Con inte heller härledbar i den .

Historiskt inflytande

Experter ger mycket olika, ibland till och med polära, bedömningar av den historiska betydelsen av Gödels satser. Vissa vetenskapsmän tror att dessa satser "vände på" grunderna för matematiken eller till och med hela kunskapsteorin , och betydelsen av Gödels briljanta upptäckt kommer gradvis att avslöjas under lång tid framöver [20] . Andra (till exempel Bertrand Russell ) uppmanar till att inte överdriva, eftersom satserna är baserade på Hilberts finita formalism [21] [22] .

I motsats till den vanliga missuppfattningen, innebär inte Gödels ofullständighetsteorem att vissa sanningar aldrig kommer att bli kända för alltid. Dessutom följer det inte av dessa teorem att den mänskliga förmågan till kognition på något sätt är begränsad. Nej, satserna visar bara de formella systemens svagheter och brister [23] .

Betrakta till exempel följande bevis på aritmetikens konsistens [24] .

Låt oss anta att Peanos axiomatik för aritmetik är inkonsekvent. Sedan kan vilket påstående som helst härledas från det, inklusive falskt. Alla Peanos axiom är dock uppenbarligen sanna, och en falsk slutsats kan inte följa av sanna påståenden - vi får en motsägelse. Därför är aritmetiken konsekvent.

Ur den mänskliga vardagslogikens synvinkel är detta bevis acceptabelt och övertygande. Men det kan inte skrivas enligt reglerna i Hilberts bevisteori, eftersom semantiken i dessa regler ersätts av syntax, och sanningen ersätts med "deducerbarhet" [24] . I alla fall höjde Gödels satser matematikfilosofin till en ny nivå.

Se även

Anteckningar

Kommentarer
  1. ↑ Kallas ibland till som Gödels andra sats "om bevis på överensstämmelse" [1] , "om ofullständighet" [2] [3] [4] , "om aritmetikens ofullständighet" [5] .
  2. ↑ 1 2 Ett formellt system som innehåller en obestämbar, det vill säga icke-härledbar och ovedersäglig formel, kallas ofullständig.
  3. ↑ 1 2 3 4 En tolkning av formlerna för en teori S kallas standard om dess domän är mängden icke-negativa heltal, symbolen 0 tolkas av siffran 0, funktionsbokstäverna ', +, • tolkas av om man adderar ett, addition respektive multiplikation, tolkas predikatbokstaven = av identitetsrelationen.
  4. ↑ Gödel använde Whitehead och Russells Principia Mathematica , med förbehållet att resonemanget gäller en bred klass av formella system.
  5. ↑ En sådan jämförelse av formler och naturliga tal kallas aritmetisering av matematik och utfördes för första gången av Gödel. Denna idé blev sedan nyckeln till att lösa många viktiga problem inom matematisk logik. Se Gödel numrering
  6. ↑ "Bew" förkortning. från honom. "Beweisbar" - bevisbar , avläsbar
Källor
  1. ↑ Kleene 1957 s.513
  2. ↑ motsvarande medlem RAS Lev Dmitrievich Beklemishev i "Introduktion till matematisk logik" . Tillträdesdatum: 7 januari 2010. Arkiverad från originalet 21 mars 2009.
  3. ↑ Explanatory Dictionary of Computing Systems - Sida 205
  4. ↑ Rapporter från USSR:s vetenskapsakademi, volym 262 - Sida 799 (1982)
  5. ↑ Proceedings of the Academy of Sciences of the USSR, Volym 50 - Sida 1140 (1986)
  6. ↑ 1 2 Pinheiro, 2015 , sid. 13, 48-49, 66, 89-90.
  7. ↑ 1 2 Kleene 1957 s.187
  8. ↑ Mendelssohn 1971 s.165
  9. ↑ Detta resonemang är hämtat från Mendelssohn 1971 s.160
  10. ↑ Se till exempel Kleene 1957 s.188
  11. ↑ Mendelssohn 1971 s.162
  12. ↑ Mendelssohn 1971 s.162-163
  13. ↑ Mendelssohn 1971 s.176
  14. ↑ Jones JP, Undecidable diophantine equations
  15. ↑ Martin Davis, Diophantine Equations & Computation (länk ej tillgänglig) . Hämtad 17 november 2009. Arkiverad från originalet 24 maj 2010. 
  16. ↑ Martin Davis, The Incompleteness Theorem . Hämtad 30 november 2011. Arkiverad från originalet 4 mars 2016.
  17. ↑ K. Podnieks, Gödels sats i diofantisk form . Hämtad 17 november 2009. Arkiverad från originalet 10 september 2017.
  18. ↑ Godel, Kurt. Om formellt oavgjorda satser av Principia Mathematica och relaterade system. I. - 1931. i Davis, Martin (red.). Det oavgörbara: Grundläggande dokument om oavgjorda propositioner, olösliga problem och beräkningsbara funktioner . - New York: Raven Press, 1965. - S.  6 -8.
  19. ↑ 1 2 Gödel 1931
  20. ↑ Stephen Hawking . Godel and the End of the Universe (inte tillgänglig länk) . Hämtad 8 april 2018. Arkiverad från originalet 29 maj 2020. 
  21. ↑ Mikhailova N.V. Problemet med att underbygga modern matematik i samband med nya filosofiska och metodologiska kriser // Mathematics Philosophy: Actual Problems. Matematik och verklighet. Sammandrag från den tredje allryska vetenskapliga konferensen; 27-28 september 2013 . - M . : Centrum för strategisk konjunktur, 2013. - S. 187. - 270 s. - ISBN 978-5-906233-39-4 . Arkiverad 16 december 2017 på Wayback Machine
  22. ↑ Musiker A. .
  23. ↑ Livio, Mario. Var Gud en matematiker? Kapitel "Sanning i ofullständighet". - M. : AST, 2016. - 384 sid. — (Vetenskapens gyllene fond). - ISBN 978-5-17-095136-9 .
  24. ↑ 1 2 Pinheiro, 2015 , sid. 155-162.

Litteratur

Länkar

Bibliografi - artiklar av Gödel

  • 1931, Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I. Monatshefte für Mathematik und Physik 38 : 173-198.
  • 1931, Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I. och On formally undecidable propositions of Principia Mathematica and related systems I in Solomon Feferman , ed., 1986. Kurt Gödel Collected works, Vol. jag. _ Oxford University Press: 144-195. - Tysk originaltext med parallell engelsk översättning, med en rudimentär introduktion skriven av Stephen Kleene .
  • Hirzel, Martin, 2000, Om formellt obeslutbara propositioner av Principia Mathematica och relaterade system I. . - Modern översättning av Marina Herzel.
  • 1951, Några grundläggande teorem om matematikens grunder och deras implikationer i Solomon Feferman , ed., 1995. Kurt Gödel Samlade verk, Vol. III . Oxford University Press: 304-323.