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

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 niech$C\subseteq {\mathrm{\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$.

Lemat 7.6 (o nasyceniu)

Niech $C$ będzie nieskończonym zbiorem, rozłącznym z sygnaturą $\mathrm{\Sigma }$ oraz takim, że $|\mathrm{\Sigma }|\le |C|$. Niech $\mathrm{\Delta }$ będzienie sprzecznym zbiorem zdań nad $\mathrm{\Sigma }$. Istnieje zbiór zdań $\mathrm{\Gamma }$ nad sygnaturą $\mathrm{\Sigma }(C)$ taki, że $\mathrm{\Delta }\subseteq \mathrm{\Gamma }$ oraz $\mathrm{\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 $\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 pozostawimy Czytelnikowi 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 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:

• ${\mathrm{\Gamma }}_n$ zawiera skończenie wiele stałych z $C$.
• $\mathrm{\Delta }\subseteq {\mathrm{\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)} , 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 ${\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ędzie stałą nie występującą w ${\mathrm{\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)\}} jestzbiorem niesprzecznym. Załóżmy przeciwnie, że

${\mathrm{\Gamma }}_n+1{⊢}_H\mathrm{\perp }$

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 ${\mathrm{\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 ${\mathrm{\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\in ̸FV({\mathrm{\Gamma }}_n)$. Na mocyTwierdzenia 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 ${\mathrm{\Gamma }}_{n+1}.\Rightarrow$ kończy konstrukcję zbiorów ${\mathrm{\Gamma }}_n$ oraz stałych $c_n$.

Niech

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

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, ż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 ${\mathrm{\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 $\mathrm{\Gamma }$.

Konstrukcja modelu ze stałych

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$. Musimy określić interpretację symboli operacji i relacji z $\mathrm{\Sigma }$. Dla przykładu załóżmy, że $f\in {\mathrm{\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 </math> Dla pokazania, że $f^{{\mathfrak{𝔄}}_{\mathrm{\Gamma }}}$ jest dobrze określoną funkcją musimy sprawdzić, że: Parser nie mógł rozpoznać (błąd składni): {\displaystyle \mbox{Dla dowolnych } c_1,c_2\in C \mbox{ istnieje } d\in C \mbox{ takie, że } \Gamma\vdash_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\,\neg f(c_1,c_2)=xParser nie mógł rozpoznać (błąd składni): {\displaystyle . Istotnie, załóżmy } \forall x\,\neg f(c_1,c_2)=xParser nie mógł rozpoznać (błąd składni): {\displaystyle . Wówczas z aksjomatu (A6) dostajemy } \neg f(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 postaci aksjomatu (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. Dla przykł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 musimy pokazać, że jeśli $c_1\sim {c_1}^{\prime }$ oraz $c_2\sim {c_2}^{\prime }$, to

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

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

Twierdzenie

Każdy niesprzeczny zbiór zdań nad dowolną sygnaturą $\mathrm{\Sigma }$ ma model, którego moc nie przekracza $\max \{{\mathrm{\aleph }}_0,|\mathrm{\Sigma }|\}$.% Dokładniej, dla struktury ${\mathfrak{𝔄}}_{\mathrm{\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)sbseteq\{x_1,\ldots,x_n\}} i dla dowolnego wartościowania $\varrho$ takiego, że $\varrho (x_i)=[c_i{]}_{\sim }$, dla $i=1,\dots ,n$ mamy \sat{\mathfrak A_\Gamma}\varrho\var\varphi\WTW\Gamma\vdash_H \var\varphi(c_1/x_1,\ldots,c_n/x_n). \end{equation}

{{dowod|eq-zwart-4|

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

Najpierw zanotujmy następującą ważną własność zbioru $\mathrm{\Gamma }$. Dla dowolnego zdania Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} , \mbox{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.} \end{equation} Dla dowodu ([[#eq-zwar-0}) 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ż </math>\Gamma\not\vdash_H \forall x\,\psi(x)Parser nie mógł rozpoznać (błąd składni): {\displaystyle . Zatem dla pewnej stałej } c\in C</math> zachodzi $\mathrm{\Gamma }{⊢}_H\mathrm{\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 $\mathrm{\Gamma }$ wynika, że Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Gamma\cup\{\var\varphi\}} musi być zbiorem sprzecznym. \Rightarrow dowodzi (#eq-zwar-0).

Zauważmy, że z własności (#eq-zwart-3) wynika pierwsza część twierdzenia, bowiem mamy wówczas ${\mathfrak{𝔄}}_{\mathrm{\Gamma }}\models \mathrm{\Gamma }$. Własność (#eq-zwart-3) 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 \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, \end{equation} gdzie $FV(t)sbseteq\{x_1,\dots ,x_n\}$ oraz $v(x_i)=[c_i{]}_{\sim }$, dla $i=1,\dots ,n$. Dowód (#eq-zwart-4) przeprowadzamy przez rutynową indukcję ze względu na budowę termu $t$. Szczegóły pozostawiamy Czytelnikowi.

Powracamy do dowodu (#eq-zwart-3). Jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest formułą </math>{t}_1={t}_2$,to$\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</math> 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 (#eq-zwart-4) jest to równoważne temu, że dla pewnego $d\in C$ zachodzi $\mathrm{\Gamma }{⊢}_H{t}_1(c_1/x_1,\dots ,c_n/x_n)=d$ oraz $\mathrm{\Gamma }{⊢}_H{t}_2(c_1/x_1,\dots ,c_n/x_n)=d$. Ostatnia własność jest równoważna (na mocy $C$-nasycenia zbioru $\mathrm{\Gamma }$) własności </math>\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)</math>.

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,\dots ,c_n/x_n)$ oraz niech ${\vartheta }^{*}$ oznacza formułę $\vartheta (c_1/x_1,\dots ,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 $\mathrm{\Gamma }{⊢}_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 $\mathrm{\Gamma }{⊢}_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 $\mathrm{\Gamma }{⊢}_H{\psi }^{*}$, to jak wynika z (#eq-zwar-0) zbiór $\mathrm{\Gamma }\cup \{{\psi }^{*}\}$ jest sprzeczny. Stąd $\mathrm{\Gamma }\cup \{{\psi }^{*}\}{⊢}_H{\vartheta }^{*}$ i z twierdzenia o dedukcji (Twierdzenie #tw-ded-pier) dostajemy ponownie Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \Gamma\vdash_H\psi^*\arr\vartheta^*} . Dowód \rightarrowlikacji 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 </math>\var\varphi$jestpostaci$\forall y\ \psi(y)</math>. 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,\dots ,c_n/x_n)$. Formuła ${\psi }^{*}$ ma co najwyżej jedną zmienną wolną $y$. Jeśli $\mathrm{\Gamma }{⊢}_H\mathrm{\forall }y{\psi }^{*}$, to z $C$-nasycenia $\mathrm{\Gamma }$ istnieje taka stała $d\in C$, że $\mathrm{\Gamma }{⊢}_H\mathrm{\neg }{\psi }^{*}(d/y)$. Zatem na mocy założenia indukcyjnego otrzymujemy $({\mathfrak{𝔄}}_{\mathrm{\Gamma }},{\varrho }_y^{[d{]}_{\sim }})\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ć $\mathrm{\Gamma }{⊢}_H\mathrm{\forall }y{\psi }^{*}$. Na odwrót, załóżmy, że $\mathrm{\Gamma }{⊢}_H\mathrm{\forall }y{\psi }^{*}$ i niech $d\in C$ będzie dowolną stałą. Z aksjomatu (A6) dostajemy $\mathrm{\Gamma }{⊢}_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ńczenieudowodnimy zapowiedziane wcześniej ,,silne twierdzenie o pełności dla systemu ${⊢}_H$. Jest ono prostym wnioskiem z twierdzenia o istnieniu modelu.

Twierdzenie

Dla dowolnego zbioru formuł $\mathrm{\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 e_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} .

<span id="\ \psi\in\Delta\}</math>.

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 \[\Delta^*\cup\{\neg\var\varphi^*\}\vdash\bot.\] Wówczas dla pewnego skończonego podzbioru ${\mathrm{\Delta }}_{0}sbseteq\mathrm{\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 \mbox{${\mathrm{\Delta }}_0=\{{\psi }_1,\dots ,{\psi }_n\}$}. Stosując $n$ razy twierdzenie o dedukcji, dostajemy \[\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 #tw-gen) i podstawiając na miejsce zmiennych związanych $z_i$ (por. aksjomat (A6)) zmienne $x_i$ dostajemy\footnote{Zauważmy, że zmienna $x_i$ jest dopuszczalna dla $z_i$ w stosownej formule.} \[\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 $\mathrm{\Sigma }(C)$-struk\-tu\-ra $\mathfrak{𝔄}$ taka, że $\mathfrak{𝔄}\models {\mathrm{\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{𝔄}}$. Na mocy Twierdzenia #tw-pier-4 mamy wówczas Parser nie mógł rozpoznać (nieznana funkcja „\sat”): {\displaystyle \sat\mathfrak A\varrho\psi} , dla każdej formuły $\psi \in \mathrm{\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} . " style="font-variant:small-caps">Dowód

{{{3}}}

sbsection*{Ćwiczenia}\begin{small}

1. Rozpatrzmy system ${⊢}_h$, którego aksjomatami są formuły

postaci (A1--A9), a nie dowolne generalizacje takich formuł. Regułami wnioskowania w ${⊢}_h$ niech będą (MP) oraz reguła generalizacji:\/

Parser nie mógł rozpoznać (nieznana funkcja „\prooftree”): {\displaystyle \prooftree \var\varphi\justifies \forall x\,\var\varphi\endprooftree}

Udowodnić, że twierdzenia systemów ${⊢}_h$ i ${⊢}_H$ są takie same, ale z Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Gamma\vdash_h\var\varphi} nie wynika Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Gamma\models\var\varphi} .

1. Udowodnić twierdzenie o pełności dla nieprzeliczalnych sygnatur.
2. System naturalnej dedukcji dla logiki pierwszego rzędu można otrzymać

przez dodanie do systemu Parser nie mógł rozpoznać (błąd składni): {\displaystyle &nbsp;\vdash_N} nastepujących reguł:

</math>\prooftree{\Gamma\vdash\var\varphi(y/x)}\justifies

{\Gamma\vdash\forall {x}\ciut \var\varphi}\using{(\forall\mbox{\rm-intro})} \endprooftree \hspace{3cm} \prooftree{\Gamma\vdash\forall {x}\ciut \var\varphi}\justifies

{\Gamma\vdash\var\varphi(t/x)}\using{(\forall\mbox{\rm-elim})}\endprooftree</math> </math>\prooftree{\Gamma\vdash\var\varphi(t/x)}\justifies

{\Gamma\vdash\exists {x}\ciut \var\varphi}\using{(\exists\mbox{\rm-intro})} \endprooftree \hspace{2cm} \prooftree{\Gamma\vdash\exists {x}\ciut \var\varphi\quad \Gamma,\var\varphi(y/x)\vdash\psi} \justifies

{\Gamma\vdash\psi}\using{(\exists\mbox{\rm-elim})}\endprooftree</math>

przy czym regułę Parser nie mógł rozpoznać (błąd składni): {\displaystyle (\forall\mbox{\rm-intro})} wolno stosować tylko wtedy gdy Parser nie mógł rozpoznać (nieznana funkcja „\fv”): {\displaystyle {y}\not\in\fv{\forall {x}\ciut \var\varphi}} oraz $y$ nie jest wolne w żadnej z formuł ze zbioru $\mathrm{\Gamma }$. Natomiast reguła Parser nie mógł rozpoznać (błąd składni): {\displaystyle (\exists\mbox{\rm-intro})} używana jest przy zastrzeżeniu Parser nie mógł rozpoznać (nieznana funkcja „\fv”): {\displaystyle {y}\not\in\fv{\Gamma\cup\{\exists {x}\ciut \var\varphi\}\cup\{\psi\}}} . Udowodnić twierdzenie o pełności dla tego systemu.

1. Zaproponować reguły rachunku sekwentów dla logiki pierwszego rzędu.

\end{small}