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. Dlaudowodnienia 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 & \textrm{\ jeśli } \varrho(q_i)=1 \\\neg q_i & \textrm{\ 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 {\em 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

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

<span id="

Powiemy, że zbiór $\mathrm{\Delta }$ jest {\em 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 Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \arr} 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

\bot\not\in\Gamma. \end{equation}

Ponadto, dla dowolnej formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} mamy \textrm{jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi\not\in\Gamma} , to Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \neg\var\varphi\in\Gamma} .} \end{equation} 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 (#eq-zda-2a).

Dla dowolnych formuł Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi,\psi} , (\var\varphi\arr\psi)\in\Gamma \hspace{.5cm} \mbox{ \wtw, gdy } \hspace{.5cm} \var\varphi\not\in\Gamma \mbox{ lub } \psi\in\Gamma. \end{equation} Jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle (\var\varphi\arr\psi)} oraz 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 (#eq-zda-2a). Wówczas sprzeczny zbiór Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \{(\var\varphi\arr\psi),\var\varphi,\neg\psi\}} jest podzbiorem $\mathrm{\Gamma }$ co dowodzi \rightarrowlikacji z lewej do prawej w (#eq-zda-2). Na odwrót, jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle (\var\varphi\arr\psi)\not\in\Gamma} , to na mocy (#eq-zda-2a) mamy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \neg(\var\varphi\arr\psi)\in\Gamma} . Tak więc zbiory </math>\{\neg(\var\varphi\arr\psi), \psi\}$oraz$\{\neg(\var\varphi\arr\psi), \neg\var\varphi\}</math> są sprzeczne, co kończy dowód (#eq-zda-2).

Teraz możemy zdefiniować wartościowanie Parser nie mógł rozpoznać (błąd składni): {\displaystyle \varrho:\\mbox{\small ZZ}\arr \{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} , \models\var\varphi[\varrho] \hspace{.5cm} \mbox{ \wtw, gdy } \hspace{.5cm} \var\varphi\in \Gamma. \end{equation} Dowód (#eq-zda-3) przeprowadzamy przez indukcję ze względu na budowę formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} . Własności (#eq-zda-1)używamy w przypadku gdy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest $\mathrm{\perp }$, a własności (#eq-zda-2) w przypadku, gdy zewnętrznym spójnikiem Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \arr} . " style="font-variant:small-caps">Dowód eq-zda-3

{{{3}}}

Przykład

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$ \wtw, 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\ldots\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łę \[\neg(p_{i,j}\wedge p_{i,j'}).\]

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łę \[\neg(p_{i,j}\wedge p_{i',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 #tw-zda-3a).

Twierdzenie

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 e_{H^+}\var\varphi} .

<span id="

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 „\arr”): {\displaystyle \psi_1\arr(\psi_2\arr\cdots\arr(\psi_n\arr\var\varphi)\cdots)} jest tautologią. Z twierdzenia o pełności wnioskujemy, że </math>\vdash_{H^+} \psi_1\arr(\psi_2\arr\cdots\arr(\psi_n\arr\var\varphi)\cdots)</math>. Stosując $n$ razy (MP) do powyższej formuły dostajemy \[\Delta_0\vdash_{H^+}\var\varphi.\] Tak więc Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle e_{H^+}\var\varphi} , co kończy dowód twierdzenia. " style="font-variant:small-caps">Dowód

{{{3}}}

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

Twierdzenie

Dowód

{{{3}}}

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

Wniosek

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

{{{3}}}

\subsection*{Ćwiczenia}\begin{small}

1. Dowieść, że "silne" twierdzenie o pełności

(Twierdzenie #tw-zda-4) pociąga twierdzenie o zwartości.

1. <span id="wtomigraj} Udowodnić, że jeśli w systemie Parser nie mógł rozpoznać (błąd składni): {\displaystyle \vdash_{H+" \> }

zamienimy aksjomaty (B1--B4) na aksjomaty

1. • [(D1)] Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi\to\var\varphi\vee \psi} ;
   • [(D2)] Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \psi\to\var\varphi\vee \psi} ;
   • [(D3)] </math>(\var\varphi\to \vartheta)\wedge(\psi\to \vartheta)

\to(\var\varphi\vee \psi \to \vartheta)</math>;

1. • [(C1)] Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi\wedge \psi\to \var\varphi} ;
   • [(C2)] Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi\wedge \psi\to \psi} ;
   • [(C3)] </math>(\vartheta\to \var\varphi)\wedge(\vartheta\to \psi)\to

(\vartheta\to\var\varphi\wedge \psi)</math>.

to twierdzenie o pełności pozostanie prawdziwe.

\item Dany jest nieskończony zbiór chłopców, z których każdy ma skończoną liczbę narzeczonych. Ponadto dla każdego $k\in N$, dowolnych $k$ chłopców ma co najmniej $k$ narzeczonych. Dowieść, że każdy chłopiec może się ożenić z jedną ze swoich narzeczonych bez popełnienia bigamii.