Loading AI tools
dwa twierdzenia limitacyjne w logice Z Wikipedii, wolnej encyklopedii
Twierdzenia Gödla – wspólna nazwa dwóch rezultatów logiki matematycznej i metamatematyki:
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.
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ć G0=Pk(k) i dodać to zdanie do aksjomatów systemu. Wtedy również będzie istniało zdanie G1 niezależne od poszerzonych aksjomatów. W ten sposób można dodać G2, G3..., a nawet Gω, Gω+1, Gω+2..., Gω2, Gω2+1..., Gω3, Gω4... i Gω²[3].
Potoczne rozumienie twierdzeń Gödla prowadzi zwykle do nieprawidłowych wniosków, np.:
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.
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.