Table of Contents
|
Предикатни формули
Дефиниция (атомарна формула)
Нека $\mathcal{L}$ е FOL и $\tau_1, \tau_2, \cdots, \tau_n$ са термове в него.
Нека $p \in \mathbb{P}\mathrm{red}$ и $\sharp[p] = n$.
Тогава $p(\tau_1, \tau_2, \cdots, \tau_n)$ е атомарна формула.
Ако в $\mathcal{L}$ има формално равенство, тогава $(\tau_1 \dot= \tau_2)$ също е атомарна формула.
Ще бележим множеството на всички атомарни формули над $\mathcal{L}$ с $\mathcal{A}\mathrm{t}_\mathcal{L}$.
Дефиниция (предикатна формула)
Нека $\mathcal{L}$ е FOL.
- ако $\varphi$ е атомарна формула над $\mathcal{L}$, то $\varphi$ е предикатна формула;
- ако $\varphi$ е предикатна формула, то $\lnot\varphi$ също е предикатна формула;
- ако $\varphi, \psi$ са предикатни формули, то $(\varphi \And \psi)$, $(\varphi \lor \psi)$, $(\varphi \Rightarrow \psi)$, $(\varphi \iff \psi)$ са предикатни формули;
- ако $\varphi$ е предикатна формула, а $x$ е индивидна променлива, то $\forall x \varphi$ и $\exists x \varphi$ са предикатни формули.
Множеството от всички предикатни формули над $\mathcal{L}$ ще бележим с $\mathcal{F}_\mathcal{L}$.
Забележка: Предикатните и атомарните формули са също синтактични образувания - просто поредица от символи. За момента не влагаме никакъв смисъл в тях, просто обясняваме как може рекурсивно да се изграждат от други предикатни/атомарни формули и/или термове (всички които са все думи - т.е. поредица от символи).
Семантика на предикатните формули
Ще въведем двете логически стойности - Истина и Лъжа. На лекции се обозначават с и и л, но поради ограничения в уикипедията ще използвам $\mathrm{t}$ и $\mathrm{f}$.
Дефиниция (H_)
Ще си дефинираме фамилия от функции, които ще извършват елементарните логически операции (отрицание, конюнкция, дизюнкция итн):
(1)Дефиниция (модифицирана оценка)
Оценка v, модифицирана в точка х с а:
(2)Дефиниция (стойност на предикатна формула)
Подобно на стойност на терм ще дефинираме и стойност на формула.
Нека $\mathcal{A}$ е структура, $v$ е оценка в нея и $\varphi$ е предикатна формула.
Ще отбелязваме стойност на $\varphi$ при оценка $v$ по следния начин:
Разбира се, $\|\varphi\|^\mathcal{A}[v] \in \{ \mathrm{t}, \mathrm{f} \}$.
Сега ще направим индуктивна дефиниция за самата стойност, според конструкцията на $\varphi$:
- Нека $\varphi = p(\tau_1, \cdots, \tau_n)$ е атомарна формула. Дефинираме
- Нека $\varphi = (\tau_1 \dot= \tau_2)$ е атомарна формула. Дефинираме
- Нека $\varphi = \lnot \psi$, където $\psi$ е предикатна формула. Дефинираме
- Нека $\varphi = (\psi_1 \sigma \psi_2)$, където $\psi_1, \psi_2$ са предикатни формули, а $\sigma \in \{ \And, \lor, \Rightarrow, \iff \}$. Дефинираме
- Нека $\varphi = \forall x\psi$, където $x$ е индивидна променлива и $\psi$ е предикатна формула. Дефинираме:
$\|\forall x \psi\|^\mathcal{A}[v] = \mathrm{t} \leftrightharpoons$ За всеки елемент $a \in A$ е изпълнено $\|\psi\|^\mathcal{A}[v_a^x] = \mathrm{t}$.
- Нека $\varphi = \exists x \psi$. Дефинираме:
$\|\exists x \psi\|^\mathcal{A}[v] = \mathrm{t} \leftrightharpoons$ Съществува елемент $a \in A$, такъв че $\|\psi\|^\mathcal{A}[v_a^x] = \mathrm{t}$.
Има още един начин да записваме оценка на предикатна формула:
(8)Област на действие на квантор
Дефиниция (област на действие на квантор)
Нека $\varphi$ е формула, $Q$ е квантор (т.е $Q \in \{ \forall, \exists \}$) и нека $\varphi = \alpha Q \beta$ е участие1 на квантора $Q$ в $\varphi$. Тогава съществува единствена индивидна променлива $x$ и единствена предикатна формула $\psi$, такива че $\varphi = \alpha Qx\psi\beta'$. Това участие на $x\psi$ се нарича област на действие на участието $\alpha Q\beta$ на $Q$ във $\varphi$. Казваме, че това участие на $Q$ е по индивидната променлива $x$.
Пример
(9)Дефиниция (свързано участие на индивидна променлива)
Едно участие на индивидната променлива $x$ се нарича свързано участие, ако то е в област на действие на квантор по $x$. Иначе това участие на $x$ се нарича свободно участие.
Пример
(10)В този случай всяко участие на индивидната променливата $x$ е в областта на действие на най-близко стоящия и отляво квантор. Това прилича малко на област на видимост на променливи в C/C++ - ако във дадена скоба дефинирате променлива, със същото име като променлива от външната скоба, ако употребите името ще се използва вътрешната (последно дефинирана) променлива.
Дефиниция (свободна за формула променлива)
Нека $\varphi$ е формула. Една променлива $x$ е свободна за $\varphi$, ако $x$ има свободно участие във $\varphi$. Бележим с $\mathrm{Var}^{free}[\varphi]$ множеството на всички свободни за $\varphi$ променливи.
Аналогично - наричаме променливата $x$ свързана за $\varphi$, ако $x$ има свързано участие във $\varphi$. Бележим с $\mathrm{Var}^{bd}[\varphi]$ множеството на всички свързани за $\varphi$ променливи.
Сега остава да дефинираме по индукция $\mathrm{Var}^{free}[\varphi]$ и $\mathrm{Var}^{bd}[\varphi]$:
Дефиниция (затворена формула)
Ще наричаме предикатната формула $\varphi$ затворена, ако $\mathrm{Var}^{free}[\varphi] = \varnothing$.
Очевидно, ако $\varphi$ е затворена, и $v_1, v_2$ са оценки в $\mathcal{A}$, имаме $\|\varphi\|^\mathcal{A}[v_1] = \|\varphi\|^\mathcal{A}[v_2]$.
Твърдение (еднаквост на стойностите на формула)
Нека $v_1, v_2$ са оценки в $\mathcal{A}$ и $\varphi$ е предикатна формула.
Ако $v_1 \upharpoonright \mathrm{Var}^{free}[\varphi] = v_2 \upharpoonright \mathrm{Var}^{free}[\varphi] \quad (\star)$, то $\|\varphi\|^\mathcal{A}[v_1] = \|\varphi\|^\mathcal{A}[v_2]$.
Доказателство: Индукция по построяването на $\varphi$.
- $\varphi = p(\tau_1, \cdots, \tau_n)$, където $\tau_i$ са термове.
Нека $v_1, v_2$ удовлетворяват условието $(\star)$.
Имаме, че $\mathrm{Var}[\tau_i] \subseteq \mathrm{Var}^{free}[\varphi]$, следователно $v_1 \upharpoonright \mathrm{Var}[\tau_i] = v_2 \upharpoonright \mathrm{Var}[\tau_i]$. Прилагаме твърдението за термове и получаваме : $\| \tau_i \|^\mathcal{A}[v_1] = \| \tau_i \|^\mathcal{A}[v_2]$ (вярно за всяко $i \in \{ 1, \cdots, n \}$).
Сега разписваме $\| \varphi \|^\mathcal{A} [v_1] = \mathrm{t}$:
с което случаят е доказан.
- $\varphi =(\tau_1 \dot= \tau_2)$ - доказава се аналогично на горния случай.
- $\varphi = \lnot \psi$, като за формулата $\psi$ твърдението е вярно.
Нека $v_1, v_2$ са оценки, удовлетворяващи $(\star)$.
Понеже $\mathrm{Var}^{free}[\varphi] = \mathrm{Var}^{free}[\psi]$, имаме
първата и третата връзка идват от горното наблюдение, а втората връзка е от условието $(\star)$.
Сега имаме, че $v_1, v_2$ изпълняват условието $(\star)$ за формулата $\psi$. Следователно $\|\psi\|^\mathcal{A}[v_1] = \|\psi\|^\mathcal{A}[v_2]$.
Вече тривиално се проверява, че $\|\varphi\|^\mathcal{A} [v_1] = H_\lnot (\|\psi\|^\mathcal{A}[v_1]) = H_\lnot(\|\psi\|^\mathcal{A}[v_2]) = \|\varphi\|^\mathcal{A}[v_2]$.
- $\varphi = (\psi_1 \sigma \psi_2)$, където $\sigma \in \{ \And, \lor, \Rightarrow, \iff \}$ и за $\psi_1, \psi_2$ твърдението е вярно.
Нека $v_1, v_2$ удовлетворяват $(\star)$. Тъй като $\mathrm{Var}^{free}[\psi_j] \subseteq \mathrm{Var}^{free}[\varphi]$, следователно $v_1, v_2$ удовлетворяват $(\star)$ за формулите $\psi_1, \psi_2$, т.е $\|\psi_j\|^\mathcal{A}[v_1] = \|\psi_j\|^\mathcal{A}[v_2]$. Сега вече тривиално:
(14)с което случаят е доказан.
- $\varphi = Qx\psi$, където $Q \in \{ \exists, \forall \}$ и за $\psi$ индукционното допускане е вярно.
Нека $v_1, v_2$ удовлетворяват $(\star)$.
Нека $b \in A$ е произволно. Ще докажем, че ${v_1}_b^x \upharpoonright \mathrm{Var}^{free}[\psi] = {v_2}_b^x \upharpoonright \mathrm{Var}^{free}[\psi]$.
Нека $y \in \mathrm{Var}^{free}[\psi]$. Възможни са 2 случая:- $y = x$. Тогава ${v_1}_b^x[y] = {v_1}_b^x[x] = b = {v_2}_b^x[x] = {v_2}_b^x[y]$.
- $y \neq x$. Понеже $y \in \mathrm{Var}^{free}[\varphi]$ и от $(\star)$: $v_1[y] = v_2[y]$. От тук: ${v_1}_b^x[y] = {v_1}[y] = {v_2}[y] = {v_2}_b^x[y]$.
С това твърдението е доказано.
Нека $b \in A$ е произволен. Тогава от ${v_1}_b^x \upharpoonright \mathrm{Var}^{free}[\psi] = {v_2}_b^x \upharpoonright \mathrm{Var}^{free}[\psi]$ следва: $\|\psi\|^\mathcal{A}[{v_1}_b^x] = \|\psi\|^\mathcal{A}[{v_2}_b^x]$.
Да разгледаме двата случая за $Q$:
- $Q = \exists$. Нека $\|\varphi\|^\mathcal{A}[v_1] = \mathrm{t}$. По дефиниция това означава, че съществува елемент $a \in A$, такъв че $\|\psi\|^\mathcal{A}[{v_1}_a^x] = t$. Сега прилагаме доказаното преди малко: $\|\psi\|^\mathcal{A}[{v_1}_a^x] = \|\psi\|^\mathcal{A}[{v_2}_a^x]$, т.е получихме, че $\|\psi\|^\mathcal{A}[{v_2}_a^x] = \mathrm{t}$. Сега прилагаме наобратно дефиницията за семантиката на $\varphi$: $\|\exists x \psi\|^\mathcal{A}[v_2] = \mathrm{t}$.
- $Q = \forall$ - доказва се аналогично;
Следствие
Нека $\mathcal{A}$ е структура за $\mathcal{L}$ и $\varphi$ е затворена формула. Тогава за всеки две оценки $v_1, v_2$ от $\mathcal{A}$ имаме, че $\|\varphi\|^\mathcal{A}[v_1] = \|\varphi\|^\mathcal{A}[v_2]$.
Ако за някоя оценка $v$ е в сила $A \underset{v}\models \varphi$, то е валидно и за произволна друга оценка, затова ще записваме просто $A \models \varphi$.
Нека $\varphi$ е затворена. Тогава $\mathcal{A} \nvDash \varphi \leftrightarrow \mathcal{A} \models \lnot \varphi$. Ако $\varphi$ не е затворена имаме само, че от $\mathcal{A} \models \lnot \varphi$ следва $\mathcal{A} \nvDash \varphi$.
Определими подмножества
Дефиниция
Ще дефинираме $\varphi[[ a_1, \cdots, a_n ]]$. За сега си няма име!
Нека $\mathrm{Var}^{free}[\varphi] = \{ x_1, \cdots, x_n \}$.
Нека $a_1, \cdots, a_n \in A$.
Ако две оценки $v_1, v_2$ дават еднакви стойности на $x_1, \cdots, x_n$, то и $\mathcal{A} \underset{v_1}\models \varphi \leftrightarrow \mathcal{A} \underset{v_2}\models \varphi$.
Ако $v$ е такава оценка в $\mathcal{A}$, че $v(x_i) = a_i$, тогава дефинираме
$\varphi[[ a_1, \cdots, a_n ]] \leftrightharpoons \|\varphi\|^\mathcal{A}[v]$.
Ако $\mathcal{A} \underset{v}\models \varphi$, може да запишем $\mathcal{A} \models \varphi[[ a_1, \cdots, a_n ]]$.
Дефиниция (определимо подмножество на An)
Множеството:
(15)ще наричаме определимо подмножество на $A^n$ с формулата $\varphi$.
Ще го записваме с $D_\varphi^\mathcal{A}$.
Ако едно подмножество на $A^n$ е определимо с някоя формула $\varphi$, ще го наричаме определимо подмножество на $A^n$.
Забележка: Ако кажем определимо подмножество с формулата $\varphi$ значи акцентираме върху едно точно конкретно множество, а ако пропуснем с формулата $\varphi$, значи се интересуваме просто от факта, че множеството е определимо (но не и коя формула точно го определя).
Лема
Нека $B$ е определимо подмножество на $A^k$.
Нека $x_1, \cdots, x_k$ са различни индивидни променливи.
Тогава съществува формула $\mathrm{Var}^{free}[\varphi] = \{ x_1, \cdots, x_k \}$, такава че $B$ е определимо подмножество на $A^k$ с формулата $\varphi$.
С други думи може да преименуваме променливите на коя да е формула, определяща $B$ (тъй като $B$ е определимо), така че променливите й да са $x_1, \cdots x_k$.
Без доказателство.
Твърдение (затвореност на определимите подмножества относно операциите в булевата алгебра)
Нека $\mathcal{A}$ е структура за $\mathcal{L}$ и $k \ge 0$. Тогава определимите подмножества на $A^k$ са затворени относно операциите:
- обединение $\cup$
- сечение $\cap$
- допълнение $A^k \setminus D$
- разлика $\setminus$
- декартово произведение $\times$
Доказателство: Нека $B_1, B_2$ са определими подмножества на $A^k$. Избираме различни индивидни променливи $x_1, \cdots, x_k$. Според лемата съществуват формули $\varphi_1, \varphi_2$, такива че $\mathrm{Var}^{free}[\varphi_i] = \{ x_1, \cdots, x_k \}$ и $\varphi_i$ определя $B_i$ (за $i \in \{1 ,2 \}$).
- Сечение - да разгледаме формулата $(\varphi_1 \And \varphi_2)$ и да проверим кое множество определя тя:
Така получихме, че всъщност формулата $(\varphi_1 \And \varphi_2)$ определя множеството $B_1 \cap B_2$.
- Обединение - абсолютно аналогично на горния случай, но формулата е $(\varphi_1 \lor \varphi_2)$.
- Допълнение - аналогично на горния случай, формулата е $\varphi = \lnot \varphi_1$. (т.е ако $\varphi_1$ определя $B_1$, то $\lnot \varphi_1$ определя $A^k \setminus B_1$.
- Разлика - аналогично, формулата е $(\varphi_1 \And \lnot \varphi_2)$ (това може да се докаже и с използване на сечение и допълнение).
- Декартово произведение - нека $B, C$ са определими подмножества на $A^n$ и $A^k$ съответно. Според лемата съществуват формули $\varphi, \psi$, такива че $\mathrm{Var}^{free}[\varphi] = \{ x_1, \cdots, x_n \}$ и $\mathrm{Var}^{free}[\psi] = \{y_1, \cdots, y_k \}$, където $x$овете и $y$ците са различни индивидни променливи (общо $n + k$ различни променливи). Да разгледаме формулата $(\varphi \And \psi)$. Нейните свободни променливи са $\{ x_1, \cdots, x_n \} \cup \{ y_1, \cdots, y_k \}$, т.е може да приемем, че формулата $\varphi$ определя множеството $B \times A^k$ (т.е определя $B$, а останлите променливи (y-ците) не ни интересуват — по-точно каквито и да са y-ците, ако x-овете удовлетворяват формулата, значи и заедно с y-ците също я удовлетворяват). Сега правим и същото разсъждение за $\psi$ - тя определя множеството $A^n \times C$, и сега прилагаме сечение върху двете (защото $\And$ във формули се превежда в сечение на определящите ги множества) и получаваме: $(B \times A^k) \cap (A^n \times C) = B \times C$, с което твърдението е доказано.
Пример
Примерите са за женчовци - който иска да въведе примера с $\langle \mathbb{N}, \le \rangle$, и как се определят някои конкретни множества.
Твърдение
Определимите множества са или крайни, или допълнение на крайни. (неофициално)
Изоморфизъм
Дефиниция (изоморфизъм на структури)
Нека $\mathcal{A}, \mathcal{B}$ са структури за $\mathcal{L}$ с формално равенство. Казваме, че $h$ е изоморфизъм на $\mathcal{A}$ върху $\mathcal{B}$, ако:
- $h : A \to B$ - биекция
- $h(c^\mathcal{A}) = c^\mathcal{B}$
- $\langle a_1, \cdots, a_n \rangle \in p^\mathcal{A} \leftrightarrow \langle h(a_1), \cdots, h(a_n) \rangle \in p^\mathcal{B}$
- $f^\mathcal{A} (a_1, \cdots, a_n) = b \leftrightarrow f^\mathcal{B} (h(a_1), \cdots, h(a_n)) = h(b)$.
Твърдение (изоморфизъм на термове и формули)
Нека $\mathcal{A}, \mathcal{B}$ са структури за $\mathcal{L}$ с формално равенство. Нека $h$ е изоморфизъм на $\mathcal{A}$ върху $\mathcal{B}$.
(1) За всеки терм $\tau$ е изпълнено: $h(\tau^\mathcal{A}[[a_1, \cdots, a_n]]) = \tau^\mathcal{B}[[h(a_1), \cdots, h(a_n)]]$.
(2) За всяка формула $\varphi$ е изпълнено $\mathcal{A} \models \varphi [[a_1, \cdots, a_n ]] \leftrightarrow \mathcal{B} \models \varphi[[h(a_1), \cdots, h(a_n) ]]$.
Доказателство:
(1) Индукция по построението на $\tau$:
- $\tau = x$
- $\tau = c$
- $\tau = f(\tau_1, \cdots, \tau_k)$ и за $\tau_1, \cdots, \tau_k$ твърдението е вярно.
(2) Индукция по построението на $\varphi$
- $\varphi = p(\tau_1, \cdots, \tau_k)$
Единственото, което се използва тук, са дефинициите за изоморфизъм и доказаното в предната точка твърдение за термове.
- $\varphi = (\tau_1 \dot= \tau_2)$ - аналогично на горния случай
- $\varphi = \lnot \psi$ и за $\psi$ твърдението е вярно, т.е $\mathcal{A} \models \psi[[a_1, \cdots, a_n]] \leftrightarrow \mathcal{B} \models \psi[[h(a_1), \cdots, h(a_n)]]$:
- $\varphi = \psi_1 \And \psi_2$
- за $\lor, \Rightarrow, \iff$ се доказва напълно аналогично на горното.
- $\varphi = \exists x \psi$ и нека твърдението е вярно за $\psi$.
Нека $\mathcal{A} \models \varphi[[a_1, \cdots, a_n]]$. Избираме си оценка на предикатната променлива $x$, за която формулата е вярна - нека я кръстим $a$. Следователно $\mathcal{A} \models \psi[[a_1, \cdots, a_n, a]]$. От индукционната хипотеза имаме, че $\mathcal{B} \models \psi[[h(a_1), \cdots, h(a_n), h(a) ]]$, следователно и $\mathcal{B} \models \exists x \psi [[h(a_1), \cdots, h(a_n)]]$ (защото съществува обект от универсума $h(a) \in B$, такъв че $\psi$ да е изпълнено)
Сега в обратната посока: Нека $\mathcal{B} \models \varphi[[h(a_1), \cdots, h(a_n)]]$, т.е $\mathcal{B} \models \exists x \psi[[h(a_1), \cdots, h(a_n)]]$. Избираме си $b \in B$, за което $\mathcal{B} \models \psi [[h(a_1), \cdots, h(a_n), b ]]$. Понеже $h$ е биекция, съществува $a$ , такова че $h(a) = b$. Прилагаме индукционното предположение за $\psi$ и получаваме, че $\mathcal{A} \models \psi [[a_1, \cdots, a_n, a]]$, от където и $\mathcal{A} \models \exists x \psi [[a_1, \cdots, a_n]]$.
- $\varphi = \forall x \psi$ - аналогично на горното.
Твърдение (обръщане на изоморфизма)
Ако $h$ е изоморфизъм на $\mathcal{A}$ върху $\mathcal{B}$, то $h^{-1}$ е изоморфизъм на $\mathcal{B}$ върху $\mathcal{A}$.
Доказателство: Доказва се тривиално, с факта че $h$ е биекция и дефиницията за изоморфизъм.
Твърдение (транзитивност на изоморфизмите)
Нека $h_1$ е изоморфизъм на $\mathcal{A}$ върху $\mathcal{B}$ и $h_2$ е изоморфизъм на $\mathcal{B}$ върху $\mathcal{C}$. Тогава функцията $h = h_2 \circ h_1$ (т.е прилагаме функцията $h_2$ след функцията $h_1$) е изоморфизъм на $\mathcal{A}$ върху $\mathcal{C}$.
Доказателство: Доказва се тривиално с дефиницията.
Автоморфизъм
Дефиниция (автоморфизъм)
Нека $\mathcal{A}$ е структура. Автоморфизъм в $\mathcal{A}$ наричаме всеки изоморфизъм $h$ на $\mathcal{A}$ върху $\mathcal{A}$.
Най-простия пример за автоморфизъм е идентитета на универсума $\mathrm{Id}_A : A \to A$, т.е $\mathrm{Id}_A(a) = a$.
Твърдение (затвореност на определимите множества спрямо автоморфизми)
Нека $h$ е автоморфизъм в $\mathcal{A}$ и $D \subseteq A^n$ е определимо в $\mathcal{A}$. Тогава ако $\langle a_1, \cdots, a_n \rangle \in D$, то $\langle h(a_1), \cdots, h(a_n) \rangle \in D$.
Доказателство: Нека $\varphi$ е формула определяща $D$ в $\mathcal{A}$. Това означава, че $\langle a_1, \cdots, a_n \rangle \in D$ е равносилно на $\mathcal{A} \models \varphi [[a_1, \cdots, a_n ]]$. Сега използваме, че $h$ е всъщност изоморфизъм на $\mathcal{A}$ върху $\mathcal{A}$ и от доказаното в предната точка твърдение получаваме, че $\mathcal{A} \models \varphi[[ h(a_1), \cdots, h(a_n) ]]$. което е равносилно на $\langle h(a_1), \cdots, h(a_n) \rangle \in D$.
Следствие (необходимо условие за определимо множество)
Нека $\mathcal{A}$ е структура и $h$ е автоморфизъм в нея. $D \subseteq A^k$ е произволно множество. Тогава ако съществува елемент $d \in D$, такъв че $h(d) \notin D$ следователно $D$ не е определимо в $\mathcal{A}$.
Примери
- $\langle \mathbb{N}, \le \rangle$ - тук само $\mathrm{Id}_A$ е изоморфизъм. Това обаче не означава, че ако вземем едно произволно подмножество на $\mathbb{N}$ (например множеството на простите числа), то е определимо само защото не съществува изоморфизъм който да го 'измести' в друго множество (горното свойство не е вярно наобратно).
- $\langle \mathbb{Z}, \le \rangle$ - $h$ е автоморфизъм т.с.т.к $h(a) = a + l$, за някое рационално $l$. От тук директно получаваме, че никое крайно подмножество не е определимо.
- $\langle \mathbb{Q}, \le \rangle$ - континуум много на брой автоморфизми - $2^{\aleph_0}$ на брой. Бтв при автоморфизмите важи континуум хипотезата - няма структура, която има брой автоморфизми, който е междинна мощност между две съседни $\aleph$.2
Дефиниция (изпълнима формула)
Нека $\varphi$ е формула. Казваме, че $\varphi$ e изпълнима, ако съществува структура $\mathcal{A}$ и оценка $v$, такава че $\mathcal{A} \underset{v}\models \varphi$.
По друг начин казано, съществува структура $\mathcal{A}$, за която множеството определимо с $\varphi$ е непразно : $D_\varphi^\mathcal{A} \neq \varnothing$.
Дефиниция (неизпълнима формула)
Нека $\varphi$ е формула. Казваме, че $\varphi$ е неизпълнима, ако не е изпълнима, т.е за всяка структура $\mathcal{A}$ е изпълнено, че $D_\varphi^\mathcal{A} = \varnothing$.
Дефиниция (предикатна тавтология)
Нека $\varphi$ е формула. Казваме, че тя е предикатна тавтология и записваме $\models \varphi$, ако за всяка структура $\mathcal{A}$ и за всяка оценка $v$ е изпълнено $\mathcal{A} \underset{v}\models \varphi$, или другояче казaно $D_\varphi^\mathcal{A} = A^n$, където $n = |\mathrm{Var}^{free}[\varphi]|$.
Твърдение
$\varphi$ е предикатна тавтология, т.с.т.к. $\lnot \varphi$ е неизпълнима.
Доказателство: Очевидно!
Дефиниция (вярна формула)
Ако $\mathcal{A}$ е структура и $\varphi$ е формула, казваме че $\varphi$ е вярна в $\mathcal{A}$, ако за всяка оценка $v$ в $\mathcal{A}$ e изпълнено $\mathcal{A} \underset{v}\models \varphi$. Записваме $\mathcal{A} \models \varphi$.
Забележка: Предикатна тавтология vs. вярна формула - вярна е формула в контекст на дадена структура. Ако е вярна една формула при всяка структура, то тя е предикатна тавтология, или по друг начин казано - само разглеждайки буквичките на формулата, без да си представяме каквото и да е под различните функции, предикати и константи, написаното е вярно. Не може да напишете нещо супер интересно, което е предикатна тавтология - просто ще бъде доста 'очевидно', или - както и да го гледате все ще е вярно ;-).
Забележка: От $\mathcal{A} \nvDash \varphi$ не следва $\mathcal{A} \models \lnot \varphi$. В единия случай трябва да съществува оценка за която $\varphi$ не е вярна, а в другия трябва за всяка оценка $\lnot \varphi$ да е вярна (т.е $\varphi$ да не е вярна).
Твърдение
Ако $\varphi$ е затворена формула, то $\mathcal{A} \nvDash \varphi$ е равносилно на $\mathcal{A} \models \lnot \varphi$.