Twierdzenie Gödla o niezupełności: dlaczego matematyka formalna ma ograniczenia
W 1931 roku Kurt Gödel udowodnił fundamentalne ograniczenia każdej wystarczająco silnej formalnej teorii arytmetyki. Jego twierdzenia o niezupełności wykazały, że niemożliwe jest stworzenie spójnego systemu zdolnego do udowodnienia wszystkich prawdziwych stwierdzeń dotyczących liczb naturalnych. To odkrycie rozbiło marzenie o pełnej formalizacji całej matematyki.
Trend jednoczenia się w nauce i matematyce
Na przełomie XIX i XX wieku nauka wykazywała wyraźną tendencję do unifikacji. Newton połączył grawitację ziemską z mechaniką niebieską. Maxwell zredukował elektryczność, magnetyzm i światło do jednego pola elektromagnetycznego. Darwin wyjaśnił różnorodność życia za pomocą doboru naturalnego.
Matematycy dążyli do podobnego syntezu: wyprowadzić arytmetykę, geometrię i analizę z jednego, spójnego zbioru aksjomatów. Gottlob Frege zaproponował konstrukcję liczb poprzez teorię mnogości:
- 0 = ∅ (zbiór pusty)
- 1 = {∅}
- 2 = {∅, {∅}}
Następnik liczby n definiowano jako sumę wszystkich poprzednich liczb. Dzięki temu udało się sformalizować arytmetykę. Jednak paradoks Russella rozpadł tę strukturę: z przyjętych aksjomatów wynikało sprzeczne stwierdzenie „zbiór wszystkich zbiorów, które nie zawierają siebie”.
Fundamentalny kryzys i program Hilberta
Paradoks Russella wywołał kryzys podstaw matematyki. David Hilbert zaproponował program formalizacji, oparty na trzech kluczowych wymogach:
- Pełność (K): system musi udowadniać wszystkie prawdziwe stwierdzenia arytmetyki.
- Spójność (K): system nie może udowadniać fałszywych stwierdzeń.
- Rozstrzygalność: musi istnieć algorytm pozwalający sprawdzić, czy dane stwierdzenie jest dowodliwe.
Hilbert żądał metamatematycznego dowodu tych własności dla skończonego zestawu aksjomatów.
„Principia Mathematica” Russella i Whiteheada
Bertrand Russell i Alfred North Whitehead stworzyli „Principia Mathematica” (PM) — aksjomatyczny system logiki wystarczająco potężny, by ująć całą matematykę. Zbudowali arytmetykę od podstaw i dopiero na stronie 379 udowodnili, że 1 + 1 = 2.
Do swojej analizy Gödel uprościł składnię PM do języka przypominającego PM-Lisp:
| Symbol | Znaczenie | Przykład |
|--------|-----------|----------|
| 0 | zero | 0 |
| next | następnik | (next 0) |
| + | dodawanie | (+ 0 (next 0)) |
| | mnożenie | ( 0 (next 0)) |
| = | równość | (= 0 (* 0 (next 0))) |
Operatory logiczne:
| Symbol | Znaczenie | Przykład |
|--------|-----------|----------|
| not | negacja | (not (= 0 1)) |
| or | alternatywa | (or (= 0 1) (not (= 0 1))) |
| when | implikacja | (when 0 (or 0 1)) |
| there-is | kwantyfikator egzystencjalny | (there-is x (= 4 (* x 2))) |
Aksjomaty PM obejmowały tautologie:
(when (or p p) p)(when p (or p q))- Przemienność i łączność alternatywy
- Regułę sylogizmu
Z nich wynikały prawa równości i podstawy arytmetyki.
Numeracja Gödla: kodowanie składni
Gödel zastosował kodowanie typu Cantora, aby przedstawić formuły jako liczby naturalne. Każdemu symbolowi przypisał unikalny numer pierwszy (tzw. liczba Gödla):
| Symbol | Liczba Gödla |
|--------|--------------|
| ( | 1 |
| ) | 3 |
| 0 | 5 |
| next | 7 |
| + | 9 |
| * | 11 |
| = | 13 |
| not | 15 |
| or | 17 |
| when | 19 |
| there-is | 21 |
| a,b,c... | 2,4,6... |
Formuła (there-is a (= (next 0) a)) jest kodowana jako sekwencja tokenów, a następnie jej liczba Gödla to G = 2^{g₁} × 3^{g₂} × 5^{g₃} × …, gdzie gᵢ to numery kolejnych tokenów. To odwzorowanie jest bijekcją między formułami a liczbami naturalnymi.
Arytmetyka w stylu PM-Lisp jest wyrażalna w sobie samej: długość formuły, podstawienie, dowodliwość — wszystko redukuje się do funkcji pierwotnie rekurencyjnych.
Samoodnoszenie się i twierdzenie o niezupełności
Gödel skonstruował formułę G, która stwierdza własną niedowodliwość: ∃p Proof(p, ⌜G⌝) — „nie istnieje dowód o numerze p dla mnie”.
Z lematu diagonalnego (punktu stałego) wynika:
G ≡ ¬Provable(⌜G⌝)
Twierdzenie 1: Jeśli PM jest spójna, to G jest prawdziwa, ale niedowodliwa w PM.
Twierdzenie 2: Jeśli PM jest spójna, to Con(PM) (spójność PM) jest niedowodliwa w PM.
Co najważniejsze:
- Każdy system interpretujący arytmetykę Peana jest niezupełny.
- Spójność systemu nie może zostać udowodniona w jego własnym wnętrzu.
- Liczby kodują składnię, umożliwiając samoodnoszenie się.
- Program Hilberta jest niewykonalny.
- Prawdziwość ≠ dowodliwość.
Konsekwencje dla informatyki
Twierdzenie Gödla jest równoważne problemowi stopu Turinga. Formalne systemy mają swoje „ślepe plamy”. W programowaniu oznacza to:
- Istnienie funkcji nierozstrzygalnych (np. „orakul stopu”).
- Ryzyko „bomb logicznych” w systemach weryfikacyjnych.
- Ograniczenia formalnej weryfikacji oprogramowania.
Współczesne narzędzia (np. Coq, Lean) świadomie uwzględniają niezupełność, wprowadzając zaufane aksjomaty.
— Editorial Team
Brak komentarzy.