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

Pełność rachunku zdań

Zagadnienie pełności systemów formalnych jest jednym z centralnych problemów logiki. O ile poprawność systemu formalnego (zwana też adekwatnością) oznacza, że wszystkie twierdzenia systemu są prawdziwe względem przyjętej semantyki, to pełność jest własnością mówiącą o tym, że każda formuła prawdziwa daje się udowodnić w systemie. Jest wiele różnych dowodów twierdzenia o pełności dla rachunku zdań. My podamy elegancki dowód pochodzący od L. Kalmára. Dla udowodnienia nieco silniejszej wersji twierdzenia o pełności (Twierdzenie 6.7) wykorzystamy silne i bardzo pożyteczne Twierdzenie 6.5 zwane twierdzeniem o zwartości.

Lemat 6.1 (Kalmár)

Niech Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} będzie formułą zbudowaną przy użyciu $\to$ oraz $\mathrm{\perp }$, o zmiennych zawartych w zbiorze $\{q_1,\dots q_n\}$ i niech Parser nie mógł rozpoznać (błąd składni): {\displaystyle \varrho:\mbox{\small ZZ}\rightarrow\{0,1\}} będzie dowolnym wartościowaniem. Dla $i=1,\dots ,n$ definiujemy formuły:

Parser nie mógł rozpoznać (nieznana funkcja „\begin{cases}”): {\displaystyle q'_i = \begin{cases}q_i & \text{\ jeśli } \varrho(q_i)=1 \\\neg q_i & \text{\ jeśli } \varrho(q_i)=0\end{cases}}

Niech Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi'} będzie formułą identyczną z Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} , jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \models\var\varphi[\varrho]} , w przeciwnym razie niech Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi'} oznacza formułę Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \neg\var\varphi} . Wówczas $\{{q_1}^{\prime },\dots ,{q_n}^{\prime }\}{⊢}_H\psi$

Dowód

Dowód jest prowadzony przez indukcję ze względu na budowę formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} . Jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest zmienną $q_i$ to Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi'=q_i'} . Zatem trywialnie zachodzi Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \{q_1',\ldots,q_n'\}\vdash\var\varphi'} .

Jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest stałą $\mathrm{\perp }$, to Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi'=\neg\bot} i oczywiście dla dowolnego wyboru ${q_1}^{\prime },\dots ,{q_n}^{\prime }$ zachodzi

$\{q{\text{'}}_1,\dots ,q{\text{'}}_n\}{⊢}_H\mathrm{\neg }\mathrm{\perp }$.

Załóżmy teraz, że Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest postaci Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \psi\arr\vartheta} i rozważmy następujące przypadki.

(A) $\models ̸\psi [\varrho ]$.

Wówczas Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi'=\var\varphi} oraz ${\psi }^{\prime }=\mathrm{\neg }\psi$. Z założenia indukcyjnego mamy $\{{q_1}^{\prime },\dots ,{q_n}^{\prime }\}{⊢}_H\mathrm{\neg }\psi$. Zatem $\{{q_1}^{\prime },\dots ,{q_n}^{\prime }\},\psi {⊢}_H\mathrm{\perp }$. Z Lematu 5.4(2) mamy Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \{q_1',\ldots,q_n'\},\psi\vdash_H\bot\arr\vartheta} . Zatem, stosując (MP) dostajemy $\{{q_1}^{\prime },\dots ,{q_n}^{\prime }\},\psi {⊢}_H\vartheta$ i z twierdzenia o dedukcji

Parser nie mógł rozpoznać (nieznana funkcja „\varaphi”): {\displaystyle \{q'_1,\ldots,q'_n\}\vdash_H\psi\rightarrow\varaphi} .

(B) $\models \vartheta [\varrho ]$.

Wówczas Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi'=\var\varphi} , oraz ${\vartheta }^{\prime }=\vartheta$. Z założenia indukcyjnego mamy $\{{q_1}^{\prime },\dots ,{q_n}^{\prime }\}{⊢}_H\vartheta$. Zatem $\{{q_1}^{\prime },\dots ,{q_n}^{\prime }\},\psi {⊢}_H\vartheta$ i z twierdzenia o dedukcji dostajemy

Parser nie mógł rozpoznać (nieznana funkcja „\varaphi”): {\displaystyle \{q'_1,\ldots,q'_n\}\vdash_H\psi\rightarrow\varaphi} .

(C) $\models \psi [\varrho ]$ oraz $\models ̸\vartheta [\varrho ]$.

Wówczas Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi'=\neg\var\varphi.\ \psi'=\psi} oraz ${\vartheta }^{\prime }=\mathrm{\neg }\vartheta$. Z założenia indukcyjnego mamy

$\{q{\text{'}}_1,\dots ,q{\text{'}}_n\}{⊢}_H\psi$   oraz   $\{q{\text{'}}_1,\dots ,q{\text{'}}_n\}{⊢}_H\mathrm{\neg }\vartheta$

Z Lematu 5.4(1) mamy

$\{q{\text{'}}_1,\dots ,{q_n}^{\prime }\}{⊢}_H$

Stosując teraz dwukrotnie (MP) dostajemy

$\{q{\text{'}}_1,\dots ,q{\text{'}}_n\}$

To kończy dowód lematu.

Lemat 6.2

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

Dowód

Jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta,\var\varphi\vdash_H \psi} to na mocy twierdzenia o dedukcji mamy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \vdash_H \var\varphi\arr\psi} . Podobnie dostajemy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \vdash_H\neg\var\varphi\arr\psi} . Stosując Lemat 5.4(3), oraz dwukrotnie regułę odrywania dostajemy ${⊢}_H\psi$.

Lemat Kalmára odgrywa kluczową rolę w dowodzie poniższego twierdzenia o pełności.

Twierdzenie 6.3 (o pełności dla ${⊢}_H$)

Jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest tautologią zbudowaną przyużyciu $\to$ oraz $\mathrm{\perp }$, 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 \var\varphi} jest tautologią. Niech $\{q_1,\dots ,q_n\}$ będą wszystkimi zmiennymi występującymi w Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} . Dla dowolnej liczby $0\le m\le n$ nazwiemy $m$-zbiorem każdy zbiór formuł $\{{q_1}^{\prime },\dots ,{q_m}^{\prime }\}$, gdzie ${q_i}^{\prime }$ jest albo $q_i$ lub $\mathrm{\neg }{q}_i$. Zauważmy, że $0$-zbiór jest pusty.

Udowodnimy następującą własność: dla każdego $m$ spełniającego $0\le m\le n$, jeśli $\mathrm{\Delta }$ jest $m$-zbiorem, to Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\vdash_H\var\varphi} .

Zauważmy, że biorąc $m=0$ w (2) dostajemy tezę twierdzenia. Dowód (2) przeprowadzimy przez indukcję ze względu na $m$ w zbiorze $\{0,\dots ,n\}$uporządkowanym relacją ${\le }^{-1}$. Dla $m=n$ własność (2) wynika z Lematu 6.1 oraz z faktu, że Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest tautologią. Załóżmy, że (2) zachodzi dla pewnego $0<m<n$ i niech $\mathrm{\Delta }$ będzie dowolnym $(m-1)$-zbiorem. Z założenia indukcyjnego dostajemy

Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta,q_{m}\vdash_H\var\varphi} oraz

Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta,\neg q_{m}\vdash_H\var\varphi} .

Zatem na mocy Lematu 6.2 dostajemy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \vdash_H\var\varphi} . To kończy dowód (2) i tym samym dowód twierdzenia o pełności.

Korzystając z Lematu 5.6 natychmiast dostajemy twierdzenie o pełności dla systemu ${⊢}_{H^{+}}$ ze wszystkimi spójnikami zdaniowymi.

Twierdzenie 6.4 (o pełności ${⊢}_{H^{+}}$)

Jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest tautologią, to Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \vdash_{H^+}\var\varphi} .

Dowód

Ponieważ Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \vdash_{H^+}\var\varphi\arr\tilde{\var\varphi}} , więc z twierdzenia o poprawności wynika, że Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \models\var\varphi\arr\tilde{\var\varphi}} . A zatem Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \tilde{\var\varphi}} jest tautologią. Z twierdzenia o pełności dla systemu ${⊢}_H$ dostajemy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \vdash_H\tilde{\var\varphi}} . Stąd Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \vdash_{H^+}\tilde{\var\varphi}} i ponieważ Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \vdash_{H^+}\tilde{\var\varphi}\arr\var\varphi} (por. Lemat 5.6) więc stosując (MP) dostajemy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \vdash_{H^+}\tilde{\var\varphi}}

Elementy teorii modeli

Powiemy, że zbiór formuł $\mathrm{\Delta }$ jest spełnialny gdy istnieje wartościowanie Parser nie mógł rozpoznać (błąd składni): {\displaystyle \varrho:\mbox{\small ZZ}\arr \{0,1\}} spełniające wszystkie formuły ze zbioru $\mathrm{\Delta }$.

Twierdzenie 6.5

Zbiór formuł $\mathrm{\Delta }$ jest spełnialny wtedy i tylko wtedy, gdy każdy skończony podzbiór zbioru $\mathrm{\Delta }$ jest spełnialny.

Dowód

Powiemy, że zbiór $\mathrm{\Delta }$ jest skończenie spełnialny, gdy każdy skończony podzbiór zbioru $\mathrm{\Delta }$ jest spełnialny.

Szkic dowodu twierdzenia o zwartości wygląda następująco. Bez zmniejszenia ogólności możemy przyjąć, że wszystkie rozważane formuły są zbudowane przyużyciu jedynie spójników $\to$ oraz $\mathrm{\perp }$. Używając lematu Kuratowskiego-Zorna pokazujemy najpierw, że istnieje maksymalny skończenie spełnialny zbiór formuł $\mathrm{\Gamma }$ zawierający $\mathrm{\Delta }$. Oczywiście mamy

$\mathrm{\perp }\in ̸\mathrm{\Gamma }.$

Ponadto, dla dowolnej formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} mamy jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi\not\in\Gamma} , to math>\neg\var\varphi\in\Gamma</math>.

Istotnie, jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} oraz Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \neg\var\varphi} nie należą do $\mathrm{\Gamma }$, to istnieją skończone zbiory $X,Y\subseteq \mathrm{\Gamma }$, takie że Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle X\cup\{\var\varphi\}} oraz Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle Y\cup\{\neg\var\varphi\}} nie są spełnialne. Wynika stąd, że zbiory wartościowań spełniających $X$ oraz $Y$ są rozłączne. Tak więc $X\cup Y$ nie jest spełnialny, a otrzymana sprzeczność dowodzi (4).

Zatem dla dowolnych formuł Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi,\psi} ,

Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle (\var\varphi\rightarrow\psi)\in\Gamma \hspace{.5cm}} wtedy i tylko wtedy, gdy Parser nie mógł rozpoznać (błąd składni): {\displaystyle \hspace{.5cm} \var\varphi\not\in\Gamma} lub $\psi \in \mathrm{\Gamma }.$

Rzeczywiście, jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle (\var\varphi\rightarrow\psi)} i Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} należą do $\mathrm{\Gamma }$ oraz $\psi \in ̸\mathrm{\Gamma }$, to $\mathrm{\neg }\psi \in \mathrm{\Gamma }$ na mocy (4). Wówczas niespełnialny zbiór Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \{(\var\varphi\rightarrow\psi),\var\varphi,\neg\psi\}} jest podzbiorem $\mathrm{\Gamma }$ co dowodzi dowodzi z lewej do prawej w (5). Na odwrót, jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle (\var\varphi\arr\psi)\not\in\Gamma} , to na mocy (4) mamy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \neg(\var\varphi\rightarrow\psi)\in\Gamma} . Jeśli teraz $\psi \in \mathrm{\Gamma }$ to niespełnialny zbiór Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \{\neg(\var\varphi\rightarrow\psi), \psi\}} jest podzbiorem $\mathrm{\Gamma }$. Podobnie, jeśli $\phi \in ̸\mathrm{\Gamma }$, to $\mathrm{\neg }\phi \in \mathrm{\Gamma }$, więc Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \{\neg(\var\varphi\rightarrow\psi), \neg\var\varphi\}\subseteq\Gamma} , co kończy dowód (5).

Teraz możemy zdefiniować wartościowanie Parser nie mógł rozpoznać (błąd składni): {\displaystyle \varrho:\mbox{\small ZZ}\rightarrow \{0,1\}} tak, że dla dowolnej zmiennej Parser nie mógł rozpoznać (błąd składni): {\displaystyle p\in \mbox{\small ZZ}} warunki $\varrho (p)=1$ i $p\in \mathrm{\Gamma }$ są równoważne. Z następującej własności wynika, że $\varrho$ spełnia wszystkie formuły ze zbioru $\mathrm{\Gamma }$, a zatem $\mathrm{\Delta }$ jest zbiorem spełnialnym.

Dla dowolnej formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} , Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \models\var\varphi[\varrho] \hspace{.5cm} \mbox{ wtedy i tylko wtedy, gdy } \hspace{.5cm} \var\varphi\in \Gamma} .

Dowód (6) przeprowadzamy przez indukcję ze względu na budowę formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} . Własności (3)używamy w przypadku gdy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest $\mathrm{\perp }$, a własności (5) w przypadku, gdy zewnętrznym spójnikiem Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest $\to$.

Przykład 6.6

Podamy przykład zastosowania twierdzenia o zwartości. Pokażemy, że jeśli nieskończonej mapy (o przeliczalnej liczbie krajów) nie da się pokolorować przy pomocy $k$ kolorów, to istnieje skończony fragment tej mapy, którego też nie da się pokolorować przy pomocy $k$ kolorów. Niech $I$ będzie zbiorem krajów tej mapy. Rozważmy zmienne zdaniowe $p_{i,j}$, gdzie $i\in I$ oraz $j<k$. Wartościowania będą odpowiadać kolorowaniom mapy. Intencją jest to, aby wartościowanie przypisywało zmiennej $p_{i,j}$ wartość $1$ wtedy i tylko wtedy, gdy kraj $i$ ma na mapie kolor $j$. Poniższe formuły przedstawiają podstawowe warunki dotyczące kolorowania.

Każdy kraj ma jakiś kolor: dla każdego $i\in I$ wyraża to formuła

$p_{i,0}\vee p_{i,1}\vee \dots \vee p_{i,k-1}$.

Każdy kraj ma co najwyżej jeden kolor: dla każdego $i\in I$, oraz każdych $i,j<k$, jeśli $j\ne j^{\prime }$ to mamy formułę

$\mathrm{\neg }(p_{i,j}\wedge p_{i,j^{\prime }})$.

Każde dwa sąsiadujące kraje mają różne kolory: dla $i,i^{\prime }\in I$ takich, że $i$ oraz $i^{\prime }$ sąsiadują oraz dla każdego $j<k$ rozważmy formułę

$\mathrm{\neg }(p_{i,j}\wedge p_{i^{\prime },j})$.

Niech $\mathrm{\Delta }$ będzie zbiorem wszystkich formuł przedstawionych wyżej. Łatwo jest zauważyć, że $\mathrm{\Delta }$ jest spełnialny wtedy i tylko wtedy, gdy mapę da się pokolorować $k$ kolorami. Zatem jeśli mapy nie da się pokolorować $k$ kolorami, to $\mathrm{\Delta }$ nie jest spełnialny i z twierdzenia o zwartości wynika, że istnieje skończony podzbiór ${\mathrm{\Delta }}_0$, który nie jest spełnialny. Wówczas fragmentu mapy zawierającego kraje wymienione w indeksach zmiennych występujących w formułach z ${\mathrm{\Delta }}_0$ nie da się pokolorować przy pomocy $k$ kolorów.

Jako wniosek z twierdzenia o zwartości otrzymujemy następujące wzmocnienie twierdzenia o pełności (por. Twierdzenie 6.4).

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

Dla dowolnego zbioru formuł $\mathrm{\Delta }$ oraz 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 \var\varphi} jest semantyczną konsekwencją zbioru $\mathrm{\Delta }$, to Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\vdash_{H^+}\var\varphi} .

Dowód

Jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\models\var\varphi} to zbiór Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\cup\{\neg\var\varphi\}} nie jest spełnialny. Na mocy twierdzenia o zwartości istnieje skończony podzbiór ${\mathrm{\Delta }}_0\subseteq \mathrm{\Delta }$ taki, że Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta_0\cup\{\neg\var\varphi\}} nie jest spełnialny. Zatem Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta_0\models\var\varphi} . Tak więc jeśli ${\mathrm{\Delta }}_0=\{{\psi }_1,\dots ,{\psi }_n\}$ to oczywiście formuła Parser nie mógł rozpoznać (nieznana funkcja „\righrarrow”): {\displaystyle \psi_1\rightarrow(\psi_2\righrarrow\cdots\righrarrow(\psi_n\righrarrow\var\varphi)\cdots)} jest tautologią. Z twierdzenia o pełności wnioskujemy, że</math>\vdash_{H^+} \psi_1\righrarrow(\psi_2\arr\cdots\righrarrow(\psi_n\righrarrow\var\varphi)\cdots)</math>. Stosując $n$ razy (MP) do powyższej formuły dostajemy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta_0\vdash_{H^+}\var\varphi} . Tak więc Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \vdash_{H^+}\var\varphi} , co kończy dowód twierdzenia.

Powiemy, że zbiór formuł $\mathrm{\Delta }$ jest sprzeczny, gdy $vdas{h}_H\mathrm{\perp }$. Zbiór, który nie jest sprzeczny nazwiemy niesprzecznym. Oto nieco inne sformułowanie "silnego" twierdzenia o pełności:

Twierdzenie 6.8

Zbiór formuł jest spełniony wtedy i tylko wtedy, gdy jest niesprzeczny.

Dowód

Zauważmy, że zbiór formuł $\mathrm{\Delta }$ jest sprzeczny, gdy $\mathrm{\Delta }\models ̸\mathrm{\perp }$. A zatem teza wynika z Twierdzeń 5.5 i 6.7, jeśli przyjmiemy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi=\bot} .

A oto twierdzenie o pełności dla rachunku sekwentów i naturalnej dedukcji.

Wniosek 6.9

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_G\var\varphi} oraz Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle e_{N}\var\varphi} .

Dowód

Natychmiast z Twierdzeń 5.8, 5.9 i 6.7.