Предикатни формули. Семантика на предикатни формули, определими подмножества, изображения

Предикатни формули

Дефиниция (атомарна формула)

Нека $\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)

\begin{array} {rcl} H_\lnot(\mathrm{t}) &=& \mathrm{f} \\ H_\lnot(\mathrm{f}) &=& \mathrm{t} \\ \end{array}\begin{array}{|rcl} H_{\And}(\mathrm{t}, \mathrm{t}) &=& \mathrm{t} \\ H_{\And}(\mathrm{t}, \mathrm{f}) &=& \mathrm{f} \\ H_{\And}(\mathrm{f}, \mathrm{t}) &=& \mathrm{f} \\ H_{\And}(\mathrm{f}, \mathrm{f}) &=& \mathrm{f} \\ \end{array}\begin{array}{|rcl} H_{\lor}(\mathrm{t}, \mathrm{t}) &=& \mathrm{t} \\ H_{\lor}(\mathrm{t}, \mathrm{f}) &=& \mathrm{t} \\ H_{\lor}(\mathrm{f}, \mathrm{t}) &=& \mathrm{t} \\ H_{\lor}(\mathrm{f}, \mathrm{f}) &=& \mathrm{f} \\ \end{array}\begin{array}{|rcl} H_{\Rightarrow}(\mathrm{t}, \mathrm{t}) &=& \mathrm{t} \\ H_{\Rightarrow}(\mathrm{t}, \mathrm{f}) &=& \mathrm{f} \\ H_{\Rightarrow}(\mathrm{f}, \mathrm{t}) &=& \mathrm{t} \\ H_{\Rightarrow}(\mathrm{f}, \mathrm{f}) &=& \mathrm{t} \\ \end{array}\begin{array}{|rcl} H_{\iff}(\mathrm{t}, \mathrm{t}) &=& \mathrm{t} \\ H_{\iff}(\mathrm{t}, \mathrm{f}) &=& \mathrm{f} \\ H_{\iff}(\mathrm{f}, \mathrm{t}) &=& \mathrm{f} \\ H_{\iff}(\mathrm{f}, \mathrm{f}) &=& \mathrm{t} \\ \end{array}

Дефиниция (модифицирана оценка)

Оценка v, модифицирана в точка х с а:

(2)

\begin{align} v_a^x[y] = \begin{cases} a & y = x \\ v(y) & y \ne x \\ \end{cases} \end{align}

Дефиниция (стойност на предикатна формула)

Подобно на стойност на терм ще дефинираме и стойност на формула.
Нека $\mathcal{A}$ е структура, $v$ е оценка в нея и $\varphi$ е предикатна формула.
Ще отбелязваме стойност на $\varphi$ при оценка $v$ по следния начин:

(3)

\begin{align} \|\varphi\|^\mathcal{A}[v] \end{align}

Разбира се, $\|\varphi\|^\mathcal{A}[v] \in \{ \mathrm{t}, \mathrm{f} \}$.
Сега ще направим индуктивна дефиниция за самата стойност, според конструкцията на $\varphi$:

• Нека $\varphi = p(\tau_1, \cdots, \tau_n)$ е атомарна формула. Дефинираме

(4)

\begin{align} \|p(\tau_1, \cdots, \tau_n)\|^\mathcal{A}[v] = \mathrm{t} \leftrightharpoons \langle \|\tau_1\|^\mathcal{A}[v], \cdots, \|\tau_n\|^\mathcal{A}[v] \rangle \in p^\mathcal{A} \end{align}

• Нека $\varphi = (\tau_1 \dot= \tau_2)$ е атомарна формула. Дефинираме

(5)

\begin{align} \|(\tau_1 \dot= \tau_2)\|^\mathcal{A}[v] = \mathrm{t} \leftrightharpoons \|\tau_1\|^\mathcal{A}[v] = \|\tau_2\|^\mathcal{A}[v] \end{align}

• Нека $\varphi = \lnot \psi$, където $\psi$ е предикатна формула. Дефинираме

(6)

\begin{align} \|\lnot\psi\|^\mathcal{A}[v] \leftrightharpoons H_\lnot(\|\psi\|^\mathcal{A}[v]) \end{align}

• Нека $\varphi = (\psi_1 \sigma \psi_2)$, където $\psi_1, \psi_2$ са предикатни формули, а $\sigma \in \{ \And, \lor, \Rightarrow, \iff \}$. Дефинираме

(7)

\begin{align} \|\psi_1 \sigma \psi_2\|^\mathcal{A}[v] \leftrightharpoons H_{\sigma}(\|\psi_1\|^\mathcal{A}[v], \|\psi_2\|^\mathcal{A}[v]) \end{align}

• Нека $\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)

\begin{eqnarray} \|\varphi\|^\mathcal{A}[v] = \mathrm{t} &\longleftrightarrow& \mathcal{A} \underset{v}\models \varphi \\ \|\varphi\|^\mathcal{A}[v] = \mathrm{f} &\longleftrightarrow& \mathcal{A} \underset{v}\nvDash \varphi \\ \end{eqnarray}

Област на действие на квантор

Дефиниция (област на действие на квантор)

Нека $\varphi$ е формула, $Q$ е квантор (т.е $Q \in \{ \forall, \exists \}$) и нека $\varphi = \alpha Q \beta$ е участие¹ на квантора $Q$ в $\varphi$. Тогава съществува единствена индивидна променлива $x$ и единствена предикатна формула $\psi$, такива че $\varphi = \alpha Qx\psi\beta'$. Това участие на $x\psi$ се нарича област на действие на участието $\alpha Q\beta$ на $Q$ във $\varphi$. Казваме, че това участие на $Q$ е по индивидната променлива $x$.

Пример

(9)

\begin{eqnarray} (p(f(x), g(y, c)) \And \forall \underbrace{x (r(z) \Rightarrow q(g(x, f(c))))}) \\ (p(x) \lor \exists \underbrace{y(\exists \underbrace{x r(x)} \And p(y))}) \end{eqnarray}

Дефиниция (свързано участие на индивидна променлива)

Едно участие на индивидната променлива $x$ се нарича свързано участие, ако то е в област на действие на квантор по $x$. Иначе това участие на $x$ се нарича свободно участие.

Пример

(10)

\begin{eqnarray} (\forall \underbrace{x (p(x) \lor \exists \underbrace{x(q(x) \And \forall \underbrace{x r(x)})})}) \end{eqnarray}

В този случай всяко участие на индивидната променливата $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]$:

(11)

\begin{array} {rcl} \mathrm{Var}^{free}[p(\tau_1, \cdots, \tau_n)] &=& \bigcup_{i=1}^{n} \mathrm{Var}[\tau_i] \\ \mathrm{Var}^{free}[(\tau_1 \dot= \tau_2)] &=& \mathrm{Var}[\tau_1] \cup \mathrm{Var}[\tau_2] \\ \mathrm{Var}^{free}[\lnot \varphi] &=& \mathrm{Var}^{free}[\varphi] \\ \mathrm{Var}^{free}[(\varphi \sigma \psi)] &=& \mathrm{Var}^{free}[\varphi] \cup \mathrm{Var}^{free}[\psi] \\ \mathrm{Var}^{free}[Qx\varphi] &=& \mathrm{Var}^{free}[\varphi] \setminus \{x\} \\ \end{array}\begin{array}{rcl} \mathrm{Var}^{bd}[p(\tau_1, \cdots, \tau_n)] &=& \varnothing \\ \mathrm{Var}^{bd}[(\tau_1 \dot= \tau_n)] &=& \varnothing \\ \mathrm{Var}^{bd}[\lnot \varphi] &=& \mathrm{Var}^{bd}[\varphi] \\ \mathrm{Var}^{bd}[(\varphi \sigma \psi)] &=& \mathrm{Var}^{bd}[\varphi] \cup \mathrm{Var}^{bd}[\psi]\\ \mathrm{Var}^{bd}[Qx\varphi] &=& \mathrm{Var}^{bd}[\varphi] \cup \{x\}\\ \end{array}

Дефиниция (затворена формула)

Ще наричаме предикатната формула $\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}$:

(12)

\begin{eqnarray} \| \varphi \|^\mathcal{A} [v_1] = \mathrm{t} &\leftrightarrow& \langle \|\tau_1\|^\mathcal{A}[v_1], \cdots, \|\tau_n\|^\mathcal{A}[v_1] \rangle \in p^\mathcal{A} \\ &\leftrightarrow& \langle \|\tau_1\|^\mathcal{A}[v_2], \cdots, \|\tau_n\|^\mathcal{A}[v_2] \rangle \in p^\mathcal{A} \\ &\leftrightarrow& \|\varphi\|^\mathcal{A} [v_2] = \mathrm{t} \end{eqnarray}

с което случаят е доказан.

• $\varphi =(\tau_1 \dot= \tau_2)$ - доказава се аналогично на горния случай.
• $\varphi = \lnot \psi$, като за формулата $\psi$ твърдението е вярно.

Нека $v_1, v_2$ са оценки, удовлетворяващи $(\star)$.
Понеже $\mathrm{Var}^{free}[\varphi] = \mathrm{Var}^{free}[\psi]$, имаме

(13)

\begin{eqnarray} v_1 \upharpoonright \mathrm{Var}^{free}[\psi] &=& v_1 \upharpoonright \mathrm{Var}^{free}[\varphi] \\ &\overset{\underset{(\star)}{}}=& v_2 \upharpoonright \mathrm{Var}^{free}[\varphi] \\ &=& v_2 \upharpoonright \mathrm{Var}^{free}[\psi] \\ \end{eqnarray}

първата и третата връзка идват от горното наблюдение, а втората връзка е от условието $(\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)

\begin{eqnarray} \|\varphi\|^\mathcal{A}[v_1] &=& H_\sigma(\|\psi_1\|^\mathcal{A}[v_1], \|\psi_2\|^\mathcal{A}[v_1]) \\ &=& H_\sigma(\|\psi_1\|^\mathcal{A}[v_2], \|\psi_2\|^\mathcal{A}[v_2]) \\ &=& \|\varphi\|^\mathcal{A}[v_2] \end{eqnarray}

с което случаят е доказан.

• $\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 ]]$.

Дефиниция (определимо подмножество на Aⁿ)

Множеството:

(15)

\begin{align} \{ \langle a_1, \cdots, a_n \rangle | \mathcal{A} \models \varphi [[a_1, \cdots, a_n ]] \} \end{align}

ще наричаме определимо подмножество на $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)$ и да проверим кое множество определя тя:

(16)

\begin{eqnarray} \mathcal{A} \models (\varphi_1 \And \varphi_2) [[ a_1, \cdots, a_k ]] &\leftrightarrow& \mathcal{A} \models \varphi_1 [[a_1, \cdots, a_k]] \mbox{ and } \mathcal{A} \models \varphi_2 [[a_1, \cdots, a_k]] \\ &\leftrightarrow& \langle a_1, \cdots, a_k \rangle \in B_1 \mbox{ and } \langle a_1, \cdots, a_k \rangle \in B_2 \\ &\leftrightarrow& \langle a_1, \cdots, a_k \rangle \in B_1 \cap B_2 \\ \end{eqnarray}

Така получихме, че всъщност формулата $(\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$

(17)

\begin{align} h(\tau^\mathcal{A}[[a]]) = h(a) = \tau^\mathcal{B}[[h(a)]] \end{align}

• $\tau = c$

(18)

\begin{align} h(\tau^\mathcal{A}) = h(c^\mathcal{A}) = c^\mathcal{B} = \tau^\mathcal{B} \end{align}

• $\tau = f(\tau_1, \cdots, \tau_k)$ и за $\tau_1, \cdots, \tau_k$ твърдението е вярно.

(19)

\begin{eqnarray} h(\tau^\mathcal{A} [[a_1, \cdots, a_n]]) &=& h(f^\mathcal{A}(\tau_1^\mathcal{A}[[a_1, \cdots, a_n]], \cdots, \tau_k^\mathcal{A}[[a_1, \cdots, a_n]])) \\ &=& f^\mathcal{B} (h(\tau_1^\mathcal{A}[[a_1, \cdots, a_n]]), \cdots, h(\tau_k^\mathcal{A}[[a_1, \cdots, a_n]])) \\ &=& f^\mathcal{B}(\tau_1^\mathcal{B}[[h(a_1), \cdots, h(a_n)]], \cdots, \tau_k^\mathcal{B}[[h(a_1), \cdots, h(a_n)]]) \\ &=& \tau^\mathcal{B} [[h(a_1), \cdots, h(a_n)]] \\ \end{eqnarray}

(2) Индукция по построението на $\varphi$

• $\varphi = p(\tau_1, \cdots, \tau_k)$

(20)

\begin{eqnarray} \mathcal{A} \models \varphi[[a_1, \cdots, a_n ]] &\leftrightarrow& \mathcal{A} \models p(\tau_1, \cdots, \tau_k)[[ a_1, \cdots, a_n ]] \\ &\leftrightarrow& \langle \tau_1^\mathcal{A}[[a_1, \cdots, a_n]], \cdots, \tau_k^\mathcal{A}[[a_1, \cdots, a_n]] \rangle \in p^\mathcal{A} \\ &\leftrightarrow& \langle h(\tau_1^\mathcal{A}[[a_1, \cdots, a_n]]), \cdots, h(\tau_k^\mathcal{A}[[a_1, \cdots, a_n]]) \rangle \in p^\mathcal{B} \\ &\leftrightarrow& \langle \tau_1^\mathcal{B} [[h(a_1), \cdots, h(a_n)]], \cdots, \tau_k^\mathcal{B} [[h(a_1), \cdots, h(a_n)]] \rangle \in p^\mathcal{B} \\ &\leftrightarrow& \mathcal{B} \models p(\tau_1, \cdots, \tau_k)[[h(a_1), \cdots, h(a_n)]] \\ &\leftrightarrow& \mathcal{B} \models \varphi[[ h(a_1), \cdots, h(a_n)]] \end{eqnarray}

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

• $\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)]]$:

(21)

\begin{eqnarray} \mathcal{A} \models \varphi[[a_1, \cdots, a_n ]] &\leftrightarrow& \mathcal{A} \nvDash \psi [[a_1, \cdots, a_n]] \\ &\leftrightarrow& \mathcal{B} \nvDash \psi [[h(a_1), \cdots, h(a_n)]] \\ &\leftrightarrow& \mathcal{B} \models \varphi [[h(a_1), \cdots, h(a_n)]] \\ \end{eqnarray}

• $\varphi = \psi_1 \And \psi_2$

(22)

\begin{eqnarray} \mathcal{A} \models \varphi[[a_1, \cdots, a_n]] &\leftrightarrow& \mathcal{A} \models \psi_1[[a_1, \cdots, a_n]] \mbox{ and } \mathcal{A} \models \psi_2[[a_1, \cdots, a_n]] \\ &\leftrightarrow& \mathcal{B} \models \psi_1[[h(a_1), \cdots, h(a_n)]] \mbox{ and } \mathcal{B} \models \psi_2[[h(a_1), \cdots, h(a_n)]] \\ &\leftrightarrow& \mathcal{B} \models \varphi [[h(a_1), \cdots, h(a_n)]] \end{eqnarray}

• за $\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$.²

Дефиниция (изпълнима формула)

Нека $\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$.

Footnotes

1. демек формулата е 'нещо в началото'=алфа, квантора, 'нещо в края'=бета

2. това е за обща култура - няма да го има на изпита, дишай спокойно