Ербранови Структури

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


Ербранови структури

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

Нека $\mathcal{L}$ е език от 1ви ред и $\mathcal{L}$ има поне една индивидна константа. За една структура $\mathcal{A}$ казваме, че е ербранова, ако:

  • $A = \mathcal{T}_\mathcal{L}^{cl}$ - затворени термове
  • $c^\mathcal{A} = c$
  • $f^\mathcal{A}(\tau_1, \dots, \tau_n) = f(\tau_1, \dots, \tau_n)$

Пример

Ако в езика има само една индивидна константа и никакви функции: $A = \{ c^\mathcal{A} \}$.
Ако в езика има една константа и една унарна функция $f$: $A = \{ c, f(c), \dots, f(f(\dots f(c)\dots )), \dots \}$.

Лема 1

Нека $\mathcal{A}$ е Ербранова структура за $\mathcal{L}$, който има поне една индивидна константа1, тогава за всеки затворен терм $\tau$ имаме, че $\| \tau \|^\mathcal{A} = \tau$.
Доказателство: Ще направим индукция по построението на $\tau$ (който е затворен терм - т.е няма индивидни променливи):
(1) $\tau = c$, където $c$ е индивидна константа. Тогава $\| \tau \|^\mathcal{A} = \| c \|^\mathcal{A} = c^\mathcal{A} = c = \tau$
(2) $\tau = f(\tau_1, \dots, \tau_n)$, където $\tau_1, \dots, \tau_n$ са затворени термове, за които твърдението е доказано:

(1)
\begin{eqnarray} \| f(\tau_1, \dots, \tau_n) \|^\mathcal{A} &=& f^\mathcal{A}(\|\tau_1\|^\mathcal{A}, \dots, \| \tau_n\|^\mathcal{A}) \\ &=& f^\mathcal{A}(\tau_1, \dots, \tau_n) \\ &=& f(\tau_1, \dots, \tau_n) \\ &=& \tau \\ \end{eqnarray}

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

Нека $\mathcal{A}$ е ербранова структура за $\mathcal{L}$. Тогава ако $v$ е оценка в $\mathcal{A}$ и $x \in \mathrm{Var}$: $v(x) = \tau$, за някой затворен терм $\tau$.

Следствие

(2)
\begin{align} \| \tau \|^\mathcal{A}[v] = \tau[ x_1/v(x_1), \dots, x_n/v(x_n)] \quad \mathrm{Var}[\tau] = \{ x_1, \dots, x_n \} \end{align}

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

Казваме, че $\mathcal{A}$ е свободна ербранова структура за $\mathcal{L}$, ако:

  • $A = \mathcal{T}_\mathcal{L}$ - универсума са всички термове (не само затворените)
  • $c^\mathcal{A} = c$
  • $f^\mathcal{A}(\tau_1, \dots, \tau_n) = f(\tau_1, \dots, \tau_n)$

Лема 2

Нека $\mathcal{A}$ е свободна ербранова структура за $\mathcal{L}$. Тогава за всеки терм $\tau$ е изпълнено:
(1) $\| \tau \|^\mathcal{A}[\mathrm{id}_A] = \tau$
(2) $\| \tau \|^\mathcal{A}[v] = \tau[ x_1/v(x_1), \dots, x_n/v(x_n) ] \quad \mathrm{Var}[\tau] = \{ x_1, \dots, x_n \}$
Доказателство:
(1) Използваме доказателството на Лема 1. Остава само случая, в който $\tau = x$, където $x$ е индивидна променлива. В този случай $\| \tau \|^\mathcal{A} [\mathrm{id}_A] = \| x \|^\mathcal{A} [\mathrm{id}_A] = \mathrm{id}_A(x) = x = \tau$
(2) Ще направим индукция по построението на $\tau$.
(2.1) $\tau = x$. $\| x \|^\mathcal{A}[v] = v(x) = x[x/v(x)]$
(2.2) $\tau = c$. $\| c \|^\mathcal{A}[v] = c^\mathcal{A} = c[]$ - тук просто няма индивидни променливи $\mathrm{Var}[c] = \varnothing$
(2.3) $\tau = f(\tau_1, \dots, \tau_n)$. Разбира се $\mathrm{Var}[\tau_i] \subseteq \mathrm{Var}[\tau] = \{ x_1, \dots x_n \}$:

(3)
\begin{eqnarray} \| f(\tau_1, \dots, \tau_n) \|^\mathcal{A} [v] &=& f^\mathcal{A}(\|\tau_1\|^\mathcal{A}[v], \dots, \|\tau_n\|^\mathcal{A}[v]) \\ &=& f^\mathcal{A}(\tau_1[x_1/v(x_1), \dots, x_n/v(x_n)], \dots, \tau_n[x_1/v(x_1), \dots, x_n/v(x_n)]) \\ &=& f(\tau_1[x_1/v(x_1), \dots, x_n/v(x_n)], \dots, \tau_n[x_1/v(x_1), \dots, x_n/v(x_n)]) \\ &=& f(\tau_1, \dots, \tau_n)[x_1/v(x_1), \dots, x_n/v(x_n)] \\ &=& \tau[x_1/v(x_1), \dots, x_n/v(x_n)] \\ \end{eqnarray}

Твърдение

Нека $\mathcal{A}$ е свободна ербранова структура за език без формално равенство, $v$ е оценка в $\mathcal{A}$ и $\varphi$ е безкванторна формула. Тогава

(4)
\begin{align} \mathcal{A} \underset{v}\models \varphi \leftrightarrow \mathcal{A} \underset{\mathrm{id}}\models \varphi[x_1/v(x_1), \dots, x_n/v(x_n)] \quad \mathrm{Var}^{free}[\varphi] = \{ x_1, \dots, x_n \} \end{align}

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

(5)
\begin{eqnarray} \mathcal{A} \underset{v}\models p(\tau_1, \dots, \tau_n) &\leftrightarrow& \langle \| \tau_1 \|^\mathcal{A}[v], \dots, \| \tau_n \|^\mathcal{A}[v] \rangle \in p^\mathcal{A} \\ &\leftrightarrow& \langle \tau_1[x_1/v(x_1), \dots, x_n/v(x_n)], \dots, \tau_n[x_1/v(x_1), \dots, x_n/v(x_n)] \rangle \in p^\mathcal{A} \\ &\leftrightarrow& \langle \|\tau_1[x_1/v(x_1), \dots, x_n/v(x_n)]\|^\mathcal{A}[\mathrm{id}_A], \dots, \|\tau_n[x_1/v(x_1), \dots, x_n/v(x_n)]\|^\mathcal{A}[\mathrm{id}_A] \rangle \in p^\mathcal{A} \\ &\leftrightarrow& \mathcal{A} \underset{\mathrm{id}_A}\models p(\tau_1, \dots, \tau_n)[x_1/v(x_1), \dots, x_n/v(x_n) ] \end{eqnarray}

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

(6)
\begin{eqnarray} \mathcal{A} \underset{v}\models \varphi &\leftrightarrow& \mathcal{A} \underset{v}\models \lnot\psi \\ &\leftrightarrow& \mathcal{A} \underset{v}\nvDash \psi \\ &\leftrightarrow& \mathcal{A} \underset{\mathrm{id}_A}\nvDash \psi[x/v(x)] \\ &\leftrightarrow& \mathcal{A} \underset{\mathrm{id}_A}\models \lnot \psi [x/v(x)] \\ &\leftrightarrow& \mathcal{A} \underset{\mathrm{id}_A}\models \varphi[x/v(x)] \\ \end{eqnarray}

(3) $\varphi = \psi_1 \sigma \psi_2$, където $\sigma \in \{ \And, \lor, \Rightarrow, \iff \}$.

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

Твърдения

Сега следват няколко изсипани ей така твърдения, който се доказват с помощта на разгледаните по-горре твърдения/леми.

Нека $\varphi = \forall x_1 \dots \forall x_n \theta$, където $x_1, \dots, x_n$ са различни индивидни променливи, а $\theta$ е безкванторна.

  • Нека $\mathcal{A}$ е структура, $v$ оценка в нея.
(8)
\begin{eqnarray} \mathcal{A} \underset{v}\models \forall x_1 \dots \forall x_n \theta &\leftrightarrow& \mbox{for all } \langle a_1, \dots, a_n \rangle \in A^n \quad \mathcal{A} \underset{v^{x_1 \dots x_n}_{a_1 \dots a_n}}\models \theta \end{eqnarray}
  • Нека $\mathcal{A}$ е свободна ербранова структура.
(9)
\begin{eqnarray} \mathcal{A} \underset{v}\models \forall x_1 \dots \forall x_n \theta &\leftrightarrow& \mbox{for all }\langle \tau_1, \dots, \tau_n \rangle \in (\mathcal{T}_\mathcal{L})^n \quad \mathcal{A} \underset{v^{x_1 \dots x_n}_{\tau_1 \dots \tau_n}}\models \theta \\ &\leftrightarrow& \mbox{for all } \langle \tau_1, \dots, \tau_n \rangle \in (\mathcal{T}_\mathcal{L})^n \quad \mathcal{A} \underset{\mathrm{id}_A}\models \theta[x_1/v^{x_1 \dots x_n}_{\tau_1 \dots \tau_n}(x_1), \dots, x_n/v^{x_1 \dots x_n}_{\tau_1 \dots \tau_n}(x_n)] \\ &\leftrightarrow& \mbox{for all }\langle \tau_1, \dots, \tau_n \rangle \in (\mathcal{T}_\mathcal{L})^n \quad \mathcal{A} \underset{\mathrm{id}_A}\models \theta[x_1/\tau_1, \dots, x_n/\tau_n] \\ \end{eqnarray}
  • Нека $\mathcal{A}$ е ербранова структура.
(10)
\begin{eqnarray} \mathcal{A} \models \forall x_1 \dots \forall x_n \theta &\leftrightarrow& \mbox{for all } \langle \tau_1 \dots \tau_n \rangle \in (\mathcal{T}_\mathcal{L}^{cl})^n \quad \mathcal{A} \models \theta[x_1/\tau_1, \dots, x_n/\tau_n] \end{eqnarray}

Дефиниция (частни случаи)

Нека $\varphi = \forall x_1 \dots \forall x_n \theta$ е затворена универсална формула, където $x_1, \dots, x_n$ са различни индивидни променливи, а $\theta$ е безкванторна.

(11)
\begin{align} \mathrm{Si}(\varphi) = \{ \theta[x_1/\tau_1, \dots, x_n/\tau_n] | \tau_1, \dots, \tau_n \in \mathcal{T}_\mathcal{L} \} \end{align}

се наричат частни случаи на формулата $\varphi$.

(12)
\begin{align} \mathrm{CSi}(\varphi) = \{ \theta[x_1/\tau_1, \dots, x_n/\tau_n] | \tau_1, \dots, \tau_n \in \mathcal{T}_\mathcal{L}^{cl} \} \end{align}

се наричат затворени частни случаи на формулата $\varphi$.

Горните твърдения могат да се препишат с използването на новите означения:

  • $\mathcal{A}$ е свободна ербранова структура, а $\varphi$ е затворена универсална формула. Тогава
(13)
\begin{align} \mathcal{A} \models \varphi \leftrightarrow \mathcal{A} \underset{\mathrm{id}_A}\models \mathrm{Si}(\varphi) \end{align}
  • $\mathcal{A}$ е ербранова структура, а $\varphi$ е затворена универсална формула. Тогава
(14)
\begin{align} \mathcal{A} \models \varphi \leftrightarrow \mathcal{A} \models \mathrm{CSi}(\varphi) \end{align}

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

Нека $\Gamma$ е множество от затворени универсални формули. Тогава дефинираме

(15)
\begin{eqnarray} \mathrm{Si}(\Gamma) &\rightleftharpoons& \bigcup_{\varphi \in \Gamma} \mathrm{Si}(\varphi) \\ \mathrm{CSi}(\Gamma) &\rightleftharpoons& \bigcup_{\varphi \in \Gamma} \mathrm{CSi}(\varphi) \\ \end{eqnarray}

Същите твърдения, но този път за множества.

  • Ако $\mathcal{A}$ е свободна ербранова структура и $\Gamma$ е множество от затворени универсални формули:
(16)
\begin{align} \mathcal{A} \models \Gamma \leftrightarrow \mathcal{A} \underset{\mathrm{id}_A}\models \mathrm{Si}(\Gamma) \end{align}
  • Ако $\mathcal{A}$ е ербранова структура и $\Gamma$ е множество от затворени универсални формули:
(17)
\begin{align} \mathcal{A} \models \Gamma \leftrightarrow \mathcal{A} \models \mathrm{CSi}(\Gamma) \end{align}
Unless otherwise stated, the content of this page is licensed under Creative Commons Attribution-NonCommercial-ShareAlike 3.0 License