Twierdzenie Gödla o zupełności

Nie mylić z twierdzeniami Gödla o niezupełności .

Formuła ( ∀ x . R ( x , x )) → ( ∀ x ∃ y . R ( x , y )) zachodzi we wszystkich strukturach (po lewej pokazano tylko 8 najprostszych). Wynik kompletności Gödla musi zatem mieć naturalny dowód dedukcji (pokazany po prawej).

Twierdzenie Gödla o kompletności jest fundamentalnym twierdzeniem logiki matematycznej , które ustanawia zgodność między prawdą semantyczną a dowodzeniem składniowym w logice pierwszego rzędu .

teorii pierwszego rzędu : jeśli T jest taką teorią, a φ jest zdaniem (w tym samym języku) i każdy model T jest modelem φ, to istnieje dowód (pierwszego rzędu) φ używając stwierdzeń T jako aksjomatów. Czasami mówi się, że „wszystko, co jest powszechnie prawdziwe, można udowodnić”. Nie jest to sprzeczne z twierdzeniem Gödla o niezupełności , które pokazuje, że pewna formuła φ _u jest niedowodliwa, chociaż jest prawdziwa w liczbach naturalnych, które są szczególnym modelem opisującej je teorii pierwszego rzędu — φ _u jest po prostu fałszywe w jakimś innym modelu rozpatrywanej teorii pierwszego rzędu (takim jak niestandardowy model arytmetyki dla arytmetyki Peano ). Ten rodzaj braku spójności między standardowym i niestandardowym modelem jest również nazywany niespójnością Omega.

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

Po raz pierwszy udowodnił to Kurt Gödel w 1929 roku. Następnie zostało to uproszczone, gdy Leon Henkin zauważył w swoim doktoracie . tezę , że twardą część dowodu można przedstawić jako modelowe twierdzenie o istnieniu (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 sekwencja (lub, w niektórych przypadkach, skończone drzewo ) formuł ze specjalnie wyznaczonym wnioskiem . Definicja dedukcji jest taka, że ​​jest skończona i możliwa do zweryfikowania algorytmicznie (przez komputer , na przykład lub ręcznie), że dana sekwencja (lub drzewo) formuł jest rzeczywiście dedukcją.

Formułę pierwszego rzędu nazywamy logicznie ważną , jeśli jest prawdziwa w każdej strukturze dla języka formuły (tj. dla dowolnego przypisania wartości zmiennym 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 ważna formuła jest konkluzją jakiejś formalnej dedukcji, a twierdzeniem o zupełności dla określonego systemu dedukcyjnego jest twierdzenie, że jest on w tym sensie zupełny. Zatem w pewnym sensie istnieje inne twierdzenie o zupełności dla każdego systemu dedukcyjnego. Odwrotnością do kompletności jest słuszność , fakt, że tylko logicznie poprawne formuły są dowodliwe w systemie dedukcyjnym.

Jeśli jakiś określony system dedukcyjny logiki pierwszego rzędu jest poprawny i kompletny, to jest „doskonały” (formuła jest dowodliwa wtedy i tylko wtedy, gdy jest logicznie poprawny), a zatem 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 inny).

Oświadczenie

Najpierw ustalimy dedukcyjny system 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 dowodu Hilberta-Ackermanna.

Oryginalna formuła Gödla

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

Zatem system dedukcyjny jest „kompletny” w tym sensie, że do udowodnienia wszystkich logicznie poprawnych formuł nie są wymagane żadne dodatkowe reguły wnioskowania. Odwrotnością kompletności jest solidność , fakt, że tylko logicznie poprawne formuły są dowodliwe w systemie dedukcyjnym. Wraz z zasadnoś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 $.$ zdanie s jest składniową konsekwencją teorii T , oznaczonej jeśli s można udowodnić z T w naszym systemie dedukcyjnym Mówimy, że s jest semantyczną konsekwencją T , oznaczoną , jeśli s ${\ Displaystyle T \ modele s}$ zachodzi w każdym modelu T . Twierdzenie o zupełności mówi następnie, że dla dowolnej teorii pierwszego rzędu T z dobrze uporządkowanym językiem i dla dowolnych zdań s w języku T ,

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

Ponieważ zachodzi również odwrotność (poprawność), wynika z tego, że ${\ displaystyle T \ modele s}$ wtedy i tylko wtedy, gdy ${\ displaystyle T \ vdash s}$ , a zatem ta konsekwencja składniowa i semantyczna są równoważne dla pierwszego -logika porządku.

To bardziej ogólne twierdzenie jest używane pośrednio, na przykład, gdy okazuje się, że zdanie można udowodnić na podstawie aksjomatów teorii grup , biorąc pod uwagę dowolną grupę i pokazując, że zdanie jest spełnione przez tę grupę.

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

Twierdzenie o istnieniu modelu

Twierdzenie o zupełności można również rozumieć w kategoriach spójności , jako konsekwencja twierdzenia Henkina o istnieniu modelu . Mówimy, że teoria T jest spójna składniowo, jeśli nie ma zdania s takiego, że zarówno s, jak i jego zaprzeczenie ¬s są możliwe do udowodnienia z T w naszym systemie dedukcyjnym. Twierdzenie o istnieniu modelu mówi, że dla dowolnej teorii pierwszego rzędu T z dobrze uporządkowanym językiem

jeśli $jest$$spójny$ składniowo, to .

Inna wersja, z powiązaniami z twierdzeniem Löwenheima-Skolema , mówi:

Każda spójna składniowo, policzalna teoria pierwszego rzędu ma skończony lub policzalny model.

$nie$ uwagę twierdzenie Henkina, twierdzenie o kompletności można udowodnić w następujący $,$ to ma Przez kontrapozycję twierdzenia Henkina $niespójne$ składniowo Tak więc sprzeczność ( $)$ jest możliwa do udowodnienia na podstawie $\ Displaystyle T \ cup \ lnot s}$ w systemie dedukcyjnym. Stąd ${\ Displaystyle (T \ cup \ lnot s) \ vdash \ bot}$ , a następnie przez właściwości systemu dedukcyjnego ${\ Displaystyle T \ vdash s}$ .

Jako twierdzenie arytmetyki

Modelowe twierdzenie o istnieniu 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ą wzoru arytmetycznego, którego zmiennymi wolnymi są argumenty symbolu. (W wielu przypadkach będziemy musieli założyć jako hipotezę konstrukcji, że T jest zgodne, ponieważ arytmetyka Peano może tego nie dowieść). Jednak definicja wyrażona tym wzorem nie jest rekurencyjna (ale generalnie 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 wykorzystanie tego do wyliczenia ich wniosków .

Stoi to w sprzeczności z bezpośrednim znaczeniem pojęcia konsekwencji semantycznej, które określa ilościowo wszystkie struktury w określonym języku, co oczywiście nie jest definicją rekurencyjną.

Sprawia również, że pojęcie „dowodliwości”, a więc i „twierdzenia”, jest 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 $T}$ ( patrz teoria modelu - Używanie twierdzeń o zwartości i kompletności ): Teoria jest kompletna (lub rozstrzygalna), jeśli każde zdanie w $displaystyle$ język ${\ displaystyle T}$ jest albo do udowodnienia ( ${\ Displaystyle T \ vdash S}$ ) lub obalić ( ${\ Displaystyle T \ vdash \ neg S}$ ).

Pierwsze twierdzenie o niezupełności stwierdza, że ​​​​każdy , który jest spójny $), musi być w$ skuteczny i zawiera arytmetykę Robinsona („ Q ” ${\ displaystyle S_ {T}}$ sensie niekompletny, poprzez jawne skonstruowanie zdania, które jest wyraźnie ani do udowodnienia, ani do obalenia w ciągu ${\ displaystyle T}$ . Drugie twierdzenie o niezupełności rozszerza ten wynik, pokazując, że ${\ Displaystyle S_ {T}}$ można wybrać tak, aby wyrażało spójność samego ${\ displaystyle T}$ .

Ponieważ nie można udowodnić w , twierdzenie o kompletności implikuje istnienie modelu $,$${\ displaystyle T$$}$ w którym $}$ to fałsz. W rzeczywistości jest to zdanie Π _; $1$ , tj. stwierdza, że ​​​​pewna właściwość finitystyczna jest prawdziwa dla wszystkich więc jeśli jest fałszywe, to jakaś liczba naturalna jest kontrprzykładem. Gdyby ten kontrprzykład istniał w ramach standardowych liczb naturalnych, jego istnienie byłoby obalone ${\ Displaystyle S_ {T}}$ w ciągu ${\ displaystyle T}$ ; ale twierdzenie o niezupełności wykazało $T}$ 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ć niestandardowe $displaystyle$ liczby .

W rzeczywistości model dowolnej teorii zawierającej Q otrzymany 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 co najmniej nieco silniejsze niż $,$ (np. jeśli obejmuje indukcję dla ograniczonych formuł egzystencjalnych), to twierdzenie Tennenbauma pokazuje że nie ma rekurencyjnych niestandardowych modeli.

Związek z twierdzeniem o zwartości

Twierdzenie o zupełności i twierdzenie o zwartości to dwa kamienie węgielne 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ć z 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ż w formalnej dedukcji φ można wymienić tylko skończoną liczbę aksjomatów z Γ, a prawidłowość systemu dedukcyjnego implikuje, że φ jest logiczną konsekwencją tego skończonego zbioru. Ten dowód twierdzenia o zwartości pochodzi pierwotnie od Gödla.

I odwrotnie, dla wielu systemów dedukcyjnych możliwe jest udowodnienie twierdzenia o zupełności jako skutecznej konsekwencji twierdzenia o zwartości.

₀⁰ Nieskuteczność twierdzenia o zupełności można zmierzyć na wzór matematyki odwrotnej . Rozważane w języku policzalnym twierdzenia o zupełności i zwartości są sobie równoważne i równoważne słabej formie wyboru znanej jako słaby lemat Königa , z równoważnością do udowodnienia w RCA (wariant drugiego rzędu arytmetyki Peano ograniczony do indukcji po wzory Σ1 _{) .} Słaby lemat Königa można udowodnić 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 dowolną dużą liczność od tego czasu, chociaż twierdzenia o zupełności i zwartości pozostają w ZF w sposób dający się udowodnić równoważne, są one również w sposób w sposób możliwy do udowodnienia równoważne słabej formie aksjomatu wyboru znanej jako lemat ultrafiltra . 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 jednoczesnego udowodnienia lematu ultrafiltra na zbiorze o tej samej liczności.

Kompletność w innych logiki

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

Twierdzenie Lindströma stwierdza, że ​​logika pierwszego rzędu jest najsilniejszą (podlegającą pewnym ograniczeniom) logiką spełniającą zarówno zwartość, jak i kompletność.

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

Dowody

Oryginalny dowód twierdzenia Gödla polegał na sprowadzeniu problemu do szczególnego przypadku dla formuł w określonej formie składniowej, a następnie potraktowaniu tej formy za pomocą argumentu ad hoc .

We współczesnych tekstach logicznych twierdzenie Gödla o zupełności jest zwykle udowadniane za pomocą dowodu Henkina , a nie 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, używając Isabelle . Znane są również inne dowody.

Zobacz też

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

Dalsza lektura

• Gödel, K. (1929). Über die Vollständigkeit des Logikkalküls (praca). Rozprawa doktorska. Uniwersytet Wiedeński. Pierwszy dowód twierdzenia o zupełności.
•    Gödel, K. (1930). „Die Vollständigkeit der Axiome des logischen Funktionenkalkü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 długiego wstępu.
•    Hansa Hermesa (1973). Wprowadzenie do logiki matematycznej . Hochschultext (Springer-Verlag). Londyn: Springer. ISBN 3540058192 . ISSN 1431-4657 . Rozdział 5: „Twierdzenie Gödla o zupełności” .

Linki zewnętrzne

• Stanford Encyclopedia of Philosophy : „ Kurt Gödel ” - autorstwa Juliette Kennedy .
• Biografia MacTutor: Kurt Gödel. Zarchiwizowane 13.10.2005 w Wayback Machine
• Detlovs, Vilnis i Podnieks, Karlis, „ Wprowadzenie do logiki matematycznej ” .