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

Poniższy system dowodzenia dotyczy formuł pierwszego rzędu nad ustaloną sygnaturą $\mathrm{\Sigma }$, zbudowanych w oparciu o spójniki $\to$, $\perp$ oraz kwantyfikator $\mathrm{\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,\dots 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\to (x_2=y_2\to \cdots \to (x_n=y_n\to f(x_1,\dots ,x_n)=f(y_1,\dots ,y_n))\cdots )$, dla $f\in {\mathrm{\Sigma }}_n^F,n\ge 0$;
(A9) $x_1=y_1\to (x_2=y_2\to \cdots \to (x_n=y_n\to (r(x_1,\dots ,x_n)\to r(y_1,\dots ,y_n)))\cdots )$, dla $r\in {\mathrm{\Sigma }}_n^R,n\ge 1$.

Reguły dowodzenia

Parser nie mógł rozpoznać (nieznana funkcja „\WTW”): {\displaystyle f^{\mathfrak A_\Gamma}([c_1]_\sim,[c_2]_\sim)=[d]_\sim \WTW \Gamma\vdash_H}

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 $\mathrm{\Delta }$ wpowyższym systemie będziemy oznaczać przez $\mathrm{\Delta }{⊢}_H\phi$.Sam system, podobnie jak w przypadku rachunku zdań, będziemyoznaczać przez ${⊢}_H$. Nie powinno prowadzić to doniejednoznaczności. Zwróćmyuwagę, że system ${⊢}_H$ zależyod sygnatury $\mathrm{\Sigma }$. Tak więc mamy różne systemy dla różnychsygnatur. 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\to y=x)$.

1. $\mathrm{\forall }{x}_1\mathrm{\forall }{x}_2\mathrm{\forall }{y}_1\mathrm{\forall }{y}_2(x_1=y_1\to (x_2=y_2\to (x_1=x_2\to y_1=y_2)))$   (A9)
2. $x=y\to (x=x\to (x=x\to y=x))$     na mocy (A6) oraz(MP)
3. $x=x\to (x=y\to (x=x\to y=x))$    z (2), jest to instancja tautologii zdaniowej
4. $x=x$    (A7)
5. $x=y\to (x=x\to y=x)$    (MP(4,3))
6. $x=x\to (x=y\to y=x)$     z (5), jest to instancja tautologii zdaniowej
7. $x=x$   (A7)
8. $x=y\to y=x$   (MP(7,6))

Twierdzenie 7.2 (o dedukcji)

Dla dowolnego zbioru formuł $\mathrm{\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 analogicznegotwierdzenia 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 $\mathrm{\Delta }{⊢}_H\mathrm{\forall }x\psi$ oraz zmienna $y\in ̸FV(\mathrm{\forall }x\psi )$ jest dopuszczalna dla $x$ w $\psi$,to $\mathrm{\Delta }{⊢}_H\mathrm{\forall }y\psi (y/x)$.

Dowód

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

Podamy jeszcze jednoużyteczne twierdzenie. Mówi ono, że tzw. reguła generalizacji jest dopuszczalna w systemie ${⊢}_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\in ̸FV(\mathrm{\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 $\mathrm{\Delta }$. JeśliParser 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 $\mathrm{\Delta }{⊢}_H\psi$ w mniejszejliczbie kroków. Z założenia indukcyjnego otrzymujemyParser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\vdash_H\forall x\,(\psi\rightarrow\var\varphi)} oraz $\mathrm{\Delta }{⊢}_H\mathrm{\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 $\mathrm{\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ł $\mathrm{\Delta }$ (i napiszemy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\models\var\varphi} ), gdy dla każdej struktury $\mathfrak{𝔄}$ i dla każdego wartościowania $\varrho$ w $\mathfrak{𝔄}$ spełniającego wszystkie formuły ze zbioru $\mathrm{\Delta }$, mamyParser nie mógł rozpoznać (nieznana funkcja „\sat”): {\displaystyle \sat\mathfrak A\varrho\var\varphi} . Zwróćmy uwagę, że jeśli $\mathrm{\Delta }$ jestzbiorem zdań, to powyższa definicja jest równoważna następującej własności: każdy model dla $\mathrm{\Delta }$ jest modelem dla Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} . W ogólnym przypadku, gdy formuły z $\mathrm{\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\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ł $\mathrm{\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 $\mathrm{\Delta }$. Jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi\in\Delta} , to oczywiście mamyParser 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), tozachodzi Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \models\var\varphi} . Oczywiście reguła (MP) zachowujerelację 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 $\mathrm{\Delta }\models \psi$.

Twierdzenie o poprawności może być użyte do pokazania, że pewnew ynikania nie dają się wyprowadzić w systemie ${⊢}_H$. Przykładowo, zobaczmy, że $x=y{⊢}_H\mathrm{\forall }x(x=y)$. Istotnie, biorąc dwuelementową strukturę $\mathfrak{𝔄}$ orazwartościowanie, które "skleja" wartości zmiennych $x$ oraz $y$, dostajemy $x=y\models ̸\mathrm{\forall }x(x=y)$. Zatem z twierdzenia o poprawności wnioskujemy, że $x=y{⊢}_H\mathrm{\forall }x(x=y)$. Jest to również przykład na to, że system ${⊢}_H$ nie jest zamknięty ze względu na dowolne generalizacje, tzn. założenie $x\in ̸FV(\mathrm{\Delta })$ w twierdzeniu o generalizacji jest istotne.

Zachodzi również odwrotne twierdzenie doTwierdzenia 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 ${⊢}_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 $\mathrm{\Gamma }$ będzie zbiorem zdań pierwszego rzędu nad sygnaturą $\mathrm{\Sigma }$ oraz niechParser nie mógł rozpoznać (nieznana funkcja „\sbseteq”): {\displaystyle C\sbseteq\Sigma_0} będzie pewnym zbiorem stałych. Powiemy, że $\mathrm{\Gamma }$jest zbiorem $C$-nasyconym, gdy $\mathrm{\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 $\mathrm{\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 $\mathrm{\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 $\mathrm{\Gamma }{⊢}_H\mathrm{\exists }x\psi (x)$. Ponadto z warunku $C$-nasycenia $\mathrm{\Gamma }$ wynika istnienie stałej $c\in C$ takiej, żeParser 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 $\mathrm{\Gamma }{⊢}_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 $\mathrm{\Sigma }$ nazwiemy moc zbioru $(\bigcup _{n=0}^{\mathrm{\infty }}{\mathrm{\Sigma }}_n^F)\cup (\bigcup _{n=1}^{\mathrm{\infty }}{\mathrm{\Sigma }}_n^R)$. Moc sygnatury $\mathrm{\Sigma }$ będziemy oznaczać przez $|\mathrm{\Sigma }|$.

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

Niech $C$ będzie nieskończonym zbiorem, rozłącznym z sygnaturą $\mathrm{\Sigma }$ oraz takim, że $|\mathrm{\Sigma }|\le |C|$. Niech $\mathrm{\Delta }$ będzieniesprzecznym zbiorem zdań nad $\mathrm{\Sigma }$. Istnieje zbiór zdań $\mathrm{\Gamma }$ nadsygnaturą $\mathrm{\Sigma }(C)$ taki, że Parser nie mógł rozpoznać (nieznana funkcja „\Deltasbseteq”): {\displaystyle \Deltasbseteq\Gamma} oraz $\mathrm{\Gamma }$ jest$C$-nasycony. \end{lemat}

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

• ${\mathrm{\Gamma }}_n$ zawiera skończenie wiele stałych z $C$.
• Parser nie mógł rozpoznać (nieznana funkcja „\Deltasbseteq”): {\displaystyle \Deltasbseteq\Gamma_n} jest niesprzecznym zbiorem zdań nad$\mathrm{\Sigma }(C)$.
• Jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Gamma_n\not\vdash_H\forall x\,\var\varphi_n(x)} , toParser 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 ${\mathrm{\Gamma }}_0=\mathrm{\Delta }$. Jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Gamma_n\vdash_H\forall x\,\var\varphi_n(x)} ,to definiujemy ${\mathrm{\Gamma }}_{n+1}={\mathrm{\Gamma }}_n$ oraz $c_n=c_{*}$. Jeśli natomiastParser 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ędziestałą nie występującą w ${\mathrm{\Gamma }}_n$ ani w Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi_n} . Musimypokazać, że Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Gamma_{n+1}=\Gamma_n\cup\{\neg\var\varphi_n(c_n/x)\}} jestzbiorem 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) dostajemyParser 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 ${\mathrm{\Gamma }}_n$ ani w Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi_n} to możemy w dowodzie powyższego sekwentuzamienić 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 ${\mathrm{\Gamma }}_n$. Tak więc otrzymujemyParser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Gamma_n\vdash_H\var\varphi_n(z/x)} oraz $z\in ̸FV({\mathrm{\Gamma }}_n)$. Na mocyTwierdzenia #tw-gen o generalizacji dostajemyParser 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 #tw-alfa) dostajemyParser 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óbudowodniliśmy niesprzeczność zbioru ${\mathrm{\Gamma }}_{n+1}$. \Rightarrow kończy konstrukcję zbiorów ${\mathrm{\Gamma }}_n$ oraz stałych $c_n$.

Niech

Pokażemy, że $\mathrm{\Gamma }$ jest zbiorem $C$-nasyconym.Oczywiście $\mathrm{\Gamma }$ jako suma łańcucha zbiorów niesprzecznych jestrównież zbiorem niesprzecznym. Niech Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi(x)} będzie dowolnąformułą nad $\mathrm{\Sigma }(C)$ o jednej zmiennej wolnej i załóżmy, żeParser 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 </math>nParser nie mógł rozpoznać (błąd składni): {\displaystyle . Oczywiście mamy } \Gamma_n\not\vdash_H\forall x\,\var\varphi_n(x)</math> i z konstrukcji zbiorów ${\mathrm{\Gamma }}_n$ wynika,że </math>\Gamma_{n+1}\vdash_H \neg\var\varphi_n(c_n/x)</math>. Zatem Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Gamma\vdash_H \neg\var\varphi_n(c_n/x)} , codowodzi $C$-nasycenia zbioru $\mathrm{\Gamma }$.\end{dowod}

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

Zdefiniujemy strukturę ${\mathfrak{𝔄}}_{\mathrm{\Gamma }}$. Nośnikiem tej struktury jest zbiór ilorazowy $C/\sim$. Musimyokreślić interpretację symboli operacji i relacji z $\mathrm{\Sigma }$. Dlaprzykładu załóżmy, że $f\in {\mathrm{\Sigma }}_2^F$ jest symbolem operacjidwuargumentowej. Funkcję $f^{{\mathfrak{𝔄}}_{\mathrm{\Gamma }}}:(C/\sim {)}^2\to C/\sim$ definiujemy warunkiem

</math>Dla pokazania, że $f^{{\mathfrak{𝔄}}_{\mathrm{\Gamma }}}$ jest dobrze określoną funkcjąmusimy sprawdzić, że: $\text{Dla dowolnych }{c}_1,c_2\in C\text{ istnieje }d\in C\text{takie, że }\mathrm{\Gamma }{⊢}_{H}f(c_1,c_2)=d$ $\text{Jeśli }{c}_1\sim {c_1}^{\prime },c_2\sim {c_2}^{\prime }\text{ oraz }\mathrm{\Gamma }{⊢}_{H}f(c_1,c_2)=d\text{ i }\mathrm{\Gamma }{⊢}_{H}f({c_1}^{\prime },{c_2}^{\prime })=d^{\prime },\text{ to }d\sim d^{\prime }.$Własność (#eq-zwart-1) wynika z faktu, że zbiór $\mathrm{\Gamma }$ jest</math>CParser nie mógł rozpoznać (błąd składni): {\displaystyle -nasycony. Zauważmy najpierw, że } \Gamma\vdash_H\neg\forall x\,\negf(c_1,c_2)=xParser nie mógł rozpoznać (błąd składni): {\displaystyle . Istotnie, załóżmy } \forall x\,\negf(c_1,c_2)=xParser nie mógł rozpoznać (błąd składni): {\displaystyle . Wówczas z aksjomatu (A6) dostajemy } \negf(c_1,c_2)=f(c_1,c_2)</math>. Z drugiej strony, z aksjomatu (A7) i (A6)dostajemy $f(c_1,c_2)=f(c_1,c_2)$. Tak więc otrzymujemy $\mathrm{\perp }$, a więc$\mathrm{\Gamma }{⊢}_H\mathrm{\neg }\mathrm{\forall }x\mathrm{\neg }f(c_1,c_2)=x$. Zatem z$C$-nasycenia $\mathrm{\Gamma }$ wynika istnienie stałej $d\in C$ takiej, że$\mathrm{\Gamma }{⊢}_H\mathrm{\neg }\mathrm{\neg }f(c_1,c_2)=d$. Korzystając teraz z (A3)dostajemy $\mathrm{\Gamma }{⊢}_{H}f(c_1,c_2)=d$.

Własność (#eq-zwart-2) wynika natychmiast z następującej postaciaksjomatu (A8) (postać tę otrzymujemy z (A8) z pomocą aksjomatu (A6)) Parser nie mógł rozpoznać (nieznana funkcja „\WTW”): {\displaystyle ([c_1]_\sim,[c_2]_\sim)\in r^{\mathfrak A_\Gamma}\WTW \Gamma\vdash_H <!--%-->Interpretacja symboli relacji w <math>\mathfrak A_\Gamma} wygląda podobnie. Dlaprzykładu zdefiniujemy relację </math>r^{\mathfrak A_\Gamma}$dlasymbolu$r\in\Sigma_2^R</math>.

</math>W tym przypadku również musimy dowieść poprawności definicji(tzn. niezależności od wyboru reprezentantów). Czyli musimypokazać, że jeśli $c_1\sim {c_1}^{\prime }$ oraz $c_2\sim {c_2}^{\prime }$, to