Twierdzenia Gödla – wspólna nazwa dwóch rezultatów logiki matematycznej i metamatematyki:

• twierdzenie o niezupełności arytmetyki^[1],
• jego konsekwencja nazywana też twierdzeniem o niedowodliwości niesprzeczności.

Oba twierdzenia zostały udowodnione w 1931 roku przez austriackiego matematyka i logika Kurta Gödla^{[potrzebny przypis]}. Uważa się również, że twierdzenia te dają negatywną odpowiedź na drugi problem Hilberta, i w ten sposób mają spore znaczenie w filozofii matematyki. Oprócz rozpatrywanych w tym artykule twierdzeń, Gödel udowodnił też twierdzenie o istnieniu modelu i twierdzenie o nierozstrzygalności (patrz: teoria, struktura matematyczna).

Twierdzenie Gödla było odpowiedzią na próbę przedstawienia wszystkich aksjomatów i twierdzeń matematycznych w postaci czysto symbolicznej (syntaktycznej), tzn. bez odwoływania się do ich znaczenia (czyli w oderwaniu od semantyki; por. logicyzm, formalizm). Próby takiej podjął się m.in. David Hilbert.

Język – zbiór termów (zdań) tworzonych według pewnych reguł.

Teoria matematyczna nad pewnym językiem – przyporządkowanie zdaniom w określonym języku własności prawdy lub fałszu. Teoria nadaje językowi znaczenie i opisuje pewną matematyczną rzeczywistość. Teoria pozwala odpowiedzieć, czy dane zdanie jest prawdziwe.

System formalny – zbiór aksjomatów (zdań) wraz z regułami wnioskowania (algorytmem), generujący pewien podzbiór zdań języka. System formalny jest „przybliżeniem” teorii matematycznej. Pozwala odpowiedzieć, czy dane zdanie jest dowodliwe. Dla jednej teorii może istnieć wiele różnych systemów formalnych (aksjomatyzacji), przybliżających ją lepiej lub gorzej. Jeżeli zdanie jest dowodliwe, to musi być ono prawdziwe (ale niekoniecznie na odwrót).

System formalny niesprzeczny – system, w którym nie da się udowodnić jednocześnie pewnego zdania i jego zaprzeczenia.

System formalny zupełny – system, w którym możliwe jest przeprowadzenie dowodu dowolnego prawidłowo zapisanego zdania tego systemu lub jego zaprzeczenia. W systemie zupełnym każde prawdziwe zdanie jest dowodliwe.

System formalny pierwszego rzędu – system, w którym użyto wyłącznie standardowych reguł wnioskowania oraz wszystkie jego aksjomaty są wyrażone w logice pierwszego rzędu, czyli nie dopuszcza się kwantyfikatorów po zmiennych przebiegających zbiory.

System formalny rozstrzygalny (efektywny) – taki system, którego algorytm wnioskowania da się zaprogramować na maszynie Turinga. Żeby system był rozstrzygalny, potrzeba i wystarcza, żeby istniała tylko jedna (ale odpowiednia) reguła wnioskowania (najczęściej przyjmuje się modus ponens) oraz żeby jego zbiór aksjomatów dał się wygenerować za pomocą maszyny Turinga.

Aksjomatyka Peana – pewien system formalny pierwszego rzędu, opisujący liczby naturalne.

Każdy niesprzeczny system formalny pierwszego rzędu, zawierający w sobie aksjomaty Peana, musi być niezupełny. Oznacza to, że żaden system formalny pierwszego rzędu nigdy nie „pokryje” w całości zbioru wszystkich twierdzeń arytmetyki. Nie oznacza to, że zbiór wszystkich twierdzeń arytmetyki nie istnieje, a jedynie, że nie może on być wygenerowany przez żaden system formalny. Inaczej mówiąc, dowodliwość jest zawsze słabsza od prawdziwości – zbiór zdań generowanych (dowodzonych) przez system formalny nigdy nie będzie równy ze zbiorem zdań prawdziwych teorii. Może on być albo mniejszy od zbioru zdań prawdziwych (system niesprzeczny, ale niezupełny), albo większy od niego (system zupełny, ale sprzeczny)^[2].

Twierdzenie Gödla zachodzi także dla każdej teorii silniejszej od arytmetyki Peana (zawierającej w sobie tę arytmetykę). Oryginalne twierdzenie nic nie mówi o teoriach słabszych od arytmetyki, ale odkryto już słabsze teorie, które wystarczają do zachodzenia podobnych twierdzeń.

Można rozszerzyć definicję systemów formalnych tak, że twierdzenie Gödla nie będzie dla nich zachodzić. Jednak takie niestandardowe systemy nigdy nie będą rozstrzygalne, tzn. ich algorytm wnioskowania nie dałby się zaprogramować na maszynie Turinga lub ich zbiór aksjomatów nie dałby się taką maszyną wygenerować. Ponieważ każdy zbiór skończony jest rozstrzygalny, dlatego twierdzenie Gödla mówi, że nie istnieje żadna zupełna niesprzeczna, skończona aksjomatyzacja arytmetyki, ani nawet taka nieskończona, która da się wygenerować ze skończonej.

To twierdzenie jest konsekwencją poprzedniego. Głosi ono, że w ramach żadnego niesprzecznego systemu formalnego pierwszego rzędu zawierającego w sobie aksjomaty Peana nie da się środkami tego systemu dowieść jego niesprzeczności. Aby taki dowód przeprowadzić, niezbędny jest szerszy system, którego niesprzeczności w ramach niego samego również nie da się dowieść – i tak ad infinitum.

Gödel przyporządkował jednoznacznie każdemu predykatowi arytmetyki pewną liczbę. Ważną częścią dowodu twierdzenia jest sam fakt, że takie przyporządkowanie istnieje.

Każdej funkcji zdaniowej arytmetyki odpowiada więc pewna unikalna liczba. Oznaczmy to przyporządkowanie przez

Istnieją także specjalne funkcje liczbowe, które pozwalają obliczać wartość dla formuł złożonych. Przykładowo:

Istnieje w końcu specjalny operator który dla każdego zdania pozwala odpowiedzieć, czy zdanie to jest dowodliwe. Wyrażenie to samo w sobie jest zdaniem.

– wtedy i tylko wtedy, kiedy istnieje dowód zdania

Każda formuła ma wobec tego jakiś numer. Można odwrócić przyporządkowanie i mówić o formule o numerze Przyporządkowanie nie musiało być surjekcją, dlatego nie wszystkie wartości są sensowne, ale nie bierzemy ich pod uwagę.

W dalszym ciągu będą nas interesować wyłącznie predykaty jednoargumentowe. Oznaczmy listę wszystkich takich predykatów jako

Rozważmy teraz wyrażenie „zdanie o numerze n zastosowane na argumencie n nie posiada dowodu”:

Powstał pewien jednoargumentowy predykat. Każdy taki predykat ma swój numer w przyporządkowaniu Oznaczmy ten numer przez

czyli

Rozważmy teraz właśnie ten predykat zastosowany na liczbie d: Z definicji powyżej mamy:

czyli

Zdanie jest zwane zdaniem Gödla i jest równoważne stwierdzeniu, że ono samo nie posiada dowodu. Czy zdanie to jest prawdziwe, czy fałszywe? Jeżeli jest prawdziwe, to prawdą jest także, że nie posiada ono dowodu, co oznacza, że nasz system formalny jest niezupełny. Jeżeli jest fałszywe, to istnieje jego dowód, co oznacza, że system formalny jest sprzeczny.

Zatem systemy formalne spełniające pewne założenia zawsze muszą być albo zupełne albo niesprzeczne i nigdy nie posiadają obu tych własności jednocześnie.

Obydwa twierdzenia Gödla można uogólnić na dowolne systemy formalne zawierające skończoną lub rekurencyjnie przeliczalną liczbę aksjomatów. Warunkiem jest, aby w skład takiego systemu wchodziła arytmetyka liczb naturalnych lub zawierał on skończoną liczbę aksjomatów umożliwiającą przeprowadzenie tzw. arytmetyzacji twierdzeń.

Można oznaczyć G₀=P_k(k) i dodać to zdanie do aksjomatów systemu. Wtedy również będzie istniało zdanie G₁ niezależne od poszerzonych aksjomatów. W ten sposób można dodać G₂, G₃..., a nawet G_ω, G_ω+1, G_ω+2..., G_ω2, G_ω2+1..., G_ω3, G_ω4... i G_ω²^[3].

• Twierdzenie Gödla nie zachodzi dla słabych teorii, gdzie niemożliwe jest zdefiniowanie przekształcenia z predykatów w liczby (arytmetyzacja twierdzeń). Dla takich teorii możliwe jest skonstruowanie systemu formalnego zupełnego i niesprzecznego. Przykłady to klasyczny rachunek zdań i geometria euklidesowa.

• Twierdzenie Gödla nie zachodzi dla różnych niestandardowych systemów formalnych. Stwierdzenie „istnieje dowód zdania teorii X” nie daje się wtedy zakodować jako zdanie tej teorii (wykracza poza nią).

• Twierdzenia Gödla stosują się tylko do efektywnie generowanych (czyli rekurencyjnie przeliczalnych) teorii. Jeśli wszystkie prawdziwe stwierdzenia o liczbach naturalnych wziąć jako aksjomaty pewnej teorii, to ta teoria jest niesprzecznym i zupełnym rozszerzeniem arytmetyki Peana (nazywaną true arithmetic – „prawdziwą arytmetyką”), dla którego żadne z twierdzeń Gödla nie stosuje się w znaczący sposób, ponieważ ta teoria nie jest rekurencyjnie przeliczalna.

Potoczne rozumienie twierdzeń Gödla prowadzi zwykle do nieprawidłowych wniosków, np.:

• istnieją w matematyce twierdzenia nierozstrzygalne (częsta nadinterpretacja GI),
• nie można udowodnić spójności arytmetyki (częsta nadinterpretacja GII).

Pierwsze twierdzenie Gödla orzeka, że zawsze istnieją prawdziwe twierdzenia arytmetyczne, których nie da się udowodnić posługując się wyłącznie środkami formalnymi danego niesprzecznego systemu F. Z tego nie wynika, że istnieją w arytmetyce prawdziwe twierdzenia, których nie da się udowodnić^[4][5], a jedynie, że nie można sformalizować wszystkich metod dowodowych w ramach pojedynczego systemu formalnego pierwszego rzędu. Udowodnienie, że dane twierdzenie arytmetyczne G(F) jest w systemie F nierozstrzygalne (i co równoważne prawdziwe) odbywa się już przy użyciu środków dowodowych wykraczających poza system formalny F.

Podobnie, drugie twierdzenie Gödla mówi, że jeśli system formalny F jest niesprzeczny, nie może wyprowadzić pewnego twierdzenia arytmetycznego, którego matematyczna prawdziwość jest równoważna faktowi jego niesprzeczności. Z tego nie wynika, że nie można udowodnić spójności systemu formalnego F, np. posługując się niearytmetycznymi środkami dowodowymi. Dowód spójności arytmetyki Peana został podany w 1936 roku przez Gentzena, co nie jest sprzeczne z drugim twierdzeniem Gödla, ponieważ rozumowanie stosowane przez Gentzena nie opiera się na interpretowaniu niesprzeczności w kategoriach prawdziwości twierdzeń skończonej teorii liczb^[6].

Istnieją również alternatywne formy twierdzeń Gödla posługujące się pojęciami m.in. z zakresu tak zwanych zbiorów rekurencyjnych. Można pokazać, że twierdzenie Gödla jest równoważne twierdzeniu Turinga o problemie stopu.

• argument Lucasa-Penrose’a
• dowód Turinga
• problem stopu

• Michał Heller: Wszechświat u schyłku stulecia. Kraków: Znak, 1994. ISBN 83-7006-348-9.
• Torkel Franzén: Gödel’s Theorem: An Incomplete Guide to Its Use and Abuse. A.K. Peters Ltd, 2005. ISBN 1-56881-238-8.
• Andrzej Mostowski: Sentences Undecidable in Formalized Arithmetic: An Exposition of the Theory of Kurt Gödel. Praeger, 1952. ISBN 978-0313231513.
• Ernest Nagel, James R. Newman: Gödel’s Proof. London: Routledge and Kegan Paul, 1958. ISBN 0-415-35528-1.

• Andrzej Mostowski: Logika matematyczna. Warszawa-Wrocław: Monografie Matematyczne, 1948. Brak numerów stron w książce
• Stanisław Krajewski: Twierdzenie Gödla i jego interpretacje filozoficzne. Warszawa: Wydawnictwo Instytutu Filozofii i Socjologii PAN, 2003. ISBN 83-7388-017-8. Brak numerów stron w książce

Polskojęzyczne

• Katja Sagerschnig, Twierdzenie Gödla (niem., polskie napisy), kanał Centrum Nauki Kopernik w Warszawie na YouTube, 14 grudnia 2018 [dostęp 2021-09-16].

Anglojęzyczne

• Eric W.E.W. Weisstein Eric W.E.W., Gödel’s First Incompleteness Theorem, [w:] MathWorld, Wolfram Research  (ang.). [dostęp 2023-06-18].
• Eric W.E.W. Weisstein Eric W.E.W., Gödel’s Second Incompleteness Theorem, [w:] MathWorld, Wolfram Research  (ang.). [dostęp 2023-06-18].
• Gödel incompleteness theorem (ang.), Encyclopedia of Mathematics, encyclopediaofmath.org, [dostęp 2023-06-18].
• PanuP. Raatikainen PanuP., Gödel’s Incompleteness Theorems, [w:] Stanford Encyclopedia of Philosophy, CSLI, Stanford University, 20 stycznia 2015, ISSN 1095-5054 [dostęp 2017-12-31]  (ang.). (Twierdzenia Gödla o niezupełności)
• JasonJ. Megill JasonJ., The Lucas-Penrose Argument about Gödel’s Theorem, Internet Encyclopedia of Philosophy, ISSN 2161-0002 [dostęp 2018-06-27]  (ang.).
• Gödel’s theorems (ang.), Routledge Encyclopedia of Philosophy, rep.routledge.com [dostęp 2023-05-10].
• Note on some misinterpretations of Gödel’s incompleteness theorems