Teoria dowodu - Proof theory

Teoria dowodu jest główną gałęzią logiki matematycznej, która przedstawia dowody jako formalne obiekty matematyczne , ułatwiając ich analizę za pomocą technik matematycznych. Dowody są zazwyczaj przedstawiane jako struktury danych zdefiniowane indukcyjnie , takie jak listy zwykłe, listy w ramkach lub drzewa , które są konstruowane zgodnie z aksjomatami i regułami wnioskowania systemu logicznego. Jako taka, teoria dowodu ma charakter syntaktyczny , w przeciwieństwie do teorii modeli , która ma charakter semantyczny .

Niektóre z głównych obszarów teorii dowodu obejmują: strukturalną teorię dowodu , analizę porządkową , logikę dowodliwości , matematykę odwrotną , eksplorację dowodów , automatyczne dowodzenie twierdzeń i złożoność dowodu . Wiele badań koncentruje się również na zastosowaniach w informatyce, językoznawstwie i filozofii.

Historia

Chociaż formalizacja logiki została znacznie zaawansowana dzięki pracom takich postaci jak Gottlob Frege , Giuseppe Peano , Bertrand Russell i Richard Dedekind , historia współczesnej teorii dowodu jest często postrzegana jako ustanowiona przez Davida Hilberta , który zainicjował tzw . program w Podstawach Matematyki . Główną ideą tego programu było to, że gdybyśmy mogli przedstawić skończone dowody spójności dla wszystkich wyrafinowanych formalnych teorii potrzebnych matematykom, to moglibyśmy ugruntować te teorie za pomocą argumentu metamatematycznego, który pokazuje, że wszystkie ich czysto uniwersalne twierdzenia (więcej technicznie ich zdania dowodzące ) są skończenie prawdziwe; skoro tak ugruntowani, nie dbamy o niefinitarny sens ich twierdzeń egzystencjalnych, uznając je za pseudoznaczące twierdzenia o istnieniu bytów idealnych. ${\ Displaystyle \ Pi _ {1} ^ {0}}$

Niepowodzenie programu zostało wywołane twierdzeniami Kurta Gödla o niezupełności , które pokazały, że każda teoria ω-spójna, która jest wystarczająco silna, aby wyrazić pewne proste prawdy arytmetyczne, nie może udowodnić własnej niesprzeczności, która według sformułowania Gödla jest zdaniem. Pojawiły się jednak zmodyfikowane wersje programu Hilberta i przeprowadzono badania nad pokrewnymi tematami. Doprowadziło to w szczególności do: ${\ Displaystyle \ Pi _ {1} ^ {0}}$

• Udoskonalenie wyniku Gödla, w szczególności udoskonalenie J. Barkley Rossera , osłabiające powyższe wymaganie -konsystencji do prostej konsystencji;
• Aksjomatyzacja rdzenia wyniku Gödla w terminach języka modalnego, logika dowodliwości ;
• Nieskończona iteracja teorii za sprawą Alana Turinga i Solomona Fefermana ;
• Odkrycie samoweryfikujących się teorii , systemów wystarczająco silnych, by mówić o sobie, ale zbyt słabych, by przeprowadzić argumentację diagonalną, która jest kluczem do argumentu o niedowodliwości Gödla.

Równolegle z powstaniem i upadkiem programu Hilberta powstawały podstawy strukturalnej teorii dowodu . Jan Łukasiewicz zasugerował w 1926 r., że można ulepszyć systemy Hilberta jako podstawę aksjomatycznej prezentacji logiki, jeśli pozwoli się wyciągnąć wnioski z założeń zawartych w regułach wnioskowania logiki. W odpowiedzi na to Stanisław Jaśkowski (1929) i Gerhard Gentzen (1934) niezależnie dostarczyli takich systemów, zwanych rachunkami dedukcji naturalnej , w podejściu Gentzena wprowadzającym ideę symetrii między podstawami twierdzenia wyrażonymi w regułach wstępnych a konsekwencjami akceptowania zdań w regułach eliminacyjnych , pomysł, który okazał się bardzo ważny w teorii dowodu. Gentzen (1934) przedstawił dalej ideę rachunku sekwencyjnego , rachunku opracowanego w podobnym duchu, który lepiej wyrażał dwoistość spójników logicznych, a następnie dokonał fundamentalnych postępów w formalizacji logiki intuicjonistycznej i przedstawił pierwszy dowód kombinatoryczny spójności arytmetyki Peano . Przedstawienie dedukcji naturalnej i rachunku sekwencyjnego razem wprowadziły fundamentalną ideę dowodu analitycznego do teorii dowodu.

Strukturalna teoria dowodu

Strukturalna teoria dowodu jest subdyscypliną teorii dowodu, która bada specyfikę rachunków dowodowych . Trzy najbardziej znane style rachunku dowodowego to:

• Hilbert kamicy
• Dedukcja naturalna kamicy
• SEQUENT kamicy

Każda z nich może dać kompletną i aksjomatyczną formalizację logiki zdań lub predykatów o charakterze klasycznym lub intuicjonistycznym , prawie każdą logikę modalną i wiele logik substrukturalnych , takich jak logika istotności lub logika liniowa . Rzeczywiście, niezwykłe jest znalezienie logiki, która opiera się przedstawieniu w jednym z tych rachunków.

Teoretycy dowodu są zazwyczaj zainteresowani rachunkiem dowodu, który wspiera pojęcie dowodu analitycznego . Pojęcie dowodu analitycznego zostało wprowadzone przez Gentzena do rachunku sekwencyjnego; tam dowody analityczne to te, które są wolne od wycinania . Duże zainteresowanie dowodami bez obcinania pochodzi z własności subformula: każda formuła w końcowym ciągu dowodu bez obcinania jest podformułą jednej z przesłanek. Pozwala to łatwo pokazać spójność rachunku sekwencyjnego; gdyby pusta sekwencja była wyprowadzalna, musiałaby być podformułą jakiejś przesłanki, której nie jest. Twierdzenie Gentzena, twierdzenie o interpolacji Craiga i twierdzenie Herbranda, również są następstwem twierdzenia o eliminacji cięcia.

Rachunek dedukcji naturalnej Gentzena również wspiera pojęcie dowodu analitycznego, jak wykazał Dag Prawitz . Definicja jest nieco bardziej złożona: mówimy, że dowody analityczne to formy normalne , które są związane z pojęciem formy normalnej w przepisaniu terminów. Bardziej egzotyczne rachunki dowodowe, takie jak sieci dowodowe Jeana-Yvesa Girarda , również wspierają koncepcję dowodu analitycznego.

Szczególna rodzina dowodów analitycznych powstających w logice redukcyjnej są dowodami skupionymi, które charakteryzują dużą rodzinę ukierunkowanych na cel procedur poszukiwania dowodów. Zdolność do przekształcenia systemu dowodowego w formę skoncentrowaną jest dobrym wskaźnikiem jego jakości syntaktycznej, podobnie jak dopuszczalność cięcia pokazuje, że system dowodowy jest syntaktycznie spójny.

Teoria dowodu strukturalnego jest połączona z teorią typów za pomocą korespondencji Curry-Howarda , w której obserwuje się analogię strukturalną między procesem normalizacji w rachunku dedukcji naturalnej a redukcją beta w typowanym rachunku lambda . Stanowi to podstawę teorii typów intuicjonistycznych opracowanej przez Pera Martina-Löfa i często jest rozszerzona na korespondencję trójstronną, której trzecią odnogą są kategorie zamknięte kartezjańskie .

Inne tematy badawcze w teorii strukturalnej obejmują tabelę analityczną, która stosuje centralną ideę dowodu analitycznego z teorii dowodu strukturalnego w celu zapewnienia procedur decyzyjnych i procedur pół-decyzji dla szerokiego zakresu logik, oraz teorię dowodu logik podstrukturalnych.

Analiza porządkowa

Analiza porządkowa jest potężną techniką dostarczania dowodów spójności kombinatorycznej dla podsystemów arytmetyki, analizy i teorii mnogości. Drugie twierdzenie Gödla o niezupełności jest często interpretowane jako wykazanie, że skończone dowody niesprzeczności są niemożliwe dla teorii o wystarczającej sile. Analiza porządkowa pozwala precyzyjnie zmierzyć nieskończoną zawartość spójności teorii. W przypadku spójnej rekurencyjnie aksjomatyzowanej teorii T można dowieść w arytmetyce skończonej, że zasadność pewnej pozaskończonej liczby porządkowej implikuje zgodność drugiego twierdzenia o niezupełności T. Gödla implikuje, że zasadność takiej liczby porządkowej nie może być udowodniona w teorii T.

Konsekwencje analizy porządkowej obejmują (1) zgodność podsystemów klasycznej arytmetyki drugiego rzędu i teorii mnogości w stosunku do teorii konstruktywnych, (2) wyniki niezależności kombinatorycznej oraz (3) klasyfikacje funkcji rekurencyjnych, które można udowodnić, oraz liczb porządkowych, które można udowodnić.

Analiza porządkowa została zapoczątkowana przez Gentzena, który udowodnił zgodność arytmetyki Peano przy użyciu indukcji pozaskończonej do liczby porządkowej ε ₀ . Analiza porządkowa została rozszerzona na wiele fragmentów arytmetyki pierwszego i drugiego rzędu oraz teorii mnogości. Jednym z głównych wyzwań była porządkowa analiza teorii implikacyjnych. Pierwszym przełomem w tym kierunku był dowód Takeuti na spójność Π¹
₁-CA ₀ przy użyciu metody diagramów porządkowych.

Logika dowodliwości

Logika dowodliwości jest logiką modalną , w której operator pola jest interpretowany jako „jest to możliwe do udowodnienia”. Chodzi o to, aby uchwycić pojęcie predykatu dowodowego dość bogatej teorii formalnej . Jako podstawowe aksjomaty logiki dowodliwości GL ( Gödel - Löb ), która ujmuje dowodzenia w arytmetyce Peano , przyjmuje się modalne analogi warunków wyprowadzalności Hilberta-Bernaysa i twierdzenie Löba (jeśli można dowieść, że dowodliwość A implikuje A, to A jest do udowodnienia).

Niektóre z podstawowych wyników dotyczących niekompletności Arytmetyki Peano i teorii pokrewnych mają analogie w logice dowodliwości. Na przykład w GL jest twierdzenie, że jeśli sprzeczność nie jest dowodliwa, to nie jest udowodnione, że sprzeczności nie można udowodnić (drugie twierdzenie Gödla o niezupełności). Istnieją również modalne analogi twierdzenia o punkcie stałym. Robert Solovay udowodnił, że logika modalna GL jest zupełna w odniesieniu do arytmetyki Peano. Oznacza to, że teoria zdań dowodliwości w arytmetyce Peano jest całkowicie reprezentowana przez logikę modalną GL. To wprost sugeruje, że rozumowanie zdaniowe dotyczące dowodliwości w arytmetyce Peano jest kompletne i rozstrzygalne.

Inne badania nad logiką dowodliwości koncentrowały się na logice dowodliwości pierwszego rzędu, polimodalnej logice dowodliwości (z jedną modalnością reprezentującą dowodliwość w teorii obiektów, a drugą reprezentującą dowodliwość w metateorii) oraz logikach interpretacyjności, których celem jest uchwycenie interakcji między dowodliwością a interpretowalnością . Niektóre najnowsze badania dotyczyły zastosowań stopniowanych algebr dowodzenia w porządkowej analizie teorii arytmetycznych.

Matematyka odwrotna

Matematyka odwrotna to program w logice matematycznej, który ma na celu określenie, które aksjomaty są wymagane do udowodnienia twierdzeń matematycznych. Pole zostało założone przez Harveya Friedmana . Jego metodę definiowania można opisać jako „cofanie się od twierdzeń do aksjomatów ”, w przeciwieństwie do zwykłej matematycznej praktyki wyprowadzania twierdzeń z aksjomatów. Program matematyki odwrotnej został zapowiedziany przez wyniki w teorii mnogości, takie jak klasyczne twierdzenie, że aksjomat wyboru i lemat Zorna są równoważne z teorią mnogości ZF . Celem matematyki odwrotnej jest jednak badanie możliwych aksjomatów zwykłych twierdzeń matematycznych, a nie możliwych aksjomatów teorii mnogości.

W matematyce odwrotnej zaczyna się od języka ramowego i teorii bazowej – podstawowego systemu aksjomatów – który jest zbyt słaby, aby udowodnić większość twierdzeń, którymi możemy być zainteresowani, ale wciąż wystarczająco potężny, aby opracować definicje niezbędne do sformułowania tych twierdzeń. Na przykład, aby zbadać twierdzenie „Każdy ograniczony ciąg liczb rzeczywistych ma supremum ”, konieczne jest użycie systemu bazowego, który może mówić o liczbach rzeczywistych i ciągach liczb rzeczywistych.

Dla każdego twierdzenia, które można sformułować w systemie podstawowym, ale nie można udowodnić w systemie podstawowym, celem jest określenie konkretnego systemu aksjomatów (silniejszego niż system podstawowy), który jest niezbędny do udowodnienia tego twierdzenia. Aby pokazać, że system S jest wymagany do udowodnienia twierdzenia T , wymagane są dwa dowody. Pierwszy dowód pokazuje, że T jest dowodliwe z S ; jest to zwykły dowód matematyczny wraz z uzasadnieniem, że można go przeprowadzić w systemie S . Drugi dowód, znany jako odwrócenie , pokazuje, że samo T implikuje S ; dowód ten jest przeprowadzany w systemie podstawowym. Odwrócenie ustala, że ​​żaden system aksjomatów S′, który rozszerza system bazowy, nie może być słabszy niż S , wciąż udowadniając  T .

Jednym z uderzających zjawisk w matematyce odwrotnej jest solidność systemów aksjomatów Wielkiej Piątki . W celu zwiększenia wytrzymałości systemy te są nazywane inicjałami RCA ₀ , WKL ₀ , ACA ₀ , ATR ₀ , i Π¹
₁-CA ₀ . Prawie każde twierdzenie zwykłej matematyki, które poddano matematycznej analizie odwrotnej, okazało się równoważne z jednym z tych pięciu systemów. Wiele ostatnich badań koncentrowało się na zasadach kombinatorycznych, które nie pasują idealnie do tych ram, takich jak RT²
₂ (Twierdzenie Ramseya dla par).

Badania w matematyce odwrotnej często obejmują metody i techniki z teorii rekurencji oraz teorii dowodu.

Interpretacje funkcjonalne

Interpretacje funkcjonalne to interpretacje teorii niekonstruktywnych w teoriach funkcjonalnych. Interpretacje funkcjonalne zwykle przebiegają dwuetapowo. Po pierwsze, „redukuje się” klasyczną teorię C do intuicjonistycznej teorii I. To znaczy zapewnia konstruktywne odwzorowanie, które przekłada twierdzenia C na twierdzenia I. Po drugie, redukuje się intuicjonistyczną teorię I do wolnej od kwantyfikatorów teorii funkcjonały F. Interpretacje te składają się na formę programu Hilberta, gdyż dowodzą spójności teorii klasycznych z teoriami konstruktywnymi. Udane interpretacje funkcjonalne zaowocowały redukcją teorii nieskończoności do teorii skończoności i teorii implikacyjnych do predykatywnych.

Interpretacje funkcjonalne zapewniają również sposób na wyodrębnienie konstruktywnych informacji z dowodów w teorii zredukowanej. Bezpośrednią konsekwencją interpretacji jest zwykle taki wynik, że każda funkcja rekurencyjna, której całość można udowodnić albo w I, albo w C, jest reprezentowana przez wyraz F. Jeśli można podać dodatkową interpretację F w I, która czasami jest jest to możliwe, w rzeczywistości ta charakterystyka jest zwykle wykazywana jako dokładna. Często okazuje się, że terminy F pokrywają się z naturalną klasą funkcji, takich jak prymitywne funkcje rekurencyjne lub obliczalne w czasie wielomianowym. Interpretacje funkcjonalne były również wykorzystywane do dostarczania porządkowych analiz teorii i klasyfikowania ich funkcji rekurencyjnych, które można udowodnić.

Badanie interpretacji funkcjonalnych rozpoczęło się od interpretacji arytmetyki intuicjonistycznej Kurta Gödla w wolnej od kwantyfikatorów teorii funkcjonałów typu skończonego. Ta interpretacja jest powszechnie znana jako interpretacja Dialectica . Wraz z podwójnie negującą interpretacją logiki klasycznej w logice intuicjonistycznej zapewnia redukcję arytmetyki klasycznej do arytmetyki intuicjonistycznej.

Dowód formalny i nieformalny

Te nieformalne dowody codziennej praktyce matematycznej są w przeciwieństwie do formalnych dowodów teoria dowodu. Są raczej jak szkice wysokiego poziomu, które pozwalają ekspertowi zrekonstruować formalny dowód przynajmniej co do zasady, mając wystarczająco dużo czasu i cierpliwości. Dla większości matematyków pisanie w pełni formalnego dowodu jest zbyt pedantyczne i rozwlekłe, by mogło być powszechnie używane.

Dowody formalne są konstruowane za pomocą komputerów w interaktywnym dowodzeniu twierdzeń . Co istotne, dowody te mogą być sprawdzane automatycznie, także komputerowo. Sprawdzanie dowodów formalnych jest zwykle proste, podczas gdy znajdowanie dowodów ( automatyczne dowodzenie twierdzeń ) jest generalnie trudne. Z kolei nieformalny dowód w literaturze matematycznej wymaga sprawdzenia przez tygodnie recenzowania i nadal może zawierać błędy.

Semantyka dowodowa

W językoznawstwie , type-logiczna gramatyka , gramatyka kategorialna i Montague gramatyki zastosowanie formalizmach oparte na teorii strukturalnej próbnym, aby dać formalnych semantyki języka naturalnego .

Zobacz też

• Logika pośrednia
• Teoria modeli
• Dowód (prawda)
• Techniki dowodowe
• Rachunek sekwencyjny

Uwagi

Bibliografia

• J. Avigad i EH Reck (2001). „'Wyjaśnianie natury nieskończoności': rozwój metamatematyki i teorii dowodu ”. Raport techniczny Carnegie-Mellona CMU-PHIL-120.
• J. Barwise , wyd. (1978). Podręcznik logiki matematycznej . Północna Holandia.
• S. Buss, wyd. (1998) Podręcznik teorii dowodu . Elsevier.
• AS Troelstra i H. Schwichtenberg (1996). Podstawowa teoria dowodu , Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, ISBN  0-521-77911-1 .
• G. Gentzen (1935/1969). " Badania nad dedukcją logiczną ". W ME Szabo, wyd. Zebrane dokumenty Gerharda Gentzena . Północna Holandia. Przekład Szabo z „Untersuchungen über das logische Schliessen”, Mathematisches Zeitschrift t . 39, s. 176–210, 405 431.
• D. Prawitza (1965). Dedukcja naturalna: badanie teoretyczno-dowodowe , Dover Publications, ISBN  978-0-486-44655-4
• SG Simpson (2010). Podsystemy arytmetyki drugiego rzędu , wydanie drugie. Cambridge University Press, ISBN  978-0521150149 .
• H. Wanga (1981). Popularne wykłady z logiki matematycznej , Van Nostrand Reinhold Company , ISBN  0-442-23109-1 .

Zewnętrzne linki

• „Teoria dowodu” , Encyklopedia Matematyki , EMS Press , 2001 [1994]
• J. von Plato (2008). Rozwój teorii dowodu . Stanford Encyclopedia of Philosophy .