Еднозначен синтактичен анализ, заместване, замяна

Еднозначен синтактичен анализ на термове

В тази точка ще докажем, че всеки правилно построен терм е построен точно по един начин - т.е не съществува друга последователност от стъпки (индуктивните стъпки от дефиницията на терм), при които се получава същия терм.

Твърдение (никой терм не е собствено начало на друг)

Нека $\tau$ е терм. Тогава за всеки терм $\varkappa$ е изпълнено, че $\tau$ не е собствено начало на $\varkappa$ и $\varkappa$ не е собствено начало на $\tau$.

Доказателство: Индуктивно по построението на $\tau$.
(1) Нека $\tau = x$ - индивидна променлива. Да разгледаме 3те случая за $\varkappa$:
(1.1) Нека $\varkappa = y$. Тъй като и двата терма са с равна дължина, не може единия да е собствено начало на другия.
(1.2) Нека $\varkappa = c$. Също като (1.1).
(1.3) Нека $\varkappa = f(\varkappa_1, \cdots, \varkappa_k)$. За да е $\tau$ собствено начало на $\varkappa$, трябва със сигурност буквите $x$ и $f$ да съвпадат. Но това е невъзможно - множествата на индивидните променливи и на функционалните символи нямат общи елементи : $\mathrm{Var} \cap \mathbb{F}\mathrm{unc} = \varnothing$. Очевидно $\varkappa$ не може да е собствено начало на $\tau$, защото $\tau$ е по-къса.
(2) Нека $\tau = c$ - индивидна константа. Да разгледаме 3те случая за $\varkappa$:
(2.1) Нека $\varkappa = y$. Термовете имат равна дължина - не може единия да е собствено начало на другия.
(2.2) Нека $\varkappa = d$. Също като (2.1).
(2.3) Нека $\varkappa = f(\varkappa_1, \cdots, \varkappa_k)$. За да е $\tau$ собствено начало на $\varkappa$, трябва със сигурност буквите $c$ и $f$ да съвпадат. Но това е невъзможно - множествата на индивидните константи и на функционалните символи нямат общи елементи : $\mathbb{C}\mathrm{onst} \cap \mathbb{F}\mathrm{unc} = \varnothing$. Очевидно $\varkappa$ не може да е собствено начало на $\tau$, защото $\tau$ е по-къса.
(3) Нека $\tau = f(\tau_1, \tau_2, \cdots, \tau_n)$ и твърдението е изпълнено за $\tau_i$ (т.е те не са собствени начала на никои други термове, и никои други термове не са им собсвени начала). Да разгледаме случаите за $\varkappa$:
(3.1) $\varkappa = y$. Ако искаме $\varkappa$ да е собствено начало на $\tau$ - не може (разсъждението е същото като в (1.3). $\tau$ не може да е собствено начало на $\varkappa$, защото е по-дълга.
(3.2) $\varkappa = c$. Случая $\varkappa$ собствено начало на $\tau$ отпада (като в (2.3)). Наобратно не може заради дължината.
(3.3) $\varkappa = g(\varkappa_1, \cdots, \varkappa_k)$. Това е основния и най-труден от всички случай. Да допуснем, че $\tau$ е собствено начало на $\varkappa$ или обратно. И в двата случая трябва всички символи в началото да съвпадат - за това ще почнем да 'засичаме' единия срещу другия (слагаме ги един под друг и започваме да задраскваме еднакви букви и да правим изводи). Следователно буквите $f, g$ съвпадат, след тях и отварящите скоби. Следват съответно $\tau_1$ и $\varkappa_1$. Или едното е собствено начало на другото, или обратно, или съвпадат. Според индуктивната хипотеза първите две отпадат ($\tau_1$ не е собсвено начало на никой друг терм, и никой друг терм не е собсвено начало на $\tau_1$). Следователно $\tau_1$ съвпада с $\varkappa_1$. Следват запетайките, след тях - $\tau_2$ и $\varkappa_2$ и.т.н… . . Това се повтаря, докато термовете на едното място не свършат. Тогава или са свършили и на 2те места, от където получихме, че $\tau = \varkappa$, или на едното има още. Но тогава там където са свършили следва затваряща скоба, а там където има още следва запетайка. Следователно не може късия да е собствено начало на дългия (и обратно заради дължините).

Теорема (еднозначен синтактичен анализ на термове)

За всеки терм $\tau$ е в сила точно едно от 3те:

  • $\tau$ е индивидна променлива (еднозначно определена)
  • $\tau$ е индивидна константа (еднозначно определена)
  • съществуват единствени $f \in \mathbb{F}\mathrm{unc}$ и термове $\tau_1, \cdots, \tau_n$, където $\sharp[f] = n$, такива че $\tau = f(\tau_1, \cdots, \tau_n)$.

Доказателство:
Първите два случая са очевидни. За 3ти случай допускаме, че съществуват два функционални символа $f, g$ и две редици от термове $\tau_1, \cdots, \tau_n$ и $\varkappa_1, \cdots, \varkappa_k$, така че $\tau = f(\tau_1, \cdots, \tau_n) = g(\varkappa_1, \cdots, \varkappa_k)$. Тъй като това са все символи, заключаваме $f = g$. Сега $\tau_1$ е собствено начало на $\varkappa_1$, или обратно, или са равни. От доказаното твърдение получаваме, че са равни. След тях запетайките, вторите термове итн. Ако термовете свършат заедно, следователно всеки терм е равен на съответния му терм от другата страна, както и функционалните букви - следователно всичко съвпада. Ако едните термове свършат по-рано, няма как и двете последователности от букви да отговарят на едно и също нещо - $\tau$. Следователно съществува единствена функционална буква и единствени термове, такива че $\tau = f(\tau_1, \cdots, \tau_n)$.

Заместване на термове

Дефиниция (заместване в терм)

Нека $x_1, \cdots, x_n$ са различни индивидни променливи, а $\tau_1, \cdots, \tau_n$ са произволни термове.
С $\tau[x_1/\tau_1, \cdots, x_n / \tau_n]$ ще означаваме думата, която се получава от думата $\tau$ при едновременно заместване на всички участия на буквите $x_1, \cdots, x_n$ в $\tau$ съответно с думите $\tau_1, \cdots, \tau_n$.

Твърдение (заместване в терм е терм)

Ако $\tau$ е терм, то $\tau[x_1/\tau_1, \cdots, x_n/\tau_n]$ е също терм.

Доказателство: Ще направим индукция по построенито на $\tau$.
(1) $\tau = x$
(1.1) $x = x_i$ за някое $i \in \{ 1, \cdots, n \}$. Сега очевидно $\tau[x_1/\tau_1, \cdots, x_n / \tau_n] = x_i[x_1/\tau_1, \cdots, x_n/\tau_n] = \tau_i$, което е терм.
(1.2) $x \notin \{ x_1, \cdots, x_n \}$. В този случай заместването не променя нищо: $x[x_1/\tau_1, \cdots, x_n/\tau_n] = x = \tau$, което е терм.
(2) $\tau = c$ В този случай заместването не променя нищо, следователно остава началния терм.
(3) $\tau = f(\varkappa_1, \cdots, \varkappa_k)$, като за $\varkappa_1, \cdots, \varkappa_k$ твърдението е вярно.
Следователно, от индуктивното предположение $\varkappa_i[x_1/\tau_1, \cdots, x_n / \tau_n] = \varkappa'_i$ също е терм. Сега остава да забележим, че като заместваме в $\tau$ всъщност заместваме във всеки един от термовете $\varkappa_i$ - защото функционалния символ не може да се замести, запетайките и скобите също. Получаваме:

(1)
\begin{eqnarray} \tau[x_1/\tau_1, \cdots, x_n/\tau_n] &=& f(\varkappa_1, \cdots, \varkappa_k)[x_1/\tau_1, \cdots, x_n/\tau_n] \\ &=& f(\varkappa_1[x_1/\tau_1, \cdots, x_n/\tau_n], \cdots, \varkappa_k[x_1/\tau_1, \cdots, x_n/\tau_n]) \\ &=& f(\varkappa'_1, \cdots, \varkappa'_k) \end{eqnarray}

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

Твърдение

Нека $x_1, \cdots, x_n$ са различни индивидни променливи и $\tau_1, \cdots, \tau_n$ са термове. Тогава всеки терм $\varkappa$ и всеки две оценки $v, w$ удовлетворяващи условието:

(2)
\begin{eqnarray} v(x_i) = \| \tau_i \|^\mathcal{A} [w] &\quad& i = \overline{1,n} \\ v(y) = w(y) &\quad& \forall y \in \mathrm{Var}[\varkappa] \setminus \{ x_1, \cdots, x_n \} \\ \end{eqnarray}

е в сила равенството:

(3)
\begin{align} \| \varkappa \|^\mathcal{A}[v] = \|\varkappa[x_1/\tau_1, \cdots, x_n/\tau_n] \|^\mathcal{A} [w] \end{align}

Доказателство: Индукция по построението на $\varkappa$
(1) $\varkappa = x$
(1.1) $x = x_i \quad i \in \{ 1, \cdots, n \}$. Тогава очевидно имаме, че

(4)
\begin{eqnarray} \| \varkappa \|^\mathcal{A}[v] &=& \| x_i \|^\mathcal{A}[v] \\ &=& v(x_i) \\ &=& \| \tau_i \|^\mathcal{A}[w] \\ &=& \| \varkappa[x_1/\tau_1, \cdots, x_n / \tau_n] \|^\mathcal{A} [w] \\ \end{eqnarray}

(използвахме първото условие за оценките).
(1.2) $x \notin \{ x_1, \cdots, x_n \}$. Т.е имаме, че $\varkappa[x_1/\tau_1, \cdots, x_n / \tau_n] = \varkappa$. Сега използваме второто условие за оценките, според което оценката на индивидна променлива различна от заменяните не се променя, т.е $\| \varkappa \|^\mathcal{A}[v] = \| x \|^\mathcal{A}[v] = v(x) = w(x) = \| x[x_1/\tau_1, \cdots, x_n / \tau_n] \|^\mathcal{A} [w]$
2) $\varkappa = c$
Оценката на константи зависи само от структурата, и освен това замяната не ги променя, следователно всичко е ок.
(3) $\varkappa = f(\varkappa_1, \cdots, \varkappa_k)$, и за $\varkappa_i$ твърдението е изпълнено. Т.е имаме, че $\| \varkappa_i \|^\mathcal{A}[v] = \| \varkappa_i[x_1/\tau_1, \cdots, x_n / \tau_n] \|^\mathcal{A}[w]$. Сега да разпишем подробно:

(5)
\begin{eqnarray} \| \varkappa [x_1/\tau_1, \cdots, x_n / \tau_n] \|^\mathcal{A} [w] &=& \| f(\varkappa_1[x_1/\tau_1, \cdots, x_n / \tau_n], \cdots, \varkappa_k[x_1/\tau_1, \cdots, x_n / \tau_n])\|^\mathcal{A} [w] \\ &=& f^\mathcal{A}(\|\varkappa_1[x_1/\tau_1, \cdots, x_n / \tau_n]\|^\mathcal{A}[w], \cdots, \|\varkappa_k[x_1/\tau_1, \cdots, x_n / \tau_n]\|^\mathcal{A}[w]) \\ &=& f^\mathcal{A}(\|\varkappa_1\|^\mathcal{A}[v], \cdots, \| \varkappa_k \|^\mathcal{A} [v]) \\ &=& \|\varkappa\|^\mathcal{A} [v] \end{eqnarray}

С това твърдението е доказано.

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

Нека $\varphi$ е предикатна формула, $x$ е индивидна променлива, a $\tau$ е терм. Казваме, че замяната на свободните участия на $x$ в $\varphi$ с $\tau$ е допустима, ако никое свободно участие на $x$ не е в област на действие на квантор по променлива участваща в $\tau$.

Извод:
Нека $\varphi$ е формула и $x \in \mathrm{Var}^{free}[\varphi]$ е променлива.

  • Ако $\tau$ е затворен терм, то $\varphi[x / \tau]$ е допустима;
  • Ако $\mathrm{Var}[\tau] \cap \mathrm{Var}^{bd}[\varphi] = \varnothing$, то $\varphi[x/\tau]$ е допустима;
  • Ако $\varphi$ е безкванторна, то $\varphi[x / \tau]$ е допустима (това е частен случай на горното).

Пример (за допустима замяна)

  • $\varphi = \forall x p (x, z) \And \exists y (p (z, y) \And q (y, x, x))$

$\tau = f (z)$. Замяната $\varphi[x / \tau] = \forall x p (x, z) \And \exists y (p (z, y) \And q (y, f (z), f (z)))$ е допустима.

  • $\varphi = \forall y p (x, y)$

$\tau = f (y)$. Очевидно замяната $\varphi[x / \tau] = \forall y p (f (y), y)$ не е допустима.

Твърдение

Нека $x$ е индивидна променлива и $\tau$ е терм. Тогава за всяка формула $\varphi$, за която замяната на свободните участия на $x$ във $\varphi$ с $\tau$ е допустима и за всеки две оценки $v, w$ удовлетворяващи условията:

(6)
\begin{eqnarray} \left\{\begin{array}{rcl} v(x) &=& \|\tau\|^\mathcal{A} [w] \\ v(y) &=& w(y) \quad \forall y \in \mathrm{Var}^{free}[\varphi] \setminus \{ x \} \\ \end{array}\right\} (\star) \end{eqnarray}

тогава:

(7)
\begin{align} \|\varphi[x / \tau] \|^\mathcal{A}[w] = \|\varphi\|^\mathcal{A} [v] \end{align}

Доказателство: Ще направим индукция по построението на $\varphi$
(1) $\varphi = p(\varkappa_1, \cdots, \varkappa_k)$
Нека $v, w$ удовлетворяват условията $(\star)$. Имаме, че $\mathrm{Var}[\varkappa_i] \subseteq \mathrm{Var}^{free}[\varphi]$, следователно може да приложим предното твърдение, следователно $\| \varkappa_i \|^\mathcal{A}[v] = \| \varkappa_i[x / \tau]\|^\mathcal{A} [w]$.

(8)
\begin{eqnarray} \| p(\varkappa_1, \cdots, \varkappa_k) \|^\mathcal{A}[v] = \mathrm{t} &\leftrightarrow& \langle \| \varkappa_1 \|^\mathcal{A}[v], \cdots, \| \varkappa_k \|^\mathcal{A}[v] \rangle \in p^\mathcal{A} \\ &\leftrightarrow& \langle \| \varkappa_1[x / \tau] \|^\mathcal{A}[w], \cdots, \| \varkappa_k[x/\tau] \|^\mathcal{A}[w] \rangle \in p^\mathcal{A} \\ &\leftrightarrow& \| p( \varkappa_1[x / \tau], \cdots, \varkappa_k[x / \tau]) \|^\mathcal{A} [w] = \mathrm{t} \\ &\leftrightarrow& \| p(\varkappa_1, \cdots, \varkappa_k)[x / \tau]\|^\mathcal{A} [w] = \mathrm{t} \\ \end{eqnarray}

(2) $\tau = (\tau_1 \dot= \tau_2)$ - напълно аналогично на горния случай.
(3) $\varphi = \lnot \psi$, където за $\psi$ твърдението е вярно.
Нека $\varphi[x / \tau]$ е допустимо, и нека оценките $v, w$ удовлетворяват условието $(\star)$. Тогава и $\psi[x / \tau]$ е допустимо (защото свободните участия на $x$ в $\varphi$ и $\psi$ са едни и същи). Тъй като твърдението е изпълнено за $\psi, v, w$, имаме че $\| \psi \|^\mathcal{A}[v] = \|\psi[x / \tau]\|^\mathcal{A}[w]$. Следователно и отрицанията им имат еднакви оценки: $\| \lnot \psi \|^\mathcal{A}[v] = \| \lnot \psi [x/\tau] \|^\mathcal{A}[w]$.
(4) $\varphi = ( \psi_1 \sigma \psi_2)$, където $\sigma \in \{ \And, \lor, \Rightarrow, \iff \}$, и за $\psi_1, \psi_2$ твърдението е изпълнено..$\psi_i[x / \tau]$ е допустимо (виж горния случай). Ако $y \in \mathrm{Var}^{free}[\psi_i] \setminus \{ x \}$, то $y \in \mathrm{Var}^{free}[\varphi] \setminus \{ x \}$, следователно $v(y) = w(y)$ и може да приложим индукционното предположение за $\psi_i$, т.е $\| \psi_i \|^\mathcal{A}[v] = \| \psi_i[x / \tau ] \|^\mathcal{A}[w]$

(9)
\begin{eqnarray} \| \varphi \|^\mathcal{A} [v] &=& H_\sigma (\| \psi_i \|^\mathcal{A}[v], \| \psi_2 \|^\mathcal{A} [v]) \\ &=& H_\sigma ( \| \psi_1 [x / \tau] \|^\mathcal{A}[w], \| \psi_2[x / \tau]^\mathcal{A}[w]) \\ &=& \| \psi_1[x / \tau] \sigma \psi_2 [x / \tau] \|^\mathcal{A} [w] \\ &=& \| \varphi [x / \tau] \|^\mathcal{A} [w] \\ \end{eqnarray}

(5) $\varphi = Qz\psi$, където $Q \in \{ \forall, \exists \}$ и за $\psi$ твърдението е вярно.
(5.1) Нека $x \notin \mathrm{Var}^{free} [Qz\psi]$. Тогава очевидно $\varphi[x/ \tau] = \varphi$. Освен това, от $(\star)$ имаме, че всички свободни променливи на $\varphi$ имат еднаква оценка при $v$ и $w$ (всички свободни променливи без $x$ имат еднакви оценки(от $(\star)$), но тъй като $x$ не е свободна, следователно всички общи применливи имат еднакви оценки). Следователно $\| \varphi \|^\mathcal{A}[v] = \| \varphi \|^\mathcal{A}[w] = \| \varphi[x / \tau] \|^\mathcal{A}[w]$.
(5.2) Нека $x \in \mathrm{Var}^{free}[Qz\psi]$.
Първо ще докажем следното помощно твърдение: ако $a \in A$ е произволен елемент, то $\| \psi \|^\mathcal{A} [v^z_a] = \| \psi[x / \tau] \|^\mathcal{A}[w^z_a]$.
T.e ще използваме индуктивната хипотеза за $\psi$ и оценки $v^z_a, w^z_a$. За да направим това трябва просто да покажем, че $v^z_a, w^z_a$ изпълняват $(\star)$ за формулата $\psi$. Т.е трябва да покажем, че:

  • $v^z_a(x) = \| \tau \|^\mathcal{A} [w^z_a]$.

Тъй като $x \ne z$ (иначе $x = z$ е под квантор във $\varphi$ и следователно замяната $\varphi[x / \tau]$ не е допустима) имаме, че $v^z_a(x) = v(x)$. Сега прилагаме $(\star)$ за $v, w$: $v(x) = \| \tau \|^\mathcal{A} [w]$. И остава да видим, че $z \notin \mathrm{Var}^{free}[\tau]$ (ако е от свободните променливи, заместването няма да е допустимо, защото $z$ е под квантор), и следователно $\| \tau \|^\mathcal{A}[w] = \| \tau \|^\mathcal{A} [w^z_a]$. Като сглобим 3те равенства получаваме, че $v^z_a(x) = \| \tau \|^\mathcal{A} [w^z_a]$.

  • $\forall y \in \mathrm{Var}^{free}[\psi] \setminus \{ x \} \rightarrow v^z_a(y) = w^z_a(y)$.
    Ще разгледаме два случая:
    • $y = z$, следователно $v^z_a(y) = v^z_a(z) = a = w^z_a(z) = w^z_a(y)$ - т.е всичко е ок.
    • $y \ne z$. От тук имаме, че $v^z_a(y) = v(y)$. Понеже $y \in \mathrm{Var}^{free}[\psi] \setminus \{ x \}$ имаме и че $y \in \mathrm{Var}^{free}[\varphi] \setminus \{ x \}$ (двете множества се различават само по това, че във свободните променливи на $\varphi$ няма $z$, но $y \ne z$ така че е вярно). Сега прилагаме $(\star)$ за $v, w$ и получаваме, че $v(y) = w(y)$. Накрая отново ползваме, че $y \ne z$ и заключваме, че $w(y) = w^z_a(y)$. Като навържем равенствата получаваме, че $v^z_a(y) = w^z_a(y)$.

С това и второто условие е на лице. Следователно $\| \psi \|^\mathcal{A} [v^z_a] = \| \psi[x / \tau] \|^\mathcal{A}[w^z_a]$ е вярно за произволно $a \in A$.
Сега да разгледаме случаите за квантора:
(5.2.1) $Q = \forall$.
Нека $\mathcal{A} \underset{v}\models \forall z\psi$. Следователно за произволно $a_0 \in A$ е изпълнено, че $\mathcal{A} \underset{v^z_{a_0}}\models \psi$. Сега използваме помощното твърдение за $a_0$ и получаваме, че $\mathcal{A} \underset{w^z_{a_0}}\models \psi[x / \tau]$. Понеже това е вярно за произволно $a_0 \in A$ имаме, че $\mathcal{A} \underset{w}\models \forall z \psi[x / \tau]$.
Сега същото нещо в обратната посока, и доказахме, че $\mathcal{A} \underset{v}\models \forall z \psi \leftrightarrow \mathcal{A} \underset{w}\models \forall z \psi[x / \tau]$.
(5.2.2) $Q = \exists$.
Абсолютно по същия начин, просто вместо "произволно $a_0 \in A$" взимаме точно това, за което $\psi$ е изпълнено.

Забележка: Записа $Qz\psi[x / \tau]$ може да означава две неща - че заместваме само в $\psi$ или че заместваме в цялата формула $\varphi$. И в двата случая стойността е една и съща (защото ако заместваме в цялата формула, понеже не пипаме квантора и буквата след него, остава да заместваме само $\psi$).

Една специална предикатна тавтология

Твърдение

Нека $Qx\varphi$ е предикатна формула и $\varphi[x / \tau]$ е допустима. Тогава:

  • $\models \forall x\varphi \Rightarrow \varphi[x / \tau]$
  • $\models \varphi[x / \tau] \Rightarrow \exists x\varphi$

Т.е. горните импликации са предикатни тавтологии

Доказателство: Нека $\mathcal{A}$ е произволна структура и $v$ е произволна оценка в нея. Ще докажем, че $\models \forall x\varphi \Rightarrow \varphi[x / \tau]$.
(1) Нека $\mathcal{A} \underset{v}\nvDash \forall x\varphi$. Тогава $\mathcal{A} \underset{v}\models \forall x\varphi \Rightarrow \varphi[x / \tau]$. (от лъжа следва всичко).
(2) Нека $\mathcal{A} \underset{v}\models \forall x\varphi$. Нека стойността на $\tau$ е $a_0 \in A$ : $\| \tau \|^\mathcal{A} [v] = a_0$. Тогава имаме, че $\mathcal{A} \underset{v_{a_0}^x}\models \varphi$ (защото имаме 'за всяко').
Сега ще покажем, че предишното твърдение е приложимо за формула $\varphi$ и оценки $v_{a_0}^x, v$:

  • $\varphi[x / \tau]$ е допустимо по условие
  • $v_{a_0}^x(x) = a_0 = \| \tau \|^\mathcal{A}[v]$ - това е първото условие на твърдението
  • Нека $y \in \mathrm{Var}^{free}[\varphi] \setminus \{ x \}$. Тогава $v_{a_0}^x(y) = v(y)$ - това е второто условие.

Прилагаме твърдението и получаваме: $\| \varphi \|^\mathcal{A}[v_{a_0}^x] = \| \varphi[x / \tau] \|^\mathcal{A}[v]$. Но от случая имаме, че $\| \varphi \|^\mathcal{A} [v_a^x] = \mathrm{t}$, следователно $\| \varphi[x / \tau] \|^\mathcal{A}[v] = \mathrm{t}$ и с това твърдението е доказано.
Остава само да споменем, че разсъждението е вярно за произволна структура и оценка, следователно е вярно за всяка структура (демек - записа $\models$ без нищо пред и под него :)).

2рото се прави по същия начин.

Вариант на формула

Накратко ще сменяме променлива, под действие на квантор - т.е "За всяко n, n + 1 е естествено" става "За всяко k, k + 1 е естествено". Може да ви звучи очевидно, но формално не е чак толкова ;-)

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

Нека $Qx\varphi$ е предикатна формула. Нека $y \in \mathrm{Var}$, такава че:

  • $\varphi[x / y]$ е допустима (свободните участия на $x$ не са в област на действие на квантор по $y$)
  • $y \notin \mathrm{Var}^{free}[\varphi]$.

Тогава казваме, че $Qy\varphi[x / y]$ е вариант на $Qx\varphi$.

Твърдение (за равносилност на вариантите)

Нека $Qy\varphi[x/y]$ е вариант на $Qx\varphi$.
Тогава $\models Qx\varphi \iff Qy\varphi[x / y]$.
Доказателство: Да разгледаме случая $Q \equiv \forall$.
(1) Ще докажем, че $\models \forall x\varphi \Rightarrow \forall y \varphi[x / y]$.
Нека $\mathcal{A}$ е произволна структура и $v$ е оценка в нея. Нека $\mathcal{A} \underset{v}\models \forall x\varphi$. Ще докажем, че $\mathcal{A} \underset{v}\models \forall y\varphi[x / y]$.
Нека $a \in A$. Ще докажем, че твърдението е изпълнено за формула $\varphi$ и оценки $v_a^x, v_a^y$:

  • $\varphi[x / y]$ е допустима
  • $v_a^x (x) = a = v_a^y(y) = \| y \|^\mathcal{A}[v_a^y]$
  • Нека $z \in \mathrm{Var}^{free}[\varphi] \setminus \{ x \}$. Тогава очевидно $y \notin \mathrm{Var}^{free}[\varphi]$ и $y \ne z$, следователно $v_a^x(z) = v(z) = v_a^y(z)$.

С това условията на твърдението са изпълнени и може да заключим, че $\| \varphi \|^\mathcal{A}[v_a^x] = \| \varphi [x / y] \|^\mathcal{A}[v_a^y]$.
Нека $a \in A$ е произволен елемент. Тогава от $\mathcal{A} \underset{v}\models \forall x\varphi$ следва, че $\mathcal{A} \underset{v_a^x}\models \varphi$, т.е $\| \varphi \|^\mathcal{A}[v_a^x] = \mathrm{t}$. От току що доказаното твърдение получаваме, че и $\| \varphi[x/y] \|^\mathcal{A}[v_a^y] = \mathrm{t}$. Следователно $\mathcal{A} \underset{v_a^y}\models \varphi[x/y]$. Това е вярно за произволно $a \in A$, следователно е вярно за всяко $a \in A$, следователно $\mathcal{A} \underset{v}\models \forall y\varphi[x/y]$. С което показахме, че $\models \forall x\varphi \Rightarrow \forall y \varphi[x / y]$.
(2) Нека $\mathcal{A} \underset{v}\models \forall y\varphi[x / y]$. Ще докажем, че $\mathcal{A} \underset{v}\models \forall x\varphi$.
Ще докажем, че $\forall x\varphi[x / y][y / x]$ е вариант на $\forall y \varphi[x / y]$. За целта трябва да проверим следните неща:

  • $\varphi[x/y][y/x]$ е допустима - ами да, след като във $\varphi[x/y]$ няма никакви свързани участия на $x$ по какъв да е квантор, то $\varphi[x/y][y/x]$ е валидна (няма участия на $y$, които да са в област на действие по квантор от $x$, защото ако има, ще излезе че предишното заместване е сложило $y$ на мястото на свързано участие на $x$).
  • $x \notin \mathrm{Var}^{free}[\varphi[x / y]]$ - очевидно, след като сме заместили всички свободни участия на $x$ със $y$.

Следователно $\forall x\varphi[x/y][y/x]$ е вариант на $\forall y \varphi[x/y]$, и сега използваме (1) за да заключим, че $\models \forall y\varphi[x/y] \Rightarrow \forall x\varphi[x/y][y/x]$. И сега разбира се $\forall x\varphi[x/y][y/x] = \forall x\varphi$ (под равно имам предвид синтактично равно - демек двата записа представят един и същи низ, представляващ формула). И с това сме готови.

Случая $Q \equiv \exists$ е напълно аналогичен.
Дефинираме няколко записа:
А-еквивалентни: $\mathcal{A} \models \varphi \iff \psi \longleftrightarrow \varphi |\overset{\mathcal{A}}=| \psi$.
логически еквивалентни: $\models \varphi \iff \psi \longleftrightarrow \varphi |=| \psi$
Забележка: $|=|$ трябва да изглежда като $\models$ със залепена вертикална черта от дясно. Естествено, такъв символ няма във латекса (или поне не успях да намеря в "The comprehensive Latex Symbol List", което работи в тази википедия - \sdststile{}{} не работи :-)).

Заместване на подформули на предикатни формули

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

Казваме, че $\varphi$ е подформула на $\psi$, ако:
(1) $\varphi$ и $\psi$ са предикатни формули;
(2) $\psi = \alpha \varphi \beta$ - т.е $\psi$ се състои от някакъв префикс $\alpha$, формулата $\varphi$ и някакъв суфикс $\beta$1.

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

Нека $\psi, \varphi$ са предикатни формули и $\psi = \alpha\varphi\beta$.
Нека $\varphi'$ е предикатна формула и $\mathcal{A}$ е структура. Тогава:
(1) $\psi' = \alpha\varphi'\beta$ е също предикатна формула.
(2) Ако $\varphi |\overset{\mathcal{A}}=| \varphi'$ то и $\psi |\overset{\mathcal{A}}=| \psi'$.

Доказателство:
(2) Ако $\alpha = \beta = \epsilon$ (т.е 2те са равни на празната дума) твърдението е вярно.
Да разгледаме случая, когато поне едното е различно от празната дума.
Да направим индукция относно построението на $\psi$.
(2.1) $\psi$ е атомарна формула. Тогава няма как $\varphi$ да и е подформула освен ако не съвпадат - разгледахме този случай в началото.
(2.2) $\psi = \lnot \psi_1$ и за $\psi_1$ твърдението е изпълнено. Тогава $\alpha\varphi\beta = \psi = \lnot \psi_1$ следва $\psi_1 = \alpha_1\varphi\beta$, където $\lnot\alpha_1 = \alpha$. Съгласно ИП за $\psi_1$ имаме: $\alpha_1\varphi\beta |\overset{\mathcal{A}}=| \alpha_1\varphi'\beta$. Следователно като прибавим по едно отрицание от двете страни пак ще е еквивалентно: $\lnot\alpha_1\varphi\beta |\overset{\mathcal{A}}=| \lnot\alpha_1\varphi'\beta$ - т.е $\alpha\varphi\beta |\overset{\mathcal{A}}=| \alpha\varphi'\beta$.
(2.3) $\psi = (\psi_1 \sigma \psi_2)$, и за $\psi_1, \psi_2$ твърдението е изпълнено.
Със сигурност $\varphi$ е или изцяло в $\psi_1$, или изцяло в $\psi_2$. Б.О.О. избираме $\psi_1 = \alpha_1\varphi\beta_1$. Съгласно ИП за $\psi_1$: $\alpha_1\varphi\beta_1 |\overset{\mathcal{A}}=| \alpha_1\varphi'\beta_1 = \psi_1'$. Следователно ако $v$ е произволна оценка в $\mathcal{A}$, то $\| \alpha_1\varphi\beta_1 \|^\mathcal{A}[v] = \| \alpha_1\varphi'\beta_1 \|^\mathcal{A}[v]$.
Имаме, че

(10)
\begin{eqnarray} \| \psi \|^\mathcal{A}[v] &=& \| (\psi_1 \sigma \psi_2) \|^\mathcal{A}[v] \\ &=& H_\sigma(\| \psi_1 \|^\mathcal{A}[v], \| \psi_2 \|^\mathcal{A}[v]) \\ &=& H_\sigma(\| \alpha_1\varphi\beta_1 \|^\mathcal{A}[v], \| \psi_2 \|^\mathcal{A}[v]) \\ &=& H_\sigma(\| \alpha_1\varphi'\beta_1 \|^\mathcal{A}[v], \| \psi_2 \|^\mathcal{A}[v]) \\ &=& \| (\psi_1' \sigma \psi_2) \|^\mathcal{A}[v] \\ &=& \| \psi' \|^\mathcal{A}[v] \\ \end{eqnarray}

(2.4) Нека $\psi = Qx\psi_1$, където $Q$ е квантор и за $\psi_1$ твърдението е изпълнено.
Да разгледаме случая $Q = \exists$.
Нека $\| \psi \|^\mathcal{A}[v] = \mathrm{t}$, т.е $\mathcal{A} \underset{v}\models \psi = \exists x \alpha_1 \varphi \beta$.
Нека $a \in A$ е такова, че $\mathcal{A} \underset{v^x_a}\models \alpha_1 \varphi \beta$. От ИП за $\psi_1$ имаме, че:

(11)
\begin{eqnarray} \alpha_1 \varphi \beta |\overset{\mathcal{A}}=| \alpha_1 \varphi' \beta &\rightarrow& \mathcal{A} \underset{v^x_a}\models \alpha_1 \varphi' \beta \\ &\rightarrow& \mathcal{A} \underset{v}\models \exists x\alpha_1 \varphi' \beta \\ &\rightarrow& \mathcal{A} \underset{v}\models \psi' \end{eqnarray}

Сега трябва да докажем и обратното: ако $\mathcal{A} \underset{v}\models \exists x \alpha_1 \psi' \beta$, то и $\mathcal{A} \underset{v}\models \exists x \alpha_1 \varphi \beta$. Доказателството е същото :)
Случая $Q = \forall$ е аналогичен.
С това твърдението е доказано.

Теорема (за еквивалентната замяна)

Нека $\varphi_1, \varphi_2, \dots, \varphi_n$, и $\varphi_1', \varphi_2', \dots, \varphi_n'$ са предикатни формули. Нека $\psi$ е предикатна формула, такава че:

(12)
\begin{align} \psi = \alpha_0 \varphi_1 \alpha_1 \dots \varphi_n \alpha_n \end{align}

Тогава са изпълнени следните две неща:
(1) думата $\psi' = \alpha_0 \varphi_1' \alpha_1 \varphi_2' \dots \varphi_n' \alpha_n$ е също предикатна формула;
(2) Ако $\varphi_i |=| \varphi_i'$ за всяко $i \in \{ 1, \dots, n \}$ то $\psi |=| \psi'$.

Доказателство: Мисля че е очевидно, използвайки предното твърдение.

Свойства

(1) Нека $x \notin \mathrm{Var}^{free}[\varphi]$. Тогава $\varphi |=| \forall x\varphi$ и $\varphi |=| \exists x\varphi$.
(2)

(13)
\begin{eqnarray} \lnot \forall x\varphi &|=|& \exists x\lnot\varphi \\ \lnot \exists x\varphi &|=|& \forall x\lnot\varphi \\ \lnot \forall x \lnot \varphi &|=|& \exists x\varphi \\ \lnot \exists x \lnot\varphi &|=|& \forall x\varphi \\ \end{eqnarray}

(3)

(14)
\begin{eqnarray} \forall x(\varphi \And \psi) &|=|& \forall x\varphi \And \forall x\psi \\ \exists x(\varphi \lor \psi) &|=|& \exists x\varphi \lor \exists x\psi \\ \end{eqnarray}

(4) Нека $x \notin \mathrm{Var}^{free}[\varphi]$. Тогава:

(15)
\begin{eqnarray} \forall x(\varphi \lor \psi) &|=|& \varphi \lor \forall x\psi \\ \exists x(\varphi \And \psi) &|=|& \varphi \And \exists x\psi \\ \end{eqnarray}

(5) Нека $x \notin \mathrm{Var}^{free}[\varphi]$. Тогава $Qx(\varphi \sigma \psi) \ \ |=| \ \ \varphi \sigma Qx \psi$, където $Q \in \{ \forall, \exists \}$ и $\sigma = \{ \And, \lor \}$. това е просто генерализация на горните.

Забележка: Горните са доказвани на лекции, мен малко ме мързи в момента.

Unless otherwise stated, the content of this page is licensed under Creative Commons Attribution-NonCommercial-ShareAlike 3.0 License