Logika dla informatyków/Pełność rachunku predykatów

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania

Hilbertowski system dowodzenia

Poniższy system dowodzenia dotyczy formuł pierwszego rzędu nad ustaloną sygnaturą , zbudowanych w oparciu o spójniki , oraz kwantyfikator . Przypomnijmy, że Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \neg\var\varphi} oznacza formułę Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi\rightarrow\perp} .

Przez generalizację formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} będziemy rozumieć dowolną formułę postaci Parser nie mógł rozpoznać (nieznana funkcja „\ciut”): {\displaystyle \forall x_1\ldots\forall x_n\ciut\var\varphi} , gdzie są dowolnymi zmiennymi.

Aksjomaty

Dowolne generalizacje formuł postaci:

(A1)   Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi\rightarrow(\psi\rightarrow\var\varphi)} ;
(A2)   Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle (\var\varphi\rightarrow(\psi\rightarrow\vartheta))\rightarrow((\var\varphi\rightarrow\psi)\rightarrow(\var\varphi\rightarrow\vartheta))} ;
(A3)   Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \neg\neg\var\varphi\rightarrow\var\varphi} ;
(A4)   Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \forall x(\var\varphi\rightarrow\psi)\rightarrow(\forall x\var\varphi\rightarrow\forall x\psi)} ;
(A5)   Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi\rightarrow \forall x \var\varphi} , o ile Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle x\not\in FV(\var\varphi)} ;
(A6)   Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \forall x\var\varphi\rightarrow \var\varphi(\sigma/x)} , o ile jestdopuszczalny dla w Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} ;
(A7)   ;
(A8)   , dla
        ;
(A9)   , dla
         .

Reguły dowodzenia

(MP)    Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \frac{\varphi\hspace{1cm}\varaphi\rightarrow\psi}{\psi}}

Pojęcie dowodu formalnego w powyższym systemie definiuje się dokładnie tak samo jak w przypadku rachunku zdań (por. Rozdział 2). Możliwość udowodnienia formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} ze zbioru hipotez w powyższym systemie będziemy oznaczać przez . Sam system, podobnie jak w przypadku rachunku zdań, będziemy oznaczać przez . Nie powinno prowadzić to do niejednoznaczności. Zwróćmy uwagę, że system zależy od sygnatury . Tak więc mamy różne systemy dla różnych sygnatur. Pojęcie niesprzecznego zbioru formuł definiuje się tak samo jak w rachunku zdań.


Przykład 7.1

Pokażemy główne kroki dowodu formuły .

  1.    (A9)
  2.     na mocy (A6) oraz(MP)
  3.     z (2), jest to instancja tautologii zdaniowej
  4.    (A7)
  5.    (MP(4,3))
  6.     z (5), jest to instancja tautologii zdaniowej
  7.    (A7)
  8.    (MP(7,6))


Twierdzenie 7.2 (o dedukcji)

Dla dowolnego zbioru formuł oraz dowolnych formuł Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi,\psi} ,jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta,\var\varphi\vdash_H\psi} , to Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\vdash_H\var\varphi\rightarrow\psi} .

Dowód

Dowód tego twierdzenia jest dokładnie taki sam, jak analogicznego twierdzenia dla rachunku zadań (por. Twierdzenie 5.2). End of proof.gif

Natępujące twierdzenie mówi, że wybór nazwy zmiennej związanej nie ma wpływu na dowodliwość formuły. Jest to tzw. własność -konwersji.

Twierdzenie 7.3 (o -konwersji)

Jeśli oraz zmienna jest dopuszczalna dla w , to .

Dowód

Ponieważ , to na mocy (A5) mamy . Z drugiej strony mamy następującą wersję aksjomatu (A6), co łącznie z aksjomatem (A4) daje . Tak więc zakładając i stosując(MP) do (7), a następnie do (8), dostajemy co kończy dowód. End of proof.gif


Podamy jeszcze jedno użyteczne twierdzenie. Mówi ono, że tzw. reguła generalizacji jest dopuszczalna w systemie . Niech

Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle FV(\Delta)=\bigcup\{FV(\var\varphi)\ |\ \var\varphi\in\Delta\}.}

Twierdzenie 7.4 (o generalizacji)

Jeśli zachodzi Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\vdash_H\var\varphi} , to dla dowolnej zmiennej , takiej że , mamy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\vdash_H\forall x\,\var\varphi} .

Dowód

Dowodzimy twierdzenie przez indukcję ze względu na liczbę kroków w dowodzie formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} ze zbioru hipotez . Jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest jednym z aksjomatów (A1--9), to dowolna generalizacja tej formuły jest też aksjomatem, więc teza zachodzi. Aby pokazać Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\vdash_H\forall x\,\var\varphi} , dla formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi\in\Delta} używamy aksjomatu (A5) i reguły (MP).

Jeśli ostatnim krokiem w dowodzie było zastosowanie (MP), to dla pewnej formuły mamy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\vdash_H\psi\rightarrow\var\varphi} oraz w mniejszej liczbie kroków. Z założenia indukcyjnego otrzymujemy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\vdash_H\forall x\,(\psi\rightarrow\var\varphi)} oraz . Zatem stosując (MP) do Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \forall x\,(\psi\rightarrow\var\varphi)} oraz do instancji Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \forall x(\psi\rightarrow\var\varphi)\rightarrow(\forall x\psi\rightarrow\forall x\var\varphi)} aksjomatu (A4) otrzymujemy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \forall x\psi\rightarrow\forall x\var\varphi} . Ponowne zastosowanie (MP) do tej formuły oraz do daje nam Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \forall x\,\var\varphi} . End of proof.gif

Powiemy, że formuła Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest konsekwencją semantyczną zbioru formuł (i napiszemy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\models\var\varphi} ), gdy dla każdej struktury i dla każdego wartościowania w spełniającego wszystkie formuły ze zbioru , mamy Parser nie mógł rozpoznać (nieznana funkcja „\sat”): {\displaystyle \sat\mathfrak A\varrho\var\varphi} . Zwróćmy uwagę, że jeśli jest zbiorem zdań, to powyższa definicja jest równoważna następującej własności: każdy model dla jest modelem dla Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} . W ogólnym przypadku, gdy formuły z mogą zawierać zmiennewolne, powyższe dwie definicje nie są równoważne. Na przykład, jeśli jest symbolem operacji jednoargumentowej, to , ale każdy model dla (czyli jednoelementowy) jest modelem dla .

Twierdzenie 7.5 (o poprawności)

Dla dowolnego zbioru formuł i formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} , jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\vdash_H\var\varphi} , to Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\models\var\varphi} .

Dowód

Dowód przeprowadzamy przez indukcję ze względu na liczbę kroków w dowodzie formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} ze zbioru hipotez . Jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi\in\Delta} , to oczywiście mamy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\models\var\varphi} . Sprawdzamy, że jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest dowolną generalizacją jednego z aksjomatów (A1--9), to zachodzi Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \models\var\varphi} . Oczywiście reguła (MP) zachowuje relację semantycznej konsekwencji, tzn. jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\models\var\varphi} i Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\models\var\varphi\rightarrow\psi} , to . End of proof.gif

Twierdzenie o poprawności może być użyte do pokazania, że pewne wynikania nie dają się wyprowadzić w systemie . Przykładowo, zobaczmy, że . Istotnie, biorąc dwuelementową strukturę oraz wartościowanie, które "skleja" wartości zmiennych oraz , dostajemy . Zatem z twierdzenia o poprawności wnioskujemy, że . Jest to również przykład na to, że system nie jest zamknięty ze względu na dowolne generalizacje, tzn. założenie w twierdzeniu o generalizacji jest istotne.

Zachodzi również odwrotne twierdzenie do Twierdzenia 7.5. Dowód tego twierdzenia jest celem niniejszego rozdziału.

System formalny dla formuł zawierających pozostałe spójniki: i kwantyfikator egzystencjalny otrzymuje się z przez dodanie aksjomatów charakteryzujących te symbole:

(B1)  Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi\wedge \psi\rightarrow\neg(\var\varphi\rightarrow\neg\psi)}
(B2)  Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \neg(\var\varphi\rightarrow\neg\psi)\rightarrow\var\varphi\wedge \psi}
(B3)  Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi\vee\psi\rightarrow(\neg\var\varphi\rightarrow\psi)}
(B4)  Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle (\neg\var\varphi\rightarrow\psi)\rightarrow\var\varphi\vee\psi}
(B5)  Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \exists x\,\var\varphi\rightarrow \neg\forall x\,\neg\var\varphi}
(B6)  Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \neg\forall x\,\neg\var\varphi\rightarrow \exists x\,\var\varphi}


Głównym narzędziem w dowodzie "silnego" twierdzenia o pełności będzie tzw. twierdzenie o istnieniu modelu. Metoda dowodu tego twierdzenia polega na budowaniu modelu ze stałych. Zaproponował ją L. Henkin.

Najpierw wprowadzimy następującą definicję. Niech będzie zbiorem zdań pierwszego rzędu nad sygnaturą oraz niech będzie pewnym zbiorem stałych. Powiemy, że jest zbiorem -nasyconym, gdy jest zbiorem niesprzecznym oraz dla dowolnej formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi(x)} o co najwyżej jednej zmiennej wolnej , jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Gamma\not\vdash_H\forall x\,\var\varphi(x)} , to istnieje stała ,taka że Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Gamma\vdash_H\neg\var\varphi(c/x)} .

Niech będzie -nasycony. Zauważmy, że jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Gamma\vdash_H\neg\forall x\,\var\varphi(x)} oraz jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest postaci , to wówczas Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Gamma\vdash_H\neg\forall x\var\varphi(x)} jest równoważne . Ponadto z warunku -nasycenia wynika istnienie stałej takiej, że Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Gamma\vdash_H\neg\var\varphi(c/x). \Rightarrow } ostatnie jest równoważne (na mocy prawa podwójnego przeczenia) temu, że . Tak więc w tym przypadku jest "świadkiem" zachodzenia własności Parser nie mógł rozpoznać (nieznana funkcja „\existsx”): {\displaystyle \Gamma\vdash_H\existsx\ \psi(x)} .

Mocą sygnatury nazwiemy moc zbioru . Moc sygnatury będziemy oznaczać przez .

Dopuścimy możliwość rozszerzenia sygnatury o stałe. Dla dowolnego zbioru rozłącznego z sygnaturą , przez będziemy oznaczać sygnaturę powstałą z przez dodanie symboli stałych ze zbioru .

Lemat 7.6 (o nasyceniu)

Niech będzie nieskończonym zbiorem, rozłącznym z sygnaturą oraz takim, że . Niech będzie niesprzecznym zbiorem zdań nad . Istnieje zbiór zdań nad sygnaturą taki, że oraz jest-nasycony.

Dowód

Bez zmniejszenia ogólności możemy przyjąć, że istnieje zmienna nie występująca wolno w żadnej formule ze zbioru (w przeciwnym przypadku możemy tak przenumerować zmienne, aby ten warunek był spełniony). Przedstawimy dowód dla przypadku, kiedy i są zbiorami przeliczalnymi. Dowód ogólnego przypadku pozostawimy Czytelnikowi jako ćwiczenie (należy zastosować indukcję pozaskończoną). Ustawmy zbiór wszystkich formuł nad o jednej zmiennej wolnej w ciąg Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi_0,\var\varphi_1,\ldots} Zdefiniujemy ciąg zbiorów Parser nie mógł rozpoznać (nieznana funkcja „\n”): {\displaystyle \{\Gamma_n\ |\n\in \NN\}} oraz ciąg stałych Parser nie mógł rozpoznać (nieznana funkcja „\NN”): {\displaystyle \{c_n\ |\ n\in \NN\}\subseteq C} o następujących własnościach:

  • zawiera skończenie wiele stałych z .
  • jest niesprzecznym zbiorem zdań nad .
  • Jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Gamma_n\not\vdash_H\forall x\,\var\varphi_n(x)} , to Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Gamma_{n+1}=\Gamma_n\cup\{\neg\var\varphi_n(c_n/x)\}} .


Ustalmy dowolną stałą . Przyjmujemy . Jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Gamma_n\vdash_H\forall x\,\var\varphi_n(x)} , to definiujemy oraz . Jeśli natomiast Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Gamma_n\not\vdash_H\forall x\,\var\varphi_n(x)} , to niech będzie stałą nie występującą w ani w Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi_n} . Musimy pokazać, że Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Gamma_{n+1}=\Gamma_n\cup\{\neg\var\varphi_n(c_n/x)\}} jest zbiorem niesprzecznym. Załóżmy przeciwnie, że

Zatem Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Gamma_n\vdash_H\neg\neg\var\varphi_n(c_n/x)} i z (A3) dostajemy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Gamma_n\vdash_H\var\varphi_n(c_n/x)} . Ponieważ nie występuje w ani w Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi_n} , to możemy w dowodzie powyższego sekwentu zamienić wszystkie wystąpienia przez nową zmienną , która się w tym dowodzie nie pojawiła oraz nie występuje wolno w formułach z . Tak więc otrzymujemy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Gamma_n\vdash_H\var\varphi_n(z/x)} oraz . Na mocy Twierdzenia 7.4 o generalizacji dostajemy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Gamma_n\vdash_H \forall z\ \var\varphi_n(z/x)} . Ponieważ jest dopuszczalna dla w Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi_n(z/x)} oraz Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi_n(z/x)(x/z)=\var\varphi_n(x)} , to stosując -konwersję (Twierdzenie 7.3) dostajemy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Gamma_n\vdash_H\forall x\,\var\varphi_n(x)} , wbrew założeniu. W ten sposób udowodniliśmy niesprzeczność zbioru kończy konstrukcję zbiorów oraz stałych .

Niech

Pokażemy, że jest zbiorem -nasyconym. Oczywiście jako suma łańcucha zbiorów niesprzecznych jest również zbiorem niesprzecznym. Niech Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi(x)} będzie dowolną formułą nad o jednej zmiennej wolnej i załóżmy, że Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Gamma\not\vdash_H \forall x\,\var\varphi(x)} . Niech Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi(x)=\var\varphi_n(x)} dla pewnego . Oczywiście mamy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Gamma_n\not\vdash_H\forall x\,\var\varphi_n(x)} i z konstrukcji zbiorów wynika, że Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Gamma_{n+1}\vdash_H \neg\var\varphi_n(c_n/x)} . Zatem Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Gamma\vdash_H \neg\var\varphi_n(c_n/x)} , co dowodzi -nasycenia zbioru . End of proof.gif

Konstrukcja modelu ze stałych

Niech będzie dowolnym zbiorem stałych i niech będzie dowolnym -nasyconym zbiorem zdań nad . W zbiorze definiujemy relację równoważności :

   wtedy i tylko wtedy, gdy

Zdefiniujemy strukturę . Nośnikiem tej struktury jest zbiór ilorazowy . Musimy określić interpretację symboli operacji i relacji z . Dla przykładu załóżmy, że jest symbolem operacji dwuargumentowej. Funkcję Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle f^{\mathfrak A_\Gamma}:(C/\sim)^2\arr C/\sim} definiujemy warunkiem

 wtedy i tylko wtedy, gdy 

Dla pokazania, że jest dobrze określoną funkcją musimy sprawdzić, że:

Dla dowolnych   istnieje    takie, że      (9)

Jeśli    oraz    i    to      (10)

Własność (9) wynika z faktu, że zbiór jest -nasycony. Zauważmy najpierw, że . Istotnie, załóżmy . Wówczas z aksjomatu (A6) dostajemy . Z drugiej strony, z aksjomatu (A7) i (A6) dostajemy . Tak więc otrzymujemy , a więc . Zatem z -nasycenia wynika istnienie stałej takiej, że . Korzystając teraz z (A3) dostajemy .

Własność (10) wynika natychmiast z następującej postaci aksjomatu (A8) (postać tę otrzymujemy z (A8) z pomocą aksjomatu (A6))

Interpretacja symboli relacji w wygląda podobnie. Dla przykładu zdefiniujemy relację dla symbolu .

 wtedy i tylko wtedy, gdy 

W tym przypadku również musimy dowieść poprawności definicji (tzn. niezależności od wyboru reprezentantów). Czyli musimy pokazać, że jeśli oraz , to

 wtedy i tylko wtedy, gdy 

Wynika to natychmiast z aksjomatów (A9) i (A6).


Teraz możemy przejść do twierdzenia o istnieniu modelu.

Twierdzenie 7.7 (o istnieniu modelu)

Każdy niesprzeczny zbiór zdań nad dowolną sygnaturą ma model, którego moc nie przekracza . Dokładniej, dla struktury zbudowanej powyżej oraz dowolnej formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} takiej, że Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle FV(\var\varphi)\subseteq\{x_1,\ldots,x_n\}} i dla dowolnego wartościowania takiego, że dla mamy Parser nie mógł rozpoznać (nieznana funkcja „\sat”): {\displaystyle \sat{\mathfrak A_\Gamma}\varrho\var\varphi\WTW\Gamma\vdash_H \var\varphi(c_1/x_1,\ldots,c_n/x_n)} .

Dowód

Załóżmy, że jest niesprzecznym zbiorem zdań. Niech będzie dowolnym nieskończonym zbiorem rozłącznym z i takim, że . Z Lematu 7.6 o nasyceniu wiemy, że istnieje zbiór zdań Parser nie mógł rozpoznać (nieznana funkcja „\Gammasbseteq”): {\displaystyle \Gammasbseteq\Delta} nad sygnaturą , który jest -nasycony. Stosując lemat Kuratowskiego-Zorna dowodzimy, że istnieje maksymalny zbiór o powyższych własnościach. Niech będzie takim zbiorem. Dalsza część dowodu będzie przebiegała w odniesieniu do ustalonego zbioru .

Najpierw zanotujmy następującą ważną własność zbioru .

Dla dowolnego zdania Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} , jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Gamma\not\vdash_H\var\varphi} , to  Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Gamma\cup\{\var\varphi\}}  jest zbiorem sprzecznym. (12)

Dla dowodu (12) zauważmy, że jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Gamma\cup\{\var\varphi\]]} jest zbiorem niesprzecznym, to jest on -nasycony. Istotnie, jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Gamma\cup\{\var\varphi\}\not\vdash_H \forall x\,\psi(x)} , dla pewnej formuły o jednej zmiennej wolnej, to mamy również . Zatem dla pewnej stałej zachodzi , więc oczywiście również Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Gamma\cup\{\var\varphi\}\vdash_H\neg\psi(c/x)} . Tak więc z maksymalności zbioru wynika, że Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Gamma\cup\{\var\varphi\}} musi być zbiorem sprzecznym. To dowodzi (12).

Zauważmy, że z własności (11) wynika pierwsza część twierdzenia, bowiem mamy wówczas . Własność (11) dowodzimy przez indukcję ze względu na budowę formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} . Dla formuł atomowych musimy dowieść następującą pomocniczą własność. Dla dowolnego termu i stałej mamy Parser nie mógł rozpoznać (nieznana funkcja „\wart”): {\displaystyle \wart\prooftree t \justifies \mathfrak A_\Gamma \using \textrm{(W)}\endprooftree\varrho=[d]_\sim\WTW \Gamma\vdash_H {t}(c_1/x_1,\ldots,c_n/x_n)=d, }

gdzie oraz , dla . Dowód (13) przeprowadzamy przez rutynową indukcję ze względu na budowę termu . Szczegóły pozostawiamy Czytelnikowi.

Powracamy do dowodu (11). Jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest formułą , to Parser nie mógł rozpoznać (nieznana funkcja „\wart”): {\displaystyle \wart\prooftree {t}_1 \justifies \mathfrak A_\Gamma \using \textrm{(W)}\endprooftree\varrho= \wart\prooftree {t}_2 \justifies \mathfrak A_\Gamma \using \textrm{(W)}\endprooftree\varrho} wtedy i tylko wtedy, gdy dla pewnego zachodzi Parser nie mógł rozpoznać (nieznana funkcja „\wart”): {\displaystyle \wart\prooftree {t}_1 \justifies \mathfrak A_\Gamma \using \textrm{(W)}\endprooftree\varrho=[d]_\sim} oraz Parser nie mógł rozpoznać (nieznana funkcja „\wart”): {\displaystyle \wart\prooftree {t}_2 \justifies \mathfrak A_\Gamma \using \textrm{(W)}\endprooftree\varrho=[d]_\sim} . Na mocy (13) jest to równoważne temu, że dla pewnego zachodzi oraz . Ostatnia własność jest równoważna (na mocy -nasycenia zbioru ) własności .

Załóżmy teraz, że Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest formułą postaci Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \psi\arr\vartheta} . Niech oznacza formułę oraz niech oznacza formułę . Załóżmy, że Parser nie mógł rozpoznać (nieznana funkcja „\sat”): {\displaystyle \sat{\mathfrak A_\Gamma}\varrho\var\varphi} i rozważmy dwa przypadki. Jeśli , to na mocy założenia indukcyjnego mamy Parser nie mógł rozpoznać (nieznana funkcja „\sat”): {\displaystyle \sat{\mathfrak A_\Gamma}\varrho\psi} . Zatem Parser nie mógł rozpoznać (nieznana funkcja „\sat”): {\displaystyle \sat{\mathfrak A_\Gamma}\varrho\vartheta} i korzystając ponownie z założenia indukcyjnego otrzymujemy . Dalej na mocy aksjomatu (A1) i reguły (MP) otrzymujemy Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \Gamma\vdash_H\psi^*\arr\vartheta^*} . Jeśli natomiast , to jak wynika z (12) zbiór jest sprzeczny. Stąd i z twierdzenia o dedukcji (Twierdzenie 7.2) dostajemy ponownie Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \Gamma\vdash_H\psi^*\arr\vartheta^*} . Dowód implikacji odwrotnej, tzn. że Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \Gamma\vdash_H\psi^*\arr\vartheta^*} pociąga Parser nie mógł rozpoznać (nieznana funkcja „\sat”): {\displaystyle \sat{\mathfrak A_\Gamma}\varrho\var\varphi} pozostawiamy Czytlnikowi do uzupełnienia.

Na koniec rozważmy przypadek, gdy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest postaci . Załóżmy, że Parser nie mógł rozpoznać (nieznana funkcja „\sat”): {\displaystyle \sat{\mathfrak A_\Gamma}\varrho\var\varphi} . Niech oznacza formułę . Formuła ma co najwyżej jedną zmienną wolną . Jeśli , to z -nasycenia istnieje taka stała , że . Zatem na mocy założenia indukcyjnego otrzymujemy , co daje sprzeczność z naszym założeniem Parser nie mógł rozpoznać (nieznana funkcja „\sat”): {\displaystyle \sat{\mathfrak A_\Gamma}\varrho\var\varphi} . Tak więc musi być . Na odwrót, załóżmy, że i niech będzie dowolną stałą. Z aksjomatu (A6) dostajemy i na mocy założenia indukcyjnego dostajemy Parser nie mógł rozpoznać (nieznana funkcja „\sa”): {\displaystyle \sa\prooftree \mathfrak A_\Gamma \justifies \varrho^{[d]_\sim}_y \using \textrm{(W)}\endprooftree\psi} . Ponieważ jest dowolne, to powyższe spełnianie dowodzi Parser nie mógł rozpoznać (nieznana funkcja „\sat”): {\displaystyle \sat{\mathfrak A_\Gamma}\varrho\var\varphi} . Tym samym dowód twierdzenia jest zakończony.

End of proof.gif

Na zakończenie udowodnimy zapowiedziane wcześniej "silne" twierdzenie o pełności dla systemu . Jest ono prostym wnioskiem z twierdzenia o istnieniu modelu.

Twierdzenie 7.8 ("Silne" twierdzenie o pełności)

Dla dowolnego zbioru formuł i dla dowolnej formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} , jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\models\var\varphi} , to Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\vdash_H\var\varphi} . W szczególności, jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest tautologią języka pierwszego rzędu, to Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \vdash_H\var\varphi} .

Dowód

Załóżmy, że Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\not\vdash\var\varphi} . Niech będzie nieskończonym przeliczalnym zbiorem stałych, rozłącznym z sygnaturą . Ustawmy zmienne indywiduowe w ciąg . Dla dowolnej formuły nad sygnaturą niech oznacza zdanie nad sygnaturą otrzymane z przez zastąpienie każdej zmiennej wolno występującej w stałą . Niech .

Twierdzimy, że zbiór zdań Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta^*\cup\{\neg\var\varphi^*\}} jest zbiorem niesprzecznym. Załóżmy przeciwnie, że

Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta^*\cup\{\neg\var\varphi^*\}\vdash\bot.}

Wówczas dla pewnego skończonego podzbioru mamy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta_0^*\cup\{\neg\var\varphi^*\}\vdash\bot} . Z twierdzenia o dedukcji dostajemy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta_0^*\vdash\neg\neg\var\varphi^*} i na mocy aksjomatu (A3) mamy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta_0^*\vdash\var\varphi^*} Przyjmijmy, że . Stosując razy twierdzenie o dedukcji, dostajemy

Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \vdash\psi_1^*\arr(\cdots\arr(\psi_n^*\arr\var\varphi^*)\cdots)} .

Zastępując w powyższym dowodzie stałe nowymi, nigdzie w tym dowodzie nie pojawiającymi się zmiennymi , następnie generalizując (por. Twierdzenie 7.4) i podstawiając na miejsce zmiennych związanych (por. aksjomat (A6)) zmienne dostajemy w stosownej formule.

Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \vdash\psi_1\arr(\cdots\arr(\psi_n\arr\var\varphi)\cdots)} ,

czyli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta_0\vdash\var\varphi} , a co za tym idzie również Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle e\var\varphi} , wbrew założeniu. Tak więc zbiór Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta^*\cup\{\neg\var\varphi^*\}} jest niesprzeczny.

Z twierdzenia o istnieniu modelu wynika, że Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta^*\cup\{\neg\var\varphi^*\}} ma model. Istnieje więc -struk\-tu\-ra taka, że oraz Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \mathfrak A\not\models\var\varphi^*} . Niech Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \varrho:X\arr A} będzie wartościowaniem, które każdej zmiennej przypisuje wartość . Na mocy Twierdzenia 7.7 mamy wówczas Parser nie mógł rozpoznać (nieznana funkcja „\sat”): {\displaystyle \sat\mathfrak A\varrho\psi} , dla każdej formuły oraz Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle (\mathfrak A,\varrho)\not\models\var\varphi} . Dowodzi to Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\not\models\var\varphi} .

End of proof.gif