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ędziemyrozumieć 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.

\vspace{.3cm}\noindentAksjomaty

Dowolne generalizacje formuł postaci:

(A1) Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi\arr(\psi\arr\var\varphi)} ;\\(A2) </math>(\var\varphi\arr(\psi\arr\vartheta))\arr((\var\varphi\arr\psi)\arr(\var\varphi\arr\vartheta))</math>;\\(A3) Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \neg\neg\var\varphi\arr\var\varphi} ;\\(A4) </math>\forall x(\var\varphi\arr\psi)\arr(\forall x\var\varphi\arr\forall x\psi)</math>;\\(A5) Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi\arr \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\arr \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) </math> x_1=y_1\arr(x_2=y_2\arr\cdots\arr(x_n=y_n\arr f(x_1,\ldots,x_n)=f(y_1,\ldots, y_n))\cdots)</math>, dla $f\in {\mathrm{\Sigma }}_n^F,n\ge 0$;\\(A9) </math> x_1=y_1\arr(x_2=y_2\arr\cdots\arr(x_n=y_n\arr(r(x_1,\ldots,x_n)\arr r(y_1,\ldots, y_n)))\cdots)</math>, dla $r\in {\mathrm{\Sigma }}_n^R,n\ge 1$.

\vspace{.3cm}\noindentReguł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&nbsp;przypadku rachunku zdań (por. Rozdział&nbsp;2).Możliwośćudowodnienia formuły <math>\var\varphi} ze zbioru hipotez $\mathrm{\Delta }$ wpowyższym systemie będziemy oznaczać przez Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle e_H\var\varphi} .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ń.

Pokażemy główne kroki dowodu formuły Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle (x=y\arr y=x)} .

1. </math>\forall x_1\forall x_2\forall y_1\forall y_2(x_1=y_1\arr(x_2=y_2\arr(x_1=x_2\arr y_1=y_2)))</math> \hspace{.5cm} (A9)
2. Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle x=y\arr(x=x\arr(x=x\arr y=x))} \hspace{.5cm} na mocy (A6) oraz(MP)
3. Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle x=x\arr(x=y\arr(x=x\arr y=x))} \hspace{.5cm} z (2), jest to instancja tautologii zdaniowej
4. $x=x$ \hspace{.5cm} (A7)
5. Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle x=y\arr(x=x\arr y=x)} \hspace{.5cm} (MP(4,3))
6. Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle x=x\arr(x=y\arr y=x)} \hspace{.5cm} z (5), jest to instancja tautologii zdaniowej
7. $x=x$ \hspace{.5cm} (A7)
8. Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle x=y\arr y=x} \hspace{.5cm} (MP(7,6))

\end{przyklad}

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 e_H\var\varphi\arr\psi} .\end{twierdzenie}

\begin{dowod}Dowód tego twierdzenia jest dokładnie taki sam jak analogicznegotwierdzenia dla rachunku zadań (por. Twierdzenie #tw-zad-1).\end{dowod}

Natępujące twierdzenie mówi, że wybór nazwy zmiennej związanejnie ma wpływu na dowodliwość formuły. Jest to tzw. własność{\em $\alpha$-konwersji}.

Jeśli $e_H\mathrm{\forall }x\psi$ oraz zmienna $y\in ̸FV(\mathrm{\forall }x\psi )$ jest dopuszczalna dla $x$ w $\psi$,to $e_H\mathrm{\forall }y\psi (y/x)$.\end{twierdzenie}

\begin{dowod}Ponieważ $y\in ̸FV(\mathrm{\forall }x\psi )$, to na mocy (A5) mamy

e_H \forall x\,\psi \arr \forall y\forall x\,\psi.\end{equation}Z drugiej strony mamy następującą wersję aksjomatu (A6)

co łącznie z aksjomatem (A4) daje

e_H\forall y\forall x\,\psi\arr\forall y\,\psi(y/x).\end{equation}Tak więc, zakładając $e_H\mathrm{\forall }x\psi$ i stosując(MP) do (#eq-pier6), a następnie do (#eq-pier7) dostajemy

co kończy dowód.\end{dowod}

Podamy jeszcze jednoużyteczne twierdzenie. Mówi ono, żetzw. {\em 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\}.}

Jeśli zachodzi Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle e_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 e_H\forall x\,\var\varphi} .\end{twierdzenie}

\begin{dowod}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 tejformuły jest też aksjomatem, więc teza zachodzi. Aby pokazać Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle e_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\mbox{Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle e_H\psi\arr\var\varphi} } oraz $e_H\psi$ w mniejszejliczbie kroków. Z założenia indukcyjnego otrzymujemyParser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle e_H\forall x\,(\psi\arr\var\varphi)} oraz $e_H\mathrm{\forall }x\psi$. Zatem stosując (MP) do Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \forall x\,(\psi\arr\var\varphi)} oraz do instancji Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \forall x(\psi\arr\var\varphi)\arr(\forall x\psi\arr\forall x\var\varphi)} aksjomatu (A4) otrzymujemy Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \forall x\psi\arr\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} .\end{dowod}

Powiemy, że formuła Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest {\em konsekwencją semantyczną}zbioru formuł $\mathrm{\Delta }$ (i napiszemy \mbox{Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\models\var\varphi} }), gdydla 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óćmyuwagę, że jeśli $\mathrm{\Delta }$ jestzbiorem zdań, to powyższa definicja jest równoważna następującejwł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$.

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

\begin{dowod}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śliParser 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\arr\psi} , to $\mathrm{\Delta }\models \psi$. \end{dowod}

Twierdzenie o poprawności może byćużyte do pokazania, że pewnewynikania 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ściwnioskujemy, że $x=y{⊢}_H\mathrm{\forall }x(x=y)$. Jest torównież przykład na to, że system ${⊢}_H$ nie jest zamknięty \zwn dowolne generalizacje, tzn. założenie $x\in ̸FV(\mathrm{\Delta })$ wtwierdzeniu o generalizacji jest istotne.

Zachodzi również odwrotne twierdzenie doTwierdzenia #tw-pier-1. Dowód tego twierdzenia jest celem niniejszego rozdziału.

System formalny dla formuł zawierających pozostałe spójniki:$\wedge ,\vee$ i kwantyfikatoregzystencjalny otrzymuje się z ${⊢}_H$ przez dodanie aksjomatów charakteryzujących te symbole:

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

Głównym narzędziem w dowodzie ,,silnego twierdzenia o pełności będzie tzw. {\em 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ędziezbiorem zdań pierwszego rzędu nad sygnaturą $\mathrm{\Sigma }$ oraz niech$Csbseteq{\mathrm{\Sigma }}_0$ będzie pewnym zbiorem stałych. Powiemy, że $\mathrm{\Gamma }$jest zbiorem {\em $C$-nasyconym}, gdy $\mathrm{\Gamma }$ jest zbioremniesprzecznym oraz dla dowolnej formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi(x)} o co najwyżej jednej zmiennejwolnej $x$, jeśliParser 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śliParser 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} jestpostaci </math>\neg\psiParser nie mógł rozpoznać (błąd składni): {\displaystyle , to wówczas } \Gamma\vdash_H\neg\forall x\\var\varphi(x)Parser nie mógł rozpoznać (błąd składni): {\displaystyle jest równoważne } \Gamma\vdash_H\exists x\\psi(x)</math>. Ponadto z warunku $C$-nasycenia $\mathrm{\Gamma }$ wynikaistnienie 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 mocyprawa podwójnego przeczenia) temu, że $\mathrm{\Gamma }{⊢}_H\psi (c/x)$. Tak więc wtym przypadku $c$ jest ,,świadkiem zachodzenia własności </math>\Gamma\vdash_H\existsx\ \psi(x)</math>.

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ę Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle f^{\mathfrak A_\Gamma}:(C/\!\!\sim)^2\arr 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