Булеви формули над дадено множество от съждителни променливи

---

страницата се нуждае от дописване/преглеждане

---

Дефиниция (булеви формули)

Нека $\mathbb{P}\mathrm{rop}$ е множество от различни букви (различни атомарни формули). Индуктивно дефинираме булеви формули над $\mathbb{P}\mathrm{rop}$:

• всеки елемент на $\mathbb{P}\mathrm{rop}$ е булева формула;
• ако $\varphi$ е булева формула, то $\lnot \varphi$ е също булева формула;
• ако $\varphi, \psi$ са булеви формули, то $(\varphi \sigma \psi)$ при $\sigma \in \{ \And, \lor, \Rightarrow, \iff \}$ също е булева формула.

Дефиниция (булева интерпретация)

Булева интерпретация е функция $I : \mathbb{P}\mathrm{rop} \to \{ \mathrm{t}, \mathrm{f} \}$.

Лема

Нека $I_0$ е булева интерпретация. Тогава съществува единствено изображение $I$ над всички булеви формули над $\mathbb{P}\mathrm{rop}$, такова че:

• $I(p) = I_0(p) \quad p \in \mathbb{P}\mathrm{rop}$
• $I(\lnot \varphi) = H_\lnot(I(\varphi))$
• $I((\varphi \sigma \psi)) = H_\sigma(I(\varphi), I(\psi))$

Забележка: Горната лема просто позволява да разглеждаме булевата интерпретацията не само върху променливите, а и върху формулите (подобно на оценка в структура). За напред под интерпретация ще разбираме точно това - функция върху всички променливи и формули над $\mathbb{P}\mathrm{rop}$.

Дефиниция (булево изпълнимо множество)

Нека $\Delta$ е множество от съждителни формули над $\mathbb{P}\mathrm{rop}$. Казваме, че $\Delta$ е булево изпълнимо, ако съществува булева интерпретация $I$, такава че $I(\varphi) = \mathrm{t}$ за всяко $\varphi \in \Delta$. Записваме $I \overset{b}\models \Delta$.

Дефиниция (булева тавтология)

Една булева формула $\varphi$ ще наричаме булева тавтология, ако за всяка интерпретация $I$, $I(\varphi) = \mathrm{t}$. Записваме $\overset{b}\models \varphi$.

Дефиниция (булево следване)

Нека $\Delta$ е множество от булеви формули. Ще казваме, че от $\Delta$ булево следва $\varphi$, ако за всяка интерпретация $I$, за която $I \overset{b}\models \Delta$ следва $I \overset{b}\models \varphi$

Твърдение

Нека $\mathcal{L}$ е език без формално равенство. $\Gamma$ е множество от затворени универсални формули. Следните две условия са еквивалентни:
(i) Има свободна ербранова структура $\mathcal{A}$, за която $\mathcal{A} \underset{\mathrm{id}_A}\models \mathrm{Si}(\Gamma)$
(ii) $\mathrm{Si}(\Gamma)$ е булево изпълнимо.

Доказателство: Първо искам да обърна внимание, че множеството $\mathrm{Si}(\Gamma)$ може да бъде разглеждано като множество от булеви формули, като буквите или по друг начин казано - атомарните формули - $\mathbb{P}\mathrm{rop}$ - са точно $p(\tau_1, \dots, \tau_n)$ за всеки предикатен символ $p$ в $\mathcal{L}$.
Нека $I$ е произволна булева интерпретация върху атомарните формули в $\mathcal{L}$. Нека $\mathcal{A}_I$ е свободна ербранова структура. Ще дефинираме $p^{\mathcal{A}_I}$ - интерпретация на произволен предикатен символ от $\mathcal{L}$ в структурата $\mathcal{A}_I$¹:

(1)

\begin{align} p^{\mathcal{A}_I} \rightleftharpoons \{ \langle \tau_1, \dots, \tau_n \rangle | I(p(\tau_1, \dots, \tau_n)) = \mathrm{t} \} \end{align}

с други думи един предикат ще бъде истина, само ако според булевата интерпретация той е истина.
Ще докажем следната еквивалентност:

(2)

\begin{align} \mathcal{A}_I \underset{\mathrm{id}_A}\models \varphi \longleftrightarrow I(\varphi) = \mathrm{t} \end{align}

Ще направим индуктивно доказателство по построението на $\varphi$:
(1) $\varphi = p(\tau_1, \dots, \tau_n)$

(3)

\begin{eqnarray} \mathcal{A}_I \underset{\mathrm{id}_A}\models \varphi &\leftrightarrow& \mathcal{A}_I \underset{\mathrm{id}_A}\models p(\tau_1, \dots, \tau_n) \\ &\leftrightarrow& \langle \|\tau_1\|^{\mathcal{A}_I}[\mathrm{id}_A], \dots, \|\tau_n\|^{\mathcal{A}_I}[\mathrm{id}_A] \rangle \in p^{\mathcal{A}_I} \\ &\leftrightarrow& \langle \tau_1, \dots, \tau_n \rangle \in p^{\mathcal{A}_I} \\ &\overset{\mbox{def } p^{\mathcal{A}_I}}\leftrightarrow& I(p(\tau_1, \dots, \tau_n)) = \mathrm{t} \\ &\leftrightarrow& I(\varphi) = \mathrm{t} \\ \end{eqnarray}

(2) $\varphi = \lnot \psi$ където за $\psi$ твърдението е изпълнено.

(4)

\begin{eqnarray} \mathcal{A}_I \underset{\mathrm{id}_A}\models \varphi &\leftrightarrow& \mathcal{A}_I \underset{\mathrm{id}_A}\models \lnot \psi \\ &\leftrightarrow& \|\lnot \psi\|^{\mathcal{A}_I}[\mathrm{id}_A] = \mathrm{t} \\ &\leftrightarrow& \| \psi \|^{\mathcal{A}_I}[\mathrm{id}_A] = \mathrm{f} \\ &\leftrightarrow& I(\psi) = \mathrm{f} \\ &\leftrightarrow& I(\lnot\psi) = \mathrm{t} \\ &\leftrightarrow& I(\varphi) = \mathrm{t} \\ \end{eqnarray}

(3) $\varphi = \psi_1 \sigma \psi_2$, където за $\psi_1, \psi_2$ твърдението е изпълнено.

(5)

\begin{eqnarray} \mathcal{A}_I \underset{\mathrm{id}_A}\models \varphi &\leftrightarrow& \mathcal{A}_I \underset{\mathrm{id}_A}\models \psi_1 \sigma \psi_2 \\ &\leftrightarrow& \|\psi_1 \sigma \psi_2\|^{\mathcal{A}_I}[\mathrm{id}_A] = \mathrm{t} \\ &\leftrightarrow& H_\sigma(\|\psi_1 \|^{\mathcal{A}_I}[\mathrm{id}_A], \|\psi_2 \|^{\mathcal{A}_I}[\mathrm{id}_A]) = \mathrm{t} \\ &\leftrightarrow& H_\sigma(I(\psi_1), I(\psi_2)) = \mathrm{t} \\ &\leftrightarrow& I(\psi_1 \sigma \psi_2) = \mathrm{t} \\ &\leftrightarrow& I(\varphi) = \mathrm{t} \\ \end{eqnarray}

С това еквивалентността е доказана.
(i) -> (ii) По-нагоре показахме, как с произволна булева интерпретация може да се дефинира свободна ербранова структура (или по-точно - интерпретация на предикатните й символи). Естествено възможно е и обратното - от произволна структура, може да дефинираме булева интерпретация над атомарните формули, използвайки интерпретацията на предикатните символи в структурата. Нека $\mathcal{A}$ е свободна ербранова структура и $\mathcal{A} \underset{\mathrm{id}_A}\models \mathrm{Si}(\Gamma)$. Нека $I_\mathcal{A}$ е булева интерпретация дефинирана върху атомарните формули в $\mathcal{L}$ такава че $I(p(\tau_1, \dots, \tau_n)) = \mathrm{t}$ тогава и само тогава, когато $\langle \tau_1, \dots, \tau_n \rangle \in p^\mathcal{A}$. Сега използваме еквивалентността за всички формули от $\mathrm{Si}(\Gamma)$ и получаваме, че $I(\varphi) = \mathrm{t}$ за всяко $\varphi \in \mathrm{Si}(\Gamma)$. Следователно $\mathrm{Si}(\Gamma)$ е булево изпълнимо - съществува булева интерпретация (именно $I_\mathcal{A}$), такава че всички формули в множеството са булево изпълними според интерпретацията. С това тази посока е доказана.
(ii) -> (i) Нека $\mathrm{Si}(\Gamma)$ е булево изпълнимо. Следователно съществува интерпретация $I$, такава че $I(\varphi) = \mathrm{t}$ за всяко $\varphi \in \mathrm{Si}(\Gamma)$. Използваме еквивалентността и получаваме, че $\mathcal{A} \underset{\mathrm{id}_A}\models \varphi$ за всяко $\varphi \in \mathrm{Si}(\Gamma)$. Следователно $\mathcal{A} \underset{\mathrm{id}_A}\models \mathrm{Si}(\Gamma)$.
С това твърдението е доказано.

Твърдение ([изпълнимост <-> булева изпълнимост] на множество съждителни формули)

Нека $\mathcal{A}$ е произволна структура за езика $\mathcal{L}$ в който няма формално равенство. Нека $v$ е оценка в $\mathcal{A}$. Нека $\Gamma$ е произволно множество от затворени универсални формули. Следните две твърдения са еквивалентни:
(i) $\mathcal{A} \underset{v}\models \mathrm{Si}(\Gamma)$;
(ii) $\mathrm{Si}(\Gamma)$ е булево изпълнимо.

Забележка: Ако не се лъжа, тук "затворената универсалност" на формулите и $\mathrm{Si}$ се ползва до толкова, че да получим безкванторни формули (съждителни). Т.е. твърдението можеше да бъде казано така: $\mathcal{A} \underset{v}\models X \leftrightarrow X$ е булево изпълнимо, ако $X$ е множество съждителни формули.

Доказателство: Доказателството много си прилича с доказателството на предишното твърдение. Ще покажем само как се извежда еквивалентността

(6)

\begin{align} \mathcal{A} \underset{v}\models \varphi \longleftrightarrow I(\varphi) = \mathrm{t} \end{align}

Нека $\mathcal{A}, v$ са интерпретация и оценка в нея. Дефинираме булева интерпретация $I_{\mathcal{A}, v}$:

(7)

\begin{align} I_{\mathcal{A}, v}(p(\tau_1, \dots, \tau_n)) = \mathrm{t} \rightleftharpoons \mathcal{A} \underset{v}\models p(\tau_1, \dots, \tau_n) \end{align}

Доказателство по индукция по построението на $\varphi$:
(1) $\varphi = p(\tau_1, \dots, \tau_n)$ - следва директно от дефиницията на $I_{\mathcal{A}, v}$.
(2) $\varphi = \lnot \psi$ — виж предното твърдение (2)
(3) $\varphi = \psi_1 \sigma \psi_2$ — виж предното твърдение (3)

Забележка 2: Аз лично не виждам защо доказахме предното твърдение, при условие, че това е доста по общо — предното говори за свободни ербранови структури и оценката идентитет, това е за произволна структура и оценка. Също разликата в доказателствата е микроскопична в имплементацията, а на идейно ниво са напълно еднакви.

Теорема (връзка между изпълнимост на множество затворени универсални формули и булева изпълнимост на частните му случаи)

Нека $\mathcal{L}$ е език без формално равенство, $\Gamma$ е множество от затворени универсални формули. Еквивалентни са:
(i) $\Gamma$ има модел;
(ii) $\Gamma$ има свободен ербранов модел;
(iii) $\mathrm{Si}(\Gamma)$ е булево изпълнимо.

Доказателство:
(ii) -> (iii) Нека $\mathcal{A}$ е свободна ербранова структура и $\mathcal{A} \models \Gamma$. Използвайки това твърдение получаваме, че $\mathcal{A} \underset{\mathrm{id}_A}\models \mathrm{Si}(\Gamma)$. Сега според това твърдение имаме, че $\mathrm{Si}(\Gamma)$ е булево изпълнимо.
(iii) -> (ii) Нека $\mathrm{Si}(\Gamma)$ е булево изпълнимо. От това твърдение следва, че съществува свободна ербранова структура $\mathcal{A}$, такава че $\mathcal{A} \underset{\mathrm{id}}\models \mathrm{Si}(\Gamma)$. От това твърдение получаваме, че $\mathcal{A} \models \Gamma$, т.е $\mathcal{A}$ е свободен ербранов модел на $\Gamma$.
(ii) -> (i) Това е очевидно - щом съществува свободен ербранов модел, следователно съществува и модел на $\Gamma$.
(i) -> (iii) Нека $\mathcal{A}$ е произволна структура. Нека $\mathcal{A} \models \Gamma$. Нека $v$ е произволна оценка в $\mathcal{A}$. Ще докажем, че $\mathcal{A} \underset{v}\models \mathrm{Si}(\Gamma)$².
Нека $\theta \in \mathrm{Si}(\Gamma)$ е произволна формула. Тогава $\theta = \varphi[x_1/\tau_1, \dots, x_n/\tau_n]$ и $\forall x_1 \dots \forall x_n \varphi = \psi \in \Gamma$ - т.е $\theta$ е частен случай на $\psi$ при термове заместващи променливите $x_1, \dots, x_n$.

Да си изберем $n$ чисто нови променливи - т.е не се срещат в $\{ x_1, \dots, x_n \}$ или в $\tau_1, \dots, \tau_n$. Да си ги кръстим $x_1', \dots, x_n'$.
Ще използваме едно много хубаво твърдение.
Като за начало ще преименуваме всички х-ове да станат с примове:

(8)

\begin{align} \mathcal{A} \underset{v}\models \forall x_1 \dots \forall x_n \varphi \rightarrow \forall x_1' \dots \forall x_n' \varphi[x_1/x_1', \dots, x_n/x_n'] \end{align}

За по-кратко си дефинираме:

(9)

\begin{align} \varphi' = \varphi[x_1/x_1', \dots, x_n/x_n'] \end{align}

Сега използваме многократно хубавото твърдение и факта, че щом в една структура и оценка е вярна една импликация (нещо1 => нещо2) и нещо1 е вярно в структурата и оценката, следователно и нещо2 е вярно в структурата и оценката:

(10)

\begin{eqnarray} &\mathcal{A} \underset{v}\models \forall x_1' \dots \forall x_n' \varphi' &\mbox{ and } \models \forall x_1' \dots \forall x_n' \varphi' \Rightarrow \forall x_2' \dots \forall x_n' \varphi'[x_1'/\tau_1] \\ \rightarrow &\mathcal{A} \underset{v}\models \forall x_2' \dots \forall x_n' \varphi'[x_1'/\tau_1]& \\ &\mathcal{A} \underset{v}\models \forall x_2' \dots \forall x_n' \varphi'[x_1'/\tau_1] &\mbox{ and } \models \forall x_2' \dots \forall x_n' \varphi'[x_1'/\tau_1] \Rightarrow \forall x_3' \dots \forall x_n' \varphi'[x_1'/\tau_1][x_2'/\tau_2] \\ \rightarrow &\mathcal{A} \underset{v}\models \forall x_3' \dots \forall x_n' \varphi'[x_1'/\tau_1][x_2'/\tau_2]& \\ &\vdots& \\ \rightarrow &\mathcal{A} \underset{v}\models \varphi'[x_1'/\tau_1][x_2'/\tau_2]\dots[x_n'/\tau_n]& \\ \rightarrow &\mathcal{A} \underset{v}\models \varphi'[x_1'/\tau_1, x_2'/\tau_2, \dots, x_n'/\tau_n]& \\ \rightarrow &\mathcal{A} \underset{v}\models \varphi[x_1/x_1', \dots, x_n/x_n'][x_1'/\tau_1, x_2'/\tau_2, \dots, x_n'/\tau_n]& \\ \rightarrow &\mathcal{A} \underset{v}\models \varphi[x_1/\tau_1, x_2/\tau_2, \dots, x_n/\tau_n] = \theta & \\ \end{eqnarray}

Доказахме, че произволна формула от $\mathrm{Si}(\Gamma)$ е вярна в $\mathcal{A}, v$, следователно $\mathcal{A} \underset{v}\models \mathrm{Si}(\Gamma)$ и сега от това излиза, че $\mathrm{Si}(\Gamma)$ е булево изпълнимо.

Забележка1: На лекции не е правено точно по този начин. Този обаче ми се вижда верен :)

Забележка2: Защо използваме примовете ами не разсъждаваме директно с нормалните х-ове? Ами причината е, че за да правим замяна с $\tau_i$ трябва да сме сигурни, че тя е валидна. Проблем ще се окаже, ако в $\tau_1$ има променливата $x_2$, защото тогава ще заместим и променлива от $\tau_2$ ще попадне под квантор (това означава, че е недупостима замяна). Затова първо преименоваме всички х-ове да станат с примове, после си заместваме спокойно (защото няма как в някое $\tau$ да има променлива $x_i'$ която да се окаже под квантор), и след като сме направили всички замени не са останали никакви примове (защото първо заменяме х-овете с х-примове и после x-примовете с $\tau_i$).

Footnotes

1. обърнете внимание, че в една свободна ербранова структура интерпретацията на предикатните символи е единственото недефинирано - в смисъл самия факт, че е свободна ербранова дефинира еднозначно как се интерпретират константите и функционалните символи - остават само предикатните

2. понеже множеството $\Gamma$ е от универсални затворени формули, то за тяхната стойност в структурата $\mathcal{A}$ нямаме нужда от оценка. В множеството $\mathrm{Si}(\Gamma)$ обаче формулите не са затворени - затова за да ги оценим се нуждаем от оценка. Друг е въпроса, че те ще бъдат вeрни при всяка оценка :-)