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 podamyelegancki dowód pochodzący od L. Kalm\'ara. Dlaudowodnienia nieco silniejszej wersji twierdzenia o pełności (Twierdzenie #tw-zda-4) wykorzystamy silne i bardzo pożyteczne Twierdzenie #tw-zda-5 zwane twierdzeniem o zwartości.

\begin{lemat}[Kalm\'ar] Niech Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} będzie formułą zbudowaną przyużyciu Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \arr} 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}\arr\{0,1\} } będzie dowolnym wartościowaniem. Dla $i=1,\dots ,n$ definiujemy formuły: Parser nie mógł rozpoznać (nieznana funkcja „\begi”): {\displaystyle q'_i=\left\{ \begi\prooftree array \justifies ll \using \textrm{(W)}\endprooftree q_i & \mbox{ jeśli } \varrho(q_i)=1,\\ \neg q_i & \mbox{ jeśli } \varrho(q_i)=0. \end{array} } 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 Parser nie mógł rozpoznać (błąd składni): {\displaystyle \{q_1',\ldots,q_n'\}\vdash_H\psi \mbox{ oraz } \end{lemat} \begin{dowod} Dowód jest prowadzony przez indukcję ze względu na budowę formuły <math>\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

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.

\noindent (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 #le-zda-1(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

\noindent (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

\noindent (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 </math> Z Lematu #le-zda-1(1) mamy $\{{q_1}^{\prime },\dots ,{q_n}^{\prime }\}{⊢}_H$ Stosując teraz dwukrotnie (MP) dostajemy

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

\begin{lemat} 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 $e_H\psi$. \end{lemat}

Dowód

{{{3}}}

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

Twierdzenie

Jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest tautologią zbudowaną przyużyciu Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \arr} oraz $\mathrm{\perp }$, to Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \vdash_H\var\varphi} .

{{dowod|eq-zda-3a|

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$-{\em 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$, \mbox{jeśli $\mathrm{\Delta }$ jest $m$-zbiorem, to Parser nie mógł rozpoznać (nieznana funkcja „\se”): {\displaystyle \se_H\var\varphi} }. \end{equation}

Zauważmy, że biorąc $m=0$ w (#eq-zda-3a) dostajemy tezę twierdzenia. Dowód (#eq-zda-3a) przeprowadzimy przez indukcję ze względu na $m$ w zbiorze $\{0,\dots ,n\}$uporządkowanym relacją ${\le }^{-1}$. Dla $m=n$ własność (#eq-zda-3a) wynika z Lematu #le-zda-2 oraz z faktu, że Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest tautologią. Załóżmy, że (#eq-zda-3a) zachodzi dla pewnego $0<m<n$ i niech $\mathrm{\Delta }$ będzie dowolnym $(m-1)$-zbiorem. Z założenia indukcyjnego dostajemy \[\Delta,q_{m}\vdash_H\var\varphi\] oraz \[\Delta,\neg q_{m}\vdash_H\var\varphi.\] Zatem na mocy Lematu #le-zda-2aa dostajemy \[\se_H\var\varphi.\] \Rightarrow kończy dowód (#eq-zda-3a) i tym samym dowód twierdzenia o pełności. }}

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

Twierdzenie

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

{{{3}}}

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 \wtw, 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.