Теоремата от предния път
Нека $S$ е множество от дизюнкти, тогава $S$ е неизпълнимо тогава и само тогава, когато $S \overset{r}{\vdash} \blacksquare$
Следствие (Теорема за компактност на изпълнимостта)
Нека $S$ е множество от дизюнкти, тогава $S$ е неизпълнимо т.с.т.к. съществува крайно $S_0 \subseteqq S$ което е неизпълнимо
Доказателство:
$|\Leftarrow|$
Нека $S_0 \subseteqq S$ и $S_0$ е неизпълнимо, тъй като всеки модел на $S$ е модел и на $S_0$, множеството $S$ също е неизпълнимо.
$|\Rightarrow|$
Нека $S$ е неизпълнимо, тогава $S \overset{r}{\vdash} \blacksquare$. Нека $D_1, \dots, D_n$ е резолютивен извод от $S$ и $D_n = \blacksquare$. Нека дефинираме $S_0 = \{ D_1, \dots, D_n \} \cap S$. $S_0$ е крайно, $S_0 \subseteqq S$ и $S_0 \overset{r}{\vdash} \blacksquare$, следователно $S_0$ е неизпълнимо. Т.е намерихме крайно неизпълнимо подмножество на $S$.
Дефиниция (булево следване)
Нека $\Delta$ е множество от съждителни формули и $\varphi$ е съждителна формула. Казваме, че от $\Delta$ булево следва $\varphi$, записваме $\Delta \overset{b}\models \varphi$, ако всяка булева интерпретация $I$ която е модел за $\Delta$ е модел и за $\varphi$.
Теорема (компактност на изпълнимостта)
Нека $\Delta$ е множество от съждителни формули. Тогава
(i) $\Delta$ е изпълнимо т.с.т.к. всяко крайно $\Delta_0 \subseteq \Delta$ е изпълнимо;
(ii) $\Delta$ е неизпълнимо т.с.т.к. съществува крайно $\Delta_0 \subseteq \Delta$, което е неизпълнимо.
Забележка: Няма ограничение за броя на променливите.
Забележка 2: (i) и (ii) са еквивалентни. Ние ще докажем второто.
Доказателство:
$|\Rightarrow|$
Нека $\Delta$ е булево неизпълнимо множество от съждителни формули.
От всяка съждителна формула (отрицание, конюнкция, дизюнкция, имликация, еквивалентност) може да образуваме конюнктивна нормална форма (конюнкция от дизюнкции) и след това да образуваме дизюнкт от всяка дизюнкция, и да вземем множеството от получените дизюнкти. Т.е от произволна съждителна формула $\varphi$ образуваме съответстващото и множество от дизюнкти $S_\varphi$. Аналогично - ако $M$ е множество от съждителни формули дефинираме $S_M = \{ S_\varphi\ |\ \varphi \in M \}$. Лесно се проверява, че $I \models M \longleftrightarrow I \models S_M$.
По условие $\Delta$ е булево неизпълнимо, следователно $S_\Delta$ е неизпълнимо. Но това е множество от дизюнкти, следователно може да приложим теоремата за компактност на множества от дизюнкти, т.е - съществува крайно $S_0 \subseteq S_\Delta$, което е неизпълнимо.
Обърнете внимание, че това множество съдържа дизюнкти от разни формули принадлежащи на $\Delta$. Остава да изберем по една формула от $\Delta$ за всеки дизюнкт от $S_0$, такава че дизюнкта да принадлежи на множеството от дизюнкти на формулата. Да си обозначим така избраните формули с $\Delta_0$. Понеже $S_0$ е неизпълнимо, то и $\Delta_0$ също е неизпълнимо - $S_{\Delta_0} \supseteq S_0$. С това намерихме крайно неизпълнимо подмножество от произволно неизпълнимо множество от съждителни формули.
$|\Leftarrow|$
Нека $\Delta_0$ е неизпълнимо. Тогава като добавим още формули, то ще продължи да бъде неизпълнимо, т.е $\Delta \supseteq \Delta_0$ е неизпълнимо.
Теорема (компактност на булевото следване)
Нека $\Delta$ е множество от съждителни формули и $\varphi$ е съждителна формула.
$\Delta \overset{b}\models \varphi$ т.с.т.к съществува крайно подмножество $\Delta_0 \subseteq \Delta$, такова че $\Delta_0 \overset{b}\models \varphi$.
Доказателство:
$|\Leftarrow|$
Нека $\Delta_0 \subseteq \Delta$ е крайно и $\Delta_0 \overset{b}\models \varphi$. Това всъщност означава, че $I \models \Delta_0 \rightarrow I \models \varphi \qquad (\star)$. Нека $I \models \Delta$, т.е $I$ е модел за всяка формула в $\Delta$ - от тук $I \models \Delta_0$. От $(\star)$ получаваме, че $I \models \varphi$. Получихме, че $I \models \Delta \rightarrow I \models \varphi$, следователно $\Delta \overset{b}\models \varphi$.
$|\Rightarrow|$
Нека $\Delta \overset{b}\models \varphi$. Ако $\Delta$ е неизпълнимо, то от теоремата за компактност на изпълнимостта получаваме, че съществува крайно $\Delta_0 \subseteq \Delta$, което е неизпълнимо. Тогава $\Delta_0 \models \varphi$1. Сега да се съсредоточим върху случая $\Delta$ изпълнимо. Нека разгледаме множеството $\Delta \cup \{ \lnot \varphi \}$. Ще докажем, че то е булево неизпълнимо (няма модели). Нека $I$ е произволна булева интерпретация. Има две възможности за нея:
(1) $I \models \Delta$. От $\Delta \models \varphi$ получаваме, че $I \models \varphi$, т.е $I \nvDash \lnot \varphi$. Следователно $I \nvDash \Delta \cup \{ \lnot \varphi \}$;
(2) $I \nvDash \Delta$. Следователно и $I \nvDash \Delta \cup \{ \lnot \varphi \}$;
Следователно за произволно $I$ е изпълнено, че $I \nvDash \Delta \cup \{ \lnot \varphi \}$ - т.е множеството е неизпълномо. От теоремата за компактност на изпълнимостта получаваме, че съществува крайно подмножество $\Delta_0 \subseteq \Delta \cup \{ \lnot \varphi \}$, което е неизпълнимо. Със сигурност $\{ \lnot \varphi \} \in \Delta_0$, защото иначе ще се окаже, че $\Delta_0 \subseteq \Delta$, т.е $\Delta$ е неизпълнимо (този случай го разгледахме в началото). Сега остава да докажем, че $\Delta_0' = \Delta_0 \setminus \{ \lnot \varphi \}$ е такова, че $\Delta_0' \overset{b}\models \varphi$. Нека $I \models \Delta_0'$, тогава със сигурност $I \nvDash \{ \lnot \varphi \}$, иначе ще се окаже, че $\Delta_0$ има модел. Т.е имаме, че $I \models \varphi$. Следователно $I \models \Delta_0' \rightarrow I \models \varphi$, т.е $\Delta_0' \overset{b}\models \varphi$.
Горната теорема има хубави приложение в теория на графите.
Теорема (компактност на предикатната изпълнимост)
Нека $\mathcal{L}$ е език на предикатното смятане, без формално равенство, нека $\Gamma$ е множество от затворени формули.
(i) $\Gamma$ има модел т.с.т.к. всяка крайно $\Gamma_0 \subseteq \Gamma$ има модел.
(ii) $\Gamma$ е неизпълнимо т.с.т.к. съществува крайно $\Gamma_0 \subseteq \Gamma$, което е неизпълнимо.
Забележка: Тук отново (i) е равносилно на (ii). Ние ще докажем второто.
Доказателство:
$|\Leftarrow|$
Нека $\Gamma_0$ е крайно подмножество на $\Gamma$ и $\Gamma_0$ е неизпълнимо. Това означава, че няма структура, в която да са верни всички формули от $\Gamma_0$ - следователно няма и структура в която са верни всички формули от $\Gamma$. Т.е $\Gamma$ е неизпълнимо.
$|\Rightarrow|$
Идеята е следната. Ще преминем през ПНФ (пренексна нормална форма), след което СНФ (скулемова нормална форма). После образуваме частните случаи $\mathrm{Si}$ на скулемизираните формули. Защо минаваме през всичко това??? Ами частните случаи са просто булеви (съждителни) формули, за които в последните теореми доказахме разни компактности, и сега ще ги използваме. За да се докопаме обаче до булеви формули първо трябва да преминем през ПНФ, СНФ, частни случаи. После трябва да се върнем и наобратно, за да пренесем извода за булеви формули до извод за затворени предикатни формули. Lets go!
Нека $\Gamma$ няма модел. За всяка формула $\varphi \in \Gamma$ избираме точно една формула $\varphi'$, такава че $\varphi'$ е в ПНФ (Пренексна Нормална Форма) $\varphi {|=|} \varphi'$. С множеството $\Gamma'$ означаваме множеството от $\varphi'$, за които $\varphi \in \Gamma$, т.е множеството от всички пренексни нормални форми на формули от $\Gamma$.
Да образуваме $\Gamma'^{S}$ - множеството от скулемовите нормални форми на формулите от $\Gamma'$.
Да разгледаме $\mathrm{Si}(\Gamma'^{S})$. По пътя не сме променяли изпълнимостта(-> ПНФ(защото формулите са еквивалентни), ПНФ->СНФ, СНФ->Частни Случаи) следователно $\mathrm{Si}(\Gamma'^S)$ е неизпълнимо.
Използваме теоремата за компактност на изпълнимостта и получаваме, че съществува крайно $\Delta \subseteq \mathrm{Si}(\Gamma'^S)$, което е неизпълнимо
Сега се връщаме назад.
За всяка формула $\theta \in \Delta$ си взимаме точно една формула $\varphi_\theta$, такава че $\theta$ е частен случай на $\varphi_\theta$. Нека $X = \{ \varphi_\theta\ |\ \theta \in \Delta \}$. $X \subseteq \Gamma'^S$.
Ще докажем, че $X$ е неизпълнимо. Да разгледаме $\mathrm{Si}(X)$ - то е надмножество на $\Delta$, защото $\theta \in \mathrm{Si}(\varphi_\theta)$ за всяко $\varphi_\theta \in X$. Понеже $\Delta$ е неизпълнимо, то и $\mathrm{Si}(X)$ е неизпълнимо. Следователно $X$ е неизпълнимо.
Да си образуваме множеството $Y$ от формули, чиито скулемови нормални форми са в множеството $X$, т.е $Y = \{ \varphi'\ |\ \varphi'^S \in X \}$. $Y \subseteq \Gamma'$. От $X$ неизпълнимо следва $Y$ неизпълнимо.
Да си образуваме множеството $\Gamma_0$ от формули, чиито пренексни нормални форми са в множеството $Y$, т.е $\Gamma_0 = \{ \varphi\ |\ \varphi' \in Y \}$. $\Gamma_0 \subseteq \Gamma$. Понеже всяка формула е еквивалентна с пренексната си нормална форма, то $\Gamma_0$ е неизпълнимо. Тъй като $|\Delta| = |X| = |Y| = |\Gamma_0|$, то $\Gamma_0$ е крайно.
Т.е намерихме крайно подмножество на $\Gamma$ което е неизпълнимо.