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

Hilbertowski system dowodzenia

Poniższy system dowodzenia dotyczy formuł pierwszego rzędu nad ustaloną sygnaturą $\Sigma$, zbudowanych w oparciu o spójniki $\rightarrow$, $\perp$ oraz kwantyfikator $\forall$. 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 $x_{1},\ldots x_{n}$ 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 $\sigma$ jestdopuszczalny dla $x$ w Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} ;
(A7)   $x=x$;
(A8)   $x_{1}=y_{1}\rightarrow (x_{2}=y_{2}\rightarrow \cdots \rightarrow (x_{n}=y_{n}\rightarrow f(x_{1},\ldots ,x_{n})=f(y_{1},\ldots ,y_{n}))\cdots )$, dla
        $f\in \Sigma _{n}^{F},\ n\geq 0$;
(A9)   $x_{1}=y_{1}\rightarrow (x_{2}=y_{2}\rightarrow \cdots \rightarrow (x_{n}=y_{n}\rightarrow (r(x_{1},\ldots ,x_{n})\rightarrow r(y_{1},\ldots ,y_{n})))\cdots )$, dla
         $r\in \Sigma _{n}^{R},\ n\geq 1$.

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 $\Delta$ w powyższym systemie będziemy oznaczać przez $\Delta \vdash _{H}\varphi$. Sam system, podobnie jak w przypadku rachunku zdań, będziemy oznaczać przez $\vdash _{H}$. Nie powinno prowadzić to do niejednoznaczności. Zwróćmy uwagę, że system $\vdash _{H}$ zależy od sygnatury $\Sigma$. 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 $(x=y\rightarrow y=x)$.

1. $\forall x_{1}\forall x_{2}\forall y_{1}\forall y_{2}(x_{1}=y_{1}\rightarrow (x_{2}=y_{2}\rightarrow (x_{1}=x_{2}\rightarrow y_{1}=y_{2})))$   (A9)
2. $x=y\rightarrow (x=x\rightarrow (x=x\rightarrow y=x))$     na mocy (A6) oraz(MP)
3. $x=x\rightarrow (x=y\rightarrow (x=x\rightarrow y=x))$    z (2), jest to instancja tautologii zdaniowej
4. $x=x$    (A7)
5. $x=y\rightarrow (x=x\rightarrow y=x)$    (MP(4,3))
6. $x=x\rightarrow (x=y\rightarrow y=x)$     z (5), jest to instancja tautologii zdaniowej
7. $x=x$   (A7)
8. $x=y\rightarrow y=x$   (MP(7,6))

Twierdzenie 7.2 (o dedukcji)

Dla dowolnego zbioru formuł $\Delta$ 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).

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ść $\alpha$-konwersji.

Twierdzenie 7.3 (o $\alpha$-konwersji)

Jeśli $\Delta \vdash _{H}\forall x\,\psi$ oraz zmienna $y\not \in FV(\forall x\,\psi )$ jest dopuszczalna dla $x$ w $\psi$, to $\Delta \vdash _{H}\forall y\,\psi (y/x)$.

Dowód

Ponieważ $y\not \in FV(\forall x\,\psi )$, to na mocy (A5) mamy $\Delta \vdash _{H}\forall x\,\psi \rightarrow \forall y\forall x\,\psi$. Z drugiej strony mamy następującą wersję aksjomatu (A6), co łącznie z aksjomatem (A4) daje $\Delta \vdash _{H}\forall y\forall x\,\psi \rightarrow \forall y\,\psi (y/x)$. Tak więc zakładając $\Delta \vdash _{H}\forall x\,\psi$ i stosując(MP) do (7), a następnie do (8), dostajemy co kończy dowód.

Podamy jeszcze jedno użyteczne twierdzenie. Mówi ono, że tzw. reguła generalizacji jest dopuszczalna w systemie $\vdash _{H}$. 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 $x$, takiej że $x\not \in FV(\Delta )$, 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 $\Delta$. 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 $\psi$ mamy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\vdash_H\psi\rightarrow\var\varphi} oraz $\Delta \vdash _{H}\psi$ 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 $\Delta \vdash _{H}\forall x\,\psi$. 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 $\forall x\,\psi$ daje nam Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \forall x\,\var\varphi} .

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

Twierdzenie 7.5 (o poprawności)

Dla dowolnego zbioru formuł $\Delta$ 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 $\Delta$. 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 $\Delta \models \psi$.

Twierdzenie o poprawności może być użyte do pokazania, że pewne wynikania nie dają się wyprowadzić w systemie $\vdash _{H}$. Przykładowo, zobaczmy, że $x=y\not \vdash _{H}\forall x\,(x=y)$. Istotnie, biorąc dwuelementową strukturę ${\mathfrak {A}}$ oraz wartościowanie, które "skleja" wartości zmiennych $x$ oraz $y$, dostajemy $x=y\not \models \forall x\,(x=y)$. Zatem z twierdzenia o poprawności wnioskujemy, że $x=y\not \vdash _{H}\forall x\,(x=y)$. Jest to również przykład na to, że system $\vdash _{H}$ nie jest zamknięty ze względu na dowolne generalizacje, tzn. założenie $x\not \in FV(\Delta )$ 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:$\wedge ,\ \vee$ i kwantyfikator egzystencjalny otrzymuje się z $\vdash _{H}$ 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 $\Gamma$ będzie zbiorem zdań pierwszego rzędu nad sygnaturą $\Sigma$ oraz niech $C\subseteq \Sigma _{0}$ będzie pewnym zbiorem stałych. Powiemy, że $\Gamma$jest zbiorem $C$-nasyconym, gdy $\Gamma$ 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 $x$, jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Gamma\not\vdash_H\forall x\,\var\varphi(x)} , to istnieje stała $c\in C$,taka że Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Gamma\vdash_H\neg\var\varphi(c/x)} .

Niech $\Gamma$ będzie $C$-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 $\neg \psi$, 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 $\Gamma \vdash _{H}\exists x\psi (x)$. Ponadto z warunku $C$-nasycenia $\Gamma$ wynika istnienie stałej $c\in C$ 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 $\Gamma \vdash _{H}\psi (c/x)$. Tak więc w tym przypadku $c$ jest "świadkiem" zachodzenia własności Parser nie mógł rozpoznać (nieznana funkcja „\existsx”): {\displaystyle \Gamma\vdash_H\existsx\ \psi(x)} .

Mocą sygnatury $\Sigma$ nazwiemy moc zbioru $(\bigcup _{n=0}^{\infty }\Sigma _{n}^{F})\cup (\bigcup _{n=1}^{\infty }\Sigma _{n}^{R})$. Moc sygnatury $\Sigma$ będziemy oznaczać przez $|\Sigma |$.

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

Lemat 7.6 (o nasyceniu)

Niech $C$ będzie nieskończonym zbiorem, rozłącznym z sygnaturą $\Sigma$ oraz takim, że $|\Sigma |\leq |C|$. Niech $\Delta$ będzie niesprzecznym zbiorem zdań nad $\Sigma$. Istnieje zbiór zdań $\Gamma$ nad sygnaturą $\Sigma (C)$ taki, że $\Delta \subseteq \Gamma$ oraz $\Gamma$ jest$C$-nasycony.

Dowód

Bez zmniejszenia ogólności możemy przyjąć, że istnieje zmienna $z$ nie występująca wolno w żadnej formule ze zbioru $\Delta$ (w przeciwnym przypadku możemy tak przenumerować zmienne, aby ten warunek był spełniony). Przedstawimy dowód dla przypadku, kiedy $\Sigma$ i $C$ są zbiorami przeliczalnymi. Dowód ogólnego przypadku pozostawimy Czytelnikowi jako ćwiczenie (należy zastosować indukcję pozaskończoną). Ustawmy zbiór wszystkich formuł nad $\Sigma (C)$ o jednej zmiennej wolnej $x$ 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:

• $\Gamma _{n}$ zawiera skończenie wiele stałych z $C$.
• $\Delta \subseteq \Gamma _{n}$ jest niesprzecznym zbiorem zdań nad $\Sigma (C)$.
• 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łą $c_{*}\in C$. Przyjmujemy $\Gamma _{0}=\Delta$. Jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Gamma_n\vdash_H\forall x\,\var\varphi_n(x)} , to definiujemy $\Gamma _{n+1}=\Gamma _{n}$ oraz $c_{n}=c_{*}$. 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 $c_{n}\in C$ będzie stałą nie występującą w $\Gamma _{n}$ 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

$\Gamma _{n}+1\vdash _{H}\bot$

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ż $c_{n}$ nie występuje w $\Gamma _{n}$ 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 $c_{n}$ przez nową zmienną $z$, która się w tym dowodzie nie pojawiła oraz nie występuje wolno w formułach z $\Gamma _{n}$. Tak więc otrzymujemy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Gamma_n\vdash_H\var\varphi_n(z/x)} oraz $z\not \in FV(\Gamma _{n})$. 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ż $x$ jest dopuszczalna dla $z$ 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 $\alpha$-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 $\Gamma _{n+1}.\Rightarrow$ kończy konstrukcję zbiorów $\Gamma _{n}$ oraz stałych $c_{n}$.

Niech

$\Gamma =\bigcup _{n\in N}\Gamma _{n}$

Pokażemy, że $\Gamma$ jest zbiorem $C$-nasyconym. Oczywiście $\Gamma$ 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 $\Sigma (C)$ 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 $n$. 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 $\Gamma _{n}$ 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 $C$-nasycenia zbioru $\Gamma$.

Konstrukcja modelu ze stałych

Niech $C\subseteq \Sigma _{0}$ będzie dowolnym zbiorem stałych i niech $\Gamma$ będzie dowolnym $C$-nasyconym zbiorem zdań nad $\Sigma$. W zbiorze $C$ definiujemy relację równoważności $\sim$:

$c_{1}\sim c_{2}$   wtedy i tylko wtedy, gdy $\Gamma \vdash _{H}c_{1}=c_{2}$

Zdefiniujemy strukturę ${\mathfrak {A}}_{\Gamma }$. Nośnikiem tej struktury jest zbiór ilorazowy $C/\sim$. Musimy określić interpretację symboli operacji i relacji z $\Sigma$. Dla przykładu załóżmy, że $f\in \Sigma _{2}^{F}$ 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

$f^{{\mathfrak {A}}_{\Gamma }}([c_{1}]_{\sim },[c_{2}]_{\sim })=[d]_{\sim }$ wtedy i tylko wtedy, gdy $\Gamma \vdash _{H}f(c_{1},c_{2})=d$

Dla pokazania, że $f^{{\mathfrak {A}}_{\Gamma }}$ jest dobrze określoną funkcją musimy sprawdzić, że:

Dla dowolnych $c_{1},c_{2}\in C$  istnieje  $d\in C$  takie, że  $\Gamma \vdash _{H}f(c_{1},c_{2})=d$    (9)

Jeśli  $c_{1}\sim c_{1}',\ c_{2}\sim c_{2}'$  oraz  $\Gamma \vdash _{H}f(c_{1},c_{2})=d$  i  $\Gamma \vdash _{H}f(c_{1}',c_{2}')=d'$  to  $d\sim d'.$    (10)

Własność (9) wynika z faktu, że zbiór $\Gamma$ jest $C$-nasycony. Zauważmy najpierw, że $\Gamma \vdash _{H}\neg \forall x\,\neg f(c_{1},c_{2})=x$. Istotnie, załóżmy $\forall x\,\neg f(c_{1},c_{2})=x$. Wówczas z aksjomatu (A6) dostajemy $\neg f(c_{1},c_{2})=f(c_{1},c_{2})$. Z drugiej strony, z aksjomatu (A7) i (A6) dostajemy $f(c_{1},c_{2})=f(c_{1},c_{2})$. Tak więc otrzymujemy $\bot$, a więc $\Gamma \vdash _{H}\neg \forall x\,\neg f(c_{1},c_{2})=x$. Zatem z $C$-nasycenia $\Gamma$ wynika istnienie stałej $d\in C$ takiej, że $\Gamma \vdash _{H}\neg \neg f(c_{1},c_{2})=d$. Korzystając teraz z (A3) dostajemy $\Gamma \vdash _{H}f(c_{1},c_{2})=d$.

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

$c_{1}=c'_{1}\rightarrow (c_{2}=c'_{2}\rightarrow f(c_{1},c_{2})=f(c'_{1},c'_{2})).$

Interpretacja symboli relacji w ${\mathfrak {A}}_{\Gamma }$ wygląda podobnie. Dla przykładu zdefiniujemy relację $r^{{\mathfrak {A}}_{\Gamma }}$ dla symbolu $r\in \Sigma _{2}^{R}$.

$([c_{1}]_{\sim },[c_{2}]_{\sim })\in r^{{\mathfrak {A}}_{\Gamma }}$ wtedy i tylko wtedy, gdy $\Gamma \vdash _{H}$

W tym przypadku również musimy dowieść poprawności definicji (tzn. niezależności od wyboru reprezentantów). Czyli musimy pokazać, że jeśli $c_{1}\sim c_{1}'$ oraz $c_{2}\sim c_{2}'$, to

$\Gamma \vdash _{H}r(c_{1},c_{2})$ wtedy i tylko wtedy, gdy $\Gamma \vdash _{H}r(c'_{1},c'_{2})$

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ą $\Sigma$ ma model, którego moc nie przekracza $\max\{\aleph _{0},|\Sigma |\}$. Dokładniej, dla struktury ${\mathfrak {A}}_{\Gamma }$ 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 $\varrho$ takiego, że $\varrho (x_{i})=[c_{i}]_{\sim }$ dla $i=1,\ldots ,n$ 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 $\Delta$ jest niesprzecznym zbiorem zdań. Niech $C$ będzie dowolnym nieskończonym zbiorem rozłącznym z $\Sigma$ i takim, że $|C|\geq |\Sigma |$. 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ą $\Sigma (C)$, który jest $C$-nasycony. Stosując lemat Kuratowskiego-Zorna dowodzimy, że istnieje maksymalny zbiór $\Gamma$ o powyższych własnościach. Niech $\Gamma$ będzie takim zbiorem. Dalsza część dowodu będzie przebiegała w odniesieniu do ustalonego zbioru $\Gamma$.

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

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 $C$-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 $\psi$ o jednej zmiennej wolnej, to mamy również $\Gamma \not \vdash _{H}\forall x\,\psi (x)$. Zatem dla pewnej stałej $c\in C$ zachodzi $\Gamma \vdash _{H}\neg \psi (c/x)$, 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 $\Gamma$ 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 ${\mathfrak {A}}_{\Gamma }\models \Gamma$. 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 $t$ i stałej $d\in C$ 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 $FV({t})sbseteq\{x_{1},\ldots ,x_{n}\}$ oraz $v(x_{i})=[c_{i}]_{\sim }$, dla $i=1,\ldots ,n$. Dowód (13) przeprowadzamy przez rutynową indukcję ze względu na budowę termu ${t}$. Szczegóły pozostawiamy Czytelnikowi.

Powracamy do dowodu (11). Jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest formułą ${t}_{1}={t}_{2}$, 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 $d\in C$ 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 $d\in C$ zachodzi $\Gamma \vdash _{H}{t}_{1}(c_{1}/x_{1},\ldots ,c_{n}/x_{n})=d$ oraz $\Gamma \vdash _{H}{t}_{2}(c_{1}/x_{1},\ldots ,c_{n}/x_{n})=d$. Ostatnia własność jest równoważna (na mocy $C$-nasycenia zbioru $\Gamma$) własności $\Gamma \vdash _{H}{t}_{1}(c_{1}/x_{1},\ldots ,c_{n}/x_{n})={t}_{2}(c_{1}/x_{1},\ldots ,c_{n}/x_{n})$.

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 $\psi ^{*}$ oznacza formułę $\psi (c_{1}/x_{1},\ldots ,c_{n}/x_{n})$ oraz niech $\vartheta ^{*}$ oznacza formułę $\vartheta (c_{1}/x_{1},\ldots ,c_{n}/x_{n})$. 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 $\Gamma \vdash _{H}\psi ^{*}$, 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 $\Gamma \vdash _{H}\vartheta ^{*}$. 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 $\Gamma \not \vdash _{H}\psi ^{*}$, to jak wynika z (12) zbiór $\Gamma \cup \{\psi ^{*}\}$ jest sprzeczny. Stąd $\Gamma \cup \{\psi ^{*}\}\vdash _{H}\vartheta ^{*}$ 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 $\forall y\psi (y)$. Załóżmy, że Parser nie mógł rozpoznać (nieznana funkcja „\sat”): {\displaystyle \sat{\mathfrak A_\Gamma}\varrho\var\varphi} . Niech $\psi ^{*}$ oznacza formułę $\psi (c_{1}/x_{1},\ldots ,c_{n}/x_{n})$. Formuła $\psi ^{*}$ ma co najwyżej jedną zmienną wolną $y$. Jeśli $\Gamma \not \vdash _{H}\forall y\ \psi ^{*}$, to z $C$-nasycenia $\Gamma$ istnieje taka stała $d\in C$, że $\Gamma \vdash _{H}\neg \psi ^{*}(d/y)$. Zatem na mocy założenia indukcyjnego otrzymujemy $({\mathfrak {A}}_{\Gamma },\varrho _{y}^{[d]_{\sim }})\not \models \psi$, 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ć $\Gamma \vdash _{H}\forall y\ \psi ^{*}$. Na odwrót, załóżmy, że $\Gamma \vdash _{H}\forall y\ \psi ^{*}$ i niech $d\in C$ będzie dowolną stałą. Z aksjomatu (A6) dostajemy $\Gamma \vdash _{H}\psi ^{*}(d/y)$ 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ż $d$ 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.

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

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

Dla dowolnego zbioru formuł $\Delta$ 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 $C=\{c_{0},c_{1},\ldots \}$ będzie nieskończonym przeliczalnym zbiorem stałych, rozłącznym z sygnaturą $\Sigma$. Ustawmy zmienne indywiduowe w ciąg $x_{0},x_{1},\ldots$. Dla dowolnej formuły $\psi$ nad sygnaturą $\Sigma$ niech $\psi ^{*}$ oznacza zdanie nad sygnaturą $\Sigma (C)$ otrzymane z $\psi$ przez zastąpienie każdej zmiennej $x_{n}$ wolno występującej w $\psi$ stałą $c_{n}$. Niech $\Delta ^{*}=\{\psi ^{*}\ |\psi \in \Delta \}$.

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 $\Delta _{0}sbseteq\Delta$ 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 $\Delta _{0}=\{\psi _{1},\ldots ,\psi _{n}\}$. Stosując $n$ 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 $c_{i}$ nowymi, nigdzie w tym dowodzie nie pojawiającymi się zmiennymi $z_{i}$, następnie generalizując (por. Twierdzenie 7.4) i podstawiając na miejsce zmiennych związanych $z_{i}$ (por. aksjomat (A6)) zmienne $x_{i}$ dostajemy $z_{i}$ 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 $\Sigma (C)$-struk\-tu\-ra ${\mathfrak {A}}$ taka, że ${\mathfrak {A}}\models \Delta ^{*}$ 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 $x_{i}$ przypisuje wartość $c_{i}^{\mathfrak {A}}$. 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 $\psi \in \Delta$ 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} .