Twierdzenie o zupełności Gödla - Gödel's completeness theorem

Wzór ( ∀ x . R ( x , x )) → (∀ x ∃ y . R ( x , y )) obowiązuje we wszystkich strukturach (po lewej pokazano tylko 8 najprostszych). Zgodnie z wynikiem zupełności Gödla, musi zatem mieć naturalny dowód dedukcji (pokazany po prawej).

Twierdzenie o zupełności Gödla jest podstawowym twierdzeniem w logice matematycznej, które ustala zgodność między prawdą semantyczną a dowodliwością syntaktyczną w logice pierwszego rzędu .

Twierdzenie o zupełności ma zastosowanie do każdej teorii pierwszego rzędu : Jeśli T jest taką teorią, a φ jest zdaniem (w tym samym języku), a każdy model T jest modelem φ, to istnieje (pierwszego rzędu) dowód φ używanie zdań T jako aksjomatów. Czasami mówi się, że „wszystko, co prawdziwe, jest możliwe do udowodnienia”.

Stanowi ścisły związek między teorią modeli, która zajmuje się tym, co jest prawdą w różnych modelach, a teorią dowodu, która bada, co można formalnie udowodnić w poszczególnych systemach formalnych .

Po raz pierwszy udowodnił to w 1929 r. Kurt Gödel . Został uproszczony w 1947 r., kiedy Leon Henkin zaobserwował w swoim doktoracie. tezę, że twardą część dowodu można przedstawić jako twierdzenie o modelu istnienia (opublikowane w 1949 r.). Dowód Henkina został uproszczony przez Gisberta Hasenjaegera w 1953 roku.

Czynności wstępne

Istnieje wiele systemów dedukcyjnych dla logiki pierwszego rzędu, w tym systemy dedukcji naturalnej i systemy w stylu Hilberta . Wspólne dla wszystkich systemów dedukcyjnych jest pojęcie dedukcji formalnej . Jest to ciąg (lub w niektórych przypadkach drzewo skończone ) formuł ze specjalnie wyznaczonym wnioskiem . Definicja dedukcji jest taka, że ​​jest ona skończona i można algorytmicznie (np. komputerowo lub ręcznie) zweryfikować , czy dany ciąg (lub drzewo) formuł jest rzeczywiście dedukcją.

Formuła pierwszego rzędu jest nazywana logicznie poprawną, jeśli jest prawdziwa w każdej strukturze dla języka formuły (tj. dla dowolnego przypisania wartości do zmiennych formuły). Aby formalnie stwierdzić, a następnie udowodnić twierdzenie o zupełności, konieczne jest również zdefiniowanie systemu dedukcyjnego. System dedukcyjny nazywamy zupełnym, jeśli każda logicznie poprawna formuła jest wnioskiem jakiejś formalnej dedukcji, a twierdzenie o zupełności dla konkretnego systemu dedukcyjnego jest twierdzeniem, że jest on w tym sensie zupełny. Tak więc w pewnym sensie istnieje inne twierdzenie o zupełności dla każdego systemu dedukcyjnego. Odwrotnością do kompletności jest poprawność , fakt, że w systemie dedukcyjnym można udowodnić tylko logicznie poprawne formuły.

Jeśli jakiś konkretny system dedukcyjny logiki pierwszego rzędu jest poprawny i kompletny, to jest „doskonały” (wzór jest możliwy do udowodnienia wtedy i tylko wtedy, gdy jest logicznie ważny), a więc równoważny z każdym innym systemem dedukcyjnym o tej samej jakości (każdy dowód w jednym systemie można przekształcić w drugi).

Oświadczenie

Najpierw ustalamy system dedukcyjny rachunku predykatów pierwszego rzędu, wybierając dowolny z dobrze znanych systemów równoważnych. Oryginalny dowód Gödla zakładał system dowodowy Hilberta-Ackermanna.

Oryginalne sformułowanie Gödla

Twierdzenie o zupełności mówi, że jeśli formuła jest logicznie poprawna, to istnieje skończona dedukcja (formalny dowód) formuły.

Zatem system dedukcyjny jest „kompletny” w tym sensie, że żadne dodatkowe reguły wnioskowania nie są wymagane do udowodnienia wszystkich logicznie ważnych formuł. Odwrotnością do kompletności jest poprawność , fakt, że w systemie dedukcyjnym można udowodnić tylko logicznie poprawne formuły. Wraz ze słusznością (której weryfikacja jest łatwa) twierdzenie to implikuje, że formuła jest logicznie ważna wtedy i tylko wtedy, gdy jest konkluzją formalnej dedukcji.

Bardziej ogólna forma

Twierdzenie można wyrazić bardziej ogólnie w kategoriach logicznej konsekwencji . Mówimy, że zdanie s jest syntaktyczną konsekwencją teorii T , oznaczaną , jeśli s można dowieść z T w naszym systemie dedukcyjnym. Mówimy, że s jest semantyczny konsekwencją od T , oznaczony , jeśli ów posiada w każdym modelu z T . Twierdzenie o zupełności mówi zatem, że dla dowolnej teorii pierwszego rzędu T z językiem dobrze uporządkowanym i dowolnego zdania s w języku T , ${\displaystyle T\vdash s}$${\displaystyle T\modele s}$

jeśli , to .${\displaystyle T\modele s}$${\displaystyle T\vdash s}$

Ponieważ zachodzi również odwrotność (zdrowość), wynika z tego , że wtedy i tylko wtedy , gdy , a zatem konsekwencja syntaktyczna i semantyczna są równoważne dla logiki pierwszego rzędu. ${\displaystyle T\modele s}$ ${\displaystyle T\vdash s}$

To bardziej ogólne twierdzenie jest używane implicite, na przykład, gdy zdanie jest udowodnione z aksjomatów teorii grup poprzez rozważenie dowolnej grupy i wykazanie, że zdanie jest spełnione przez tę grupę.

Oryginalne sformułowanie Gödla jest wydedukowane przez przyjęcie konkretnego przypadku teorii bez żadnego aksjomatu.

Twierdzenie o istnieniu modelu

Twierdzenie o zupełności może być również rozumiane w kategoriach niesprzeczności , jako konsekwencja twierdzenia Henkina o istnieniu modelu . Mówimy, że teoria T jest składniowo zgodna , jeśli nie ma zdanie s takie, że oba s i jego negację ¬ s to udowodnić z T naszego systemu dedukcyjnego. Twierdzenie o istnieniu modelu mówi, że dla każdej teorii pierwszego rzędu T z językiem dobrze uporządkowanym,

jeśli jest spójna składniowo, to ma model.${\ Displaystyle T}$${\ Displaystyle T}$

Inna wersja, z połączeniami z twierdzeniem Löwenheima-Skolema , mówi:

Każda syntaktycznie spójna, przeliczalna teoria pierwszego rzędu ma model skończony lub przeliczalny.

Mając twierdzenie Henkina, twierdzenie o zupełności można udowodnić w następujący sposób: Jeżeli , to nie ma modeli. Zgodnie z przeciwieństwem twierdzenia Henkina, to jest syntaktycznie niespójne. Tak więc sprzeczność ( ) można udowodnić z systemu dedukcyjnego. Stąd , a następnie przez właściwości systemu dedukcyjnego, . ${\displaystyle T\modele s}$${\ Displaystyle T \ filiżanka \ nie s}$${\ Displaystyle T \ filiżanka \ nie s}$${\displaystyle \bot}$${\ Displaystyle T \ filiżanka \ nie s}$${\ Displaystyle (T \ filiżanka \ nie s) \ vdash \ bot}$${\displaystyle T\vdash s}$

Jako twierdzenie arytmetyki

Twierdzenie o istnieniu modelu i jego dowód można sformalizować w ramach arytmetyki Peano . Dokładniej, możemy systematycznie zdefiniować model dowolnej spójnej efektywnej teorii pierwszego rzędu T w arytmetyce Peano, interpretując każdy symbol T za pomocą formuły arytmetycznej, której wolne zmienne są argumentami symbolu. (W wielu przypadkach będziemy musieli założyć, jako hipotezę konstrukcji, że T jest niesprzeczne, ponieważ arytmetyka Peano może tego nie udowodnić.) Jednak definicja wyrażona tą formułą nie jest rekurencyjna (ale w ogólności jest , Δ ₂ ).

Konsekwencje

Ważną konsekwencją twierdzenia o zupełności jest to, że możliwe jest rekurencyjne wyliczenie semantycznych konsekwencji dowolnej efektywnej teorii pierwszego rzędu, poprzez wyliczenie wszystkich możliwych formalnych dedukcji z aksjomatów teorii i użycie tego do wyliczenia ich wniosków .

Kontrastuje to z bezpośrednim znaczeniem pojęcia konsekwencji semantycznej, która obejmuje wszystkie struktury w danym języku, co oczywiście nie jest definicją rekurencyjną.

Czyni to także pojęcie „dowodliwości”, a tym samym „twierdzenia”, pojęciem jasnym, które zależy tylko od wybranego systemu aksjomatów teorii, a nie od wyboru systemu dowodowego.

Związek z twierdzeniami o niezupełności

Twierdzenia Gödla o niezupełności pokazują, że istnieją nieodłączne ograniczenia tego, co można udowodnić w ramach dowolnej teorii pierwszego rzędu w matematyce. „Niezupełność” w ich nazwie odnosi się do innego znaczenia zupełności (patrz teoria modeli – Korzystanie z twierdzeń o zwartości i zupełności ): Teoria jest zupełna (lub rozstrzygalna), jeśli każde zdanie w języku jest albo dowodzące ( ) albo nie do udowodnienia ( ) . ${\ Displaystyle T}$${\displaystyle S}$${\ Displaystyle T}$${\ Displaystyle T \ vdash S}$${\ Displaystyle T \ vdash \ neg S}$

Pierwsze twierdzenie o niezupełności mówi, że każdy, co jest niesprzeczny , skuteczny i zawiera arytmetykę Robinsona („ Q ”), musi być niekompletny w tym sensie, poprzez wyraźne skonstruowanie zdania, którego nie można udowodnić ani obalić w ramach . Drugie twierdzenie o niezupełności rozszerza ten wynik, pokazując, że można go wybrać tak, aby wyrażał spójność samego siebie. ${\ Displaystyle T}$${\displaystyle S_{T}}$${\ Displaystyle T}$${\displaystyle S_{T}}$${\ Displaystyle T}$

Ponieważ nie można obalić w , twierdzenie o zupełności implikuje istnienie modelu, w którym jest fałszywy. W rzeczywistości jest zdaniem Π ₁ , tj. stwierdza, że ​​jakaś własność skończona jest prawdziwa dla wszystkich liczb naturalnych; więc jeśli jest fałszywa, to jakaś liczba naturalna jest kontrprzykładem. Gdyby ten kontrprzykład istniał w obrębie standardowych liczb naturalnych, jego istnienie zostałoby obalone w obrębie ; ale twierdzenie o niezupełności pokazało, że jest to niemożliwe, więc kontrprzykład nie może być liczbą standardową, a zatem każdy model, w którym jest fałszywy, musi zawierać liczby niestandardowe . ${\displaystyle S_{T}}$${\ Displaystyle T}$${\ Displaystyle T}$${\displaystyle S_{T}}$${\displaystyle S_{T}}$${\displaystyle S_{T}}$${\ Displaystyle T}$${\ Displaystyle T}$${\displaystyle S_{T}}$

W rzeczywistości model dowolnej teorii zawierającej Q uzyskany przez systematyczną konstrukcję twierdzenia o istnieniu modelu arytmetycznego jest zawsze niestandardowy z nierównoważnym predykatem dowodliwości i nierównoważnym sposobem interpretacji własnej konstrukcji, tak że ta konstrukcja jest nierekurencyjny (ponieważ definicje rekurencyjne byłyby jednoznaczne).

Ponadto, jeśli jest przynajmniej nieco silniejszy niż Q (np. jeśli zawiera indukcję dla ograniczonych formuł egzystencjalnych), to twierdzenie Tennenbauma pokazuje, że nie ma rekurencyjnych modeli niestandardowych. ${\ Displaystyle T}$

Związek z twierdzeniem o zwartości

Twierdzenie o zupełności i twierdzenie o zwartości to dwa filary logiki pierwszego rzędu. Chociaż żadnego z tych twierdzeń nie można udowodnić w całkowicie skuteczny sposób, każde z nich można skutecznie uzyskać od drugiego.

Twierdzenie o zwartości mówi, że jeśli formuła φ jest logiczną konsekwencją (prawdopodobnie nieskończonego) zbioru formuł Γ, to jest logiczną konsekwencją skończonego podzbioru Γ. Jest to bezpośrednia konsekwencja twierdzenia o zupełności, ponieważ tylko skończoną liczbę aksjomatów z Γ można wymienić w formalnej dedukcji φ, a poprawność systemu dedukcyjnego implikuje φ jest logiczną konsekwencją tego skończonego zbioru. Ten dowód twierdzenia o zwartości pochodzi od Gödla.

Odwrotnie, w przypadku wielu systemów dedukcyjnych możliwe jest udowodnienie twierdzenia o zupełności jako efektywnej konsekwencji twierdzenia o zwartości.

Nieskuteczność twierdzenia o zupełności można zmierzyć zgodnie z matematyką odwrotną . Twierdzenia o zupełności i zwartości, gdy są rozpatrywane w języku policzalnym, są równoważne sobie i równoważne słabej formie wyboru znanej jako słaby lemat Königa , z równoważnością możliwą do udowodnienia w RCA ₀ (wariant drugiego rzędu arytmetyki Peano ograniczony do indukcji ponad Σ ⁰ ₁ formuł). Słaby lemat Königa jest możliwy do udowodnienia w ZF, systemie teorii mnogości Zermelo-Fraenkela bez aksjomatu wyboru, a zatem twierdzenia o zupełności i zwartości dla języków policzalnych można udowodnić w ZF. Jednak sytuacja jest inna, gdy język ma arbitralnie dużą kardynalność, od tego czasu, chociaż twierdzenia o zupełności i zwartości pozostają dowodowo równoważne w ZF, są one również dowodowo równoważne ze słabą formą aksjomatu wyboru, znaną jako lemat ultrafiltru. . W szczególności żadna teoria rozszerzająca ZF nie może udowodnić ani twierdzeń o zupełności, ani o zwartości w dowolnych (prawdopodobnie niepoliczalnych) językach bez udowodnienia również lematu ultrafiltru na zbiorze o tej samej kardynalności.

Kompletność w innych logikach

Twierdzenie o zupełności jest centralną własnością logiki pierwszego rzędu , która nie obowiązuje dla wszystkich logik. Na przykład logika drugiego rzędu nie ma twierdzenia o zupełności dla swojej standardowej semantyki (ale ma właściwość zupełności dla semantyki Henkina ), a zbiór logicznie poprawnych formuł w logice drugiego rzędu nie jest rekurencyjnie przeliczalny. To samo dotyczy wszystkich logik wyższego rzędu. Możliwe jest wytworzenie dźwiękowych systemów dedukcyjnych dla logik wyższego rzędu, ale żaden taki system nie może być kompletny.

Twierdzenie Lindströma mówi, że logika pierwszego rzędu jest najsilniejszą (z pewnymi ograniczeniami) logiką spełniającą zarówno zwartość, jak i zupełność.

Twierdzenie o zupełności można udowodnić dla logiki modalnej lub logiki intuicjonistycznej w odniesieniu do semantyki Kripkego .

Dowody

Gödla oryginalny dowód twierdzenia przebiegała przez zmniejszenie problemu szczególnym przypadku dla formuł w pewnej formie składniowej, a następnie przenoszenia tego formularza z ad hoc argument.

We współczesnych tekstach logicznych twierdzenie Gödla o zupełności jest zwykle udowadniane za pomocą dowodu Henkina , a nie za pomocą oryginalnego dowodu Gödla. Dowód Henkina bezpośrednio konstruuje model terminowy dla dowolnej spójnej teorii pierwszego rzędu. James Margetson (2004) opracował skomputeryzowany dowód formalny przy użyciu dowodzącego twierdzenia Isabelle . Znane są również inne dowody.

Zobacz też

• Twierdzenia o niezupełności Gödla
• Oryginalny dowód twierdzenia o zupełności Gödla

Dalsza lektura

• Gödel, K (1929). „Über die Vollständigkeit des Logikkalküls” . Rozprawa doktorska. Uniwersytet Wiedeński. Cytowanie dziennika wymaga |journal=( pomoc ) Pierwszy dowód twierdzenia o zupełności.
• Gödel, K (1930). „Die Vollständigkeit der Axiome des logischen Funktionkalküls”. Monatshefte für Mathematik (w języku niemieckim). 37 (1): 349–360. doi : 10.1007/BF01696781 . JFM  56.0046.04 . S2CID  123343522 . Ten sam materiał co rozprawa, z wyjątkiem krótszych dowodów, bardziej zwięzłych wyjaśnień i pominięcia przydługiego wstępu.

Zewnętrzne linki

• Stanford Encyclopedia of Philosophy : „ Kurt Gödel ” — Juliette Kennedy .
• Biografia MacTutora: Kurt Gödel.
• Detlovs, Wilnis i Podnieks, Karlis, „ Wprowadzenie do logiki matematycznej ”.