Drugi problem Hilberta

W matematyce drugi problem Hilberta został postawiony przez Davida Hilberta w 1900 roku jako jeden z jego 23 problemów . Prosi o dowód, że arytmetyka jest spójna – wolna od jakichkolwiek wewnętrznych sprzeczności. Hilbert stwierdził, że aksjomaty, które rozważał dla arytmetyki, to te podane w Hilbert (1900) , które obejmują aksjomat kompletności drugiego rzędu.

W latach trzydziestych XX wieku Kurt Gödel i Gerhard Gentzen udowodnili wyniki, które rzucają nowe światło na problem. Niektórzy uważają, że twierdzenia Gödla dają negatywne rozwiązanie problemu, podczas gdy inni uważają dowód Gentzena za częściowe rozwiązanie pozytywne.

Problem Hilberta i jego interpretacja

W jednym tłumaczeniu na język angielski Hilbert pyta:

„Kiedy zajmujemy się badaniem podstaw nauki, musimy ustanowić system aksjomatów, który zawiera dokładny i pełny opis relacji zachodzących między elementarnymi ideami tej nauki. ... Ale przede wszystkim chcę wyznaczyć spośród licznych pytań, które można postawić w odniesieniu do aksjomatów, najważniejsze jest następujące: udowodnić, że nie są one sprzeczne, to znaczy, że określona liczba kroków logicznych opartych na nich nie może nigdy prowadzić do sprzecznych wyników. , dowód zgodności aksjomatów można przeprowadzić konstruując odpowiednie pole liczb, tak aby analogiczne relacje między liczbami tego ciała odpowiadały aksjomatom geometrycznym. ... Z drugiej strony potrzebna jest metoda bezpośrednia dla dowód zgodności aksjomatów arytmetycznych”.

Stwierdzenie Hilberta jest czasami źle rozumiane, ponieważ przez „aksjomaty arytmetyczne” miał na myśli nie system równoważny arytmetyce Peano, ale mocniejszy system z aksjomatem zupełności drugiego rzędu. System, którego dowód kompletności zażądał Hilbert, bardziej przypomina arytmetykę drugiego rzędu niż arytmetykę Peano pierwszego rzędu.

Jako powszechna obecnie interpretacja, pozytywne rozwiązanie drugiego pytania Hilberta dostarczyłoby w szczególności dowodu, że arytmetyka Peano jest spójna.

Istnieje wiele znanych dowodów na to, że arytmetyka Peano jest spójna, które można przeprowadzić w silnych systemach, takich jak teoria mnogości Zermelo – Fraenkla . Nie dają one jednak rozwiązania drugiego pytania Hilberta, ponieważ jest mało prawdopodobne, aby ktoś, kto wątpi w spójność arytmetyki Peano, zaakceptował aksjomaty teorii mnogości (która jest znacznie silniejsza), aby udowodnić jej spójność. Tak więc satysfakcjonujące rozwiązanie problemu Hilberta musi zostać przeprowadzone przy użyciu zasad, które byłyby do przyjęcia dla kogoś, kto nie wierzy już, że PA jest spójne. Takie zasady są często nazywane finitystycznymi ponieważ są one całkowicie konstruktywne i nie zakładają skończonej nieskończoności liczb naturalnych. Drugie twierdzenie Gödla o niezupełności (patrz twierdzenia Gödla o niezupełności ) nakłada surowe ograniczenie na to, jak słaby może być system finitystyczny, jednocześnie udowadniając spójność arytmetyki Peano.

Twierdzenie Gödla o niezupełności

Drugie twierdzenie Gödla o niezupełności pokazuje, że nie jest możliwe, aby jakikolwiek dowód na to, że arytmetyka Peano była spójna, mógł zostać przeprowadzony w ramach samej arytmetyki Peano. To twierdzenie pokazuje, że jeśli jedynymi akceptowalnymi procedurami dowodowymi są te, które można sformalizować w ramach arytmetyki, to nie można odpowiedzieć na wezwanie Hilberta do dowodu spójności. Jednak, jak wyjaśniają Nagel i Newman (1958: 96–99), wciąż jest miejsce na dowód, którego nie można sformalizować w arytmetyce:

„Tego imponującego wyniku analizy Godla nie należy źle rozumieć: nie wyklucza on metamatematycznego dowodu spójności arytmetyki. Wyklucza dowód spójności, który można odzwierciedlić w formalnych dedukcjach arytmetycznych. Dowody meta-matematyczne konsystencji arytmetyki zostały w rzeczywistości skonstruowane, zwłaszcza przez Gerharda Gentzena , członek szkoły Hilberta, w 1936 roku i od tego czasu przez innych. ... Ale tych metamatematycznych dowodów nie można przedstawić w rachunku arytmetycznym; a ponieważ nie są finitystyczne, nie osiągają ogłoszonych celów pierwotnego programu Hilberta. ... Wyniki Gödla nie wykluczają możliwości skonstruowania finitystycznego absolutnego dowodu zgodności dla arytmetyki. Gödel wykazał, że żaden taki dowód nie jest możliwy, który można przedstawić w ramach arytmetyki. Jego argumentacja nie eliminuje możliwości ściśle skończonych dowodów, których nie można przedstawić w arytmetyce. Wydaje się jednak, że nikt dzisiaj nie ma jasnego pojęcia, jak wyglądałby dowód finitystyczny, którego nie da się sformułować w ramach arytmetyki”.

Dowód konsystencji Gentzena

W 1936 roku Gentzen opublikował dowód na to, że arytmetyka Peano jest spójna. Wynik Gentzena pokazuje, że dowód spójności można uzyskać w systemie, który jest znacznie słabszy niż teoria mnogości.

Dowód Gentzena przebiega poprzez przypisanie każdemu dowodowi w arytmetyce Peano liczby porządkowej , na podstawie struktury dowodu, przy czym każda z tych liczb porządkowych jest mniejsza niż ε 0 . Następnie udowadnia za pomocą indukcji pozaskończonej na tych liczbach porządkowych, że żaden dowód nie może zakończyć się sprzecznością. Metodę zastosowaną w tym dowodzie można również wykorzystać do udowodnienia eliminacji cięcia dla arytmetyki Peano w logice silniejszej niż logika pierwszego rzędu, ale sam dowód spójności można przeprowadzić w zwykłej logice pierwszego rzędu przy użyciu aksjomatów prymitywna arytmetyka rekurencyjna i zasada indukcji pozaskończonej. Tait (2005) przedstawia teoretyczną interpretację metody Gentzena.

Dowód spójności Gentzena zapoczątkował program analizy porządkowej w teorii dowodu. W tym programie formalnym teoriom arytmetyki lub teorii mnogości przypisuje się liczby porządkowe , które mierzą siłę spójności teorii. Teoria nie będzie w stanie udowodnić spójności innej teorii z wyższą teorią porządkową dowodu.

Współczesne poglądy na stan problemu

Chociaż twierdzenia Gödla i Gentzena są obecnie dobrze rozumiane przez społeczność logiki matematycznej, nie osiągnięto konsensusu co do tego, czy (lub w jaki sposób) te twierdzenia odpowiadają na drugi problem Hilberta. Simpson (1988: rozdz. 3) argumentuje, że twierdzenie Gödla o niezupełności pokazuje, że nie jest możliwe przedstawienie finitystycznych dowodów spójności silnych teorii. Kreisel (1976) stwierdza, że ​​chociaż wyniki Gödla sugerują, że nie można uzyskać żadnego finitystycznego dowodu spójności składniowej, semantyczny (w szczególności drugiego rzędu ) można użyć argumentów, aby przedstawić przekonujące dowody spójności. Detlefsen (1990: s. 65) argumentuje, że twierdzenie Gödla nie uniemożliwia dowodu spójności, ponieważ jego hipotezy mogą nie mieć zastosowania do wszystkich systemów, w których można przeprowadzić dowód spójności. Dawson (2006: sek. 2) nazywa przekonanie, że twierdzenie Gödla eliminuje możliwość przekonującego dowodu spójności „błędnym”, powołując się na dowód spójności podany przez Gentzena i późniejszy dowód podany przez Gödla w 1958 roku.

Zobacz też

Notatki

Linki zewnętrzne