Разширяване на езици. Обогатяване на структури. Скулемизация.

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


Разширяване на език

Дефиниция (разширяване на език)

Нека $\mathcal{L}_1, \mathcal{L}_2$ са предикатни езици. Ще казваме, че $\mathcal{L}_2$ обогатява $\mathcal{L}_1$ ако са в сила следните изисквания:

  • двата езика са от един и същи тип1;
  • всички нелогически символи от $\mathcal{L}_1$ са нелогически символи от $\mathcal{L}_2$2;
  • ако $p$ е предикатен вимвол в $\mathcal{L}_1$, то в $\mathcal{L}_2$ той има същата арност (от второто условие знаем че го има);
  • ако $f$ е функционален символ в $\mathcal{L}_1$, то в $\mathcal{L}_2$ има функционален символ $f$ и той е със същата арност (от второто условие знаем че го има).

Забележка: Дефиницията всъщност казва, че разширение на един език може да правим като само добавяме нови константи, функционални символи и предикати към езика, но нямаме право да променяме съществуващите такива на оригиналния език. И понеже в езика се казва само арността на функционалните и предикатите символи - значи нямаме право да я променяме. Обърнете внимание че в структурата се задава интерпретацията, а не в самия език.

Свойства на разширените езици

  • всеки терм от $\mathcal{L}_1$ е терм и от $\mathcal{L}_2$;
  • всяка атомарна формула от $\mathcal{L}_1$ е атомарна формула и от $\mathcal{L}_2$;
  • всяка формула от $\mathcal{L}_1$ е и формула от $\mathcal{L}_2$.

Обогатяване на структура

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

Нека $\mathcal{L}_2$ е разширение на $\mathcal{L}_1$. И $\mathcal{A}_i$ е структура за $\mathcal{L}_i,\quad i = 1, 2$.
Ще казваме, че $\mathcal{A}_2$ е обогатяване на $\mathcal{A}_1$ до структура за $\mathcal{L}_2$, ако са изпълнени следните изисквания:

  • $| \mathcal{A}_1 | = | \mathcal{A}_2 |$;
  • за всеки нелогичен символ $\xi \in \mathcal{L}_1$ е изпълнено $\xi^{\mathcal{A}_1} = \xi^{\mathcal{A}_2}$.

Свойства на обогатените структури

  • всяка структура за езика $\mathcal{L}_1$ може да се обогати до структура за разширение на $\mathcal{L}_1$;
  • нека $\mathcal{L}_1$ е език, $\mathcal{L}_2$ е негово разширение, $\mathcal{A}_1$ е структура за $\mathcal{L}_1$ и $\mathcal{A}_2$ е обогатяване на $\mathcal{A}_1$ за езика $\mathcal{L}_2$. Нека $v$ е оценка на индивидните променливи в $A = | \mathcal{A}_1 | = | \mathcal{A}_2 |$. Тогава:
    • за всеки терм $\tau \in \mathcal{T}_{\mathcal{L}_1}$ е изпълнено $\| \tau \|^{\mathcal{A}_1}[v] = \| \tau \|^{\mathcal{A}_2}[v]$;
    • за всяка предикатна формула $\varphi$ от езика $\mathcal{L}_1$ е изпълнено $\| \varphi \|^{\mathcal{A}_1}[v] = \| \varphi \|^{\mathcal{A}_2}[v]$.

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

В тази точка ще покажем, как може да преобразуваме една формула от ПНФ (всички квантори отпред) до СНФ (всички квантори отпред, но без 'съществува'). За да постигнем този холокост на всички 'съществува' ще въвеждаме константи и функционални символи, които ще забождат променливите след квантора на някаква фиксирана стойност която върши работа. Ето няколко примера:

Съществува константа, такава че като я умножим по радиуса на окръжност получаваме полу-дължината й.

става:

Като умножим радиуса на окръжност по $\pi$ получаваме полу-дължината на окръжността.

тук константата $\pi$ е дефинирана в самия език - колко точно е оставяме на различните структури да определят.

Още един пример:

За всяко епсилон, съществува делта, такова че при $|x_1 - x_2| < \delta$ е изпълнено $|f(x_1) - f(x_2) | < \epsilon$

става:

За всяко епсилон е вярно, че при $|x_1 - x_2| < \delta(\epsilon)$ е изпълнено $|f(x_1) - f(x_2)| < \epsilon$

Сега сигурно ще си кажете - еее ама това $\delta(\epsilon)$ колко е точно (примерно $\epsilon^4 * 9.549 . 10^-5$). Истината е, че тази функция може да няма явен вид (като в примера) - просто е някакво изображение. По-точно бигхме могли да кажем, че съществува функция $\delta(\epsilon)$ за която при …, но това изказване даже не е в език от първи ред (защото има квантор по функция, а не по обект, ако приемем че обектите са реалните числа). Това което ние правим е да разширим езика, така че в него да има функционален символ $\delta$ с арност 1 - т.е магически вкарваме на ниско ниво съществуването на символ $\delta$, който е функционален, и когато се наложи да го интерпретираме слагаме подходящо изображение под него (не задължително функция в явен вид).

За да получим от всяка формула в ПНФ, неин еквивалент в който няма 'съществува' първо ще обясним как се маха едно съществува и после ще повторим докато не се разкарат всичките.

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

Нека $\varphi$ е затворена формула в ПНФ. Дефинираме $\varphi_s$ по следния начин:
(1) Ако в кванторния префикс на $\varphi$ не се среща $\exists$, тогава $\varphi_S \rightleftharpoons \varphi$
(2) В противен случай разглеждаме два възможни случая за местположението на $\exists$:
(2.1) $\varphi = \exists x \psi$3.
Дефинираме си нова индивидна константа $c_\varphi$ и $\varphi_s \rightleftharpoons \psi[x/c_\varphi]$.
(2.2) $\varphi = \forall x_1 \dots \forall x_n \exists x \psi$4
Дефинираме си нов функционален символ $f_\varphi$ с арност $n \ge 1$ и $\varphi_s \rightleftharpoons \forall x_1 \dots \forall x_n \psi[x / f_\varphi(x_1, \dots, x_n)]$5

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

Нека $\varphi$ е затворена формула в ПНФ. Скулемова нормална форма на $\varphi$ наричаме формулата $\varphi^S$, дефинирана по следния начин:

(1)
\begin{align} \varphi^S \rightleftharpoons \varphi_{\underbrace{ss\dots s}_n} \end{align}

където $n$ е броя срещания на $\exists$ в кванторния префикс на $\varphi$.

С други думи - прилагаме едностъпковата скулемизация докато не останат квантори 'съществува'.

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

Нека $\varphi$ е затворена формула в ПНФ. Тогава са в сила следните твърдения:
(i) $\models \varphi_s \Rightarrow \varphi$
(ii) ако $\mathcal{A}$ е структура и $\mathcal{A} \models \varphi$ то съществува обогатяване $\mathcal{A}_s$ на $\mathcal{A}$, такова че $\mathcal{A}_s \models \varphi_s$;
(iii) $\varphi$ е изпълнима т.с.т.к. $\varphi_s$ е изпълнима.

Доказателство:
(i.1) $\varphi = \exists x \psi$. В този случай $\varphi_s = \psi[x/c_\varphi]$.
Но $\models \psi[x/c_\varphi] \Rightarrow \exists x \psi$ е тавталогия. С това тази част е доказана.
(i.2) $\varphi = \forall x_1 \dots \forall x_n \exists x \psi$. В този случай $\varphi_s = \forall x_1 \dots \forall x_n \psi[x/f_\varphi(x_1,\dots, x_n)]$.
Използвайки същата тавталогия получаваме, че $\models \psi[x/f_\varphi(x_1,\dots, x_n)] \Rightarrow \exists x \psi$. Това към което ние се стремим обаче, е

(2)
\begin{align} \models \forall x_1 \dots \forall x_n \psi[x/f_\varphi(x_1,\dots, x_n)] \Rightarrow \forall x_1 \dots \forall x_n \exists x \psi \end{align}

Сега ще го докажем: Нека $\mathcal{A}$ е структура и $v$ е оценка в нея, и нека: $\mathcal{A} \underset{v}\models \forall x_1 \dots \forall x_n \psi[x/f_\varphi(x_1,\dots, x_n)]$. Ще докажем, че $\mathcal{A} \underset{v}\models \forall x_1 \dots \forall x_n \exists x \psi$. Нека $w$ е оценка като $v$, но всички хиксове са заместени с конкретни стойности от универсума: $w = v^{x_1\dots x_n}_{a_1\dots a_n}$. Сега $\mathcal{A} \underset{w}\models \psi[x/f_\varphi(x_1,\dots,x_n)]$. Използвайки тавталогията която споменахме по-горе $\mathcal{A} \underset{w}\models \exists x \psi$, и понеже направихме разсъждението за произволни $a_1, \dots, a_n$ получаваме, че $\mathcal{A} \underset{v}\models \forall x_1 \dots \forall x_n \exists x \psi$. Т.е показахме, че от $\mathcal{A} \underset{v}\models \forall x_1 \dots \forall x_n \psi[x/f_\varphi(x_1,\dots, x_n)]$ следва $\mathcal{A} \underset{v}\models \forall x_1 \dots \forall x_n \exists x \psi$. И това за произволна структура и оценка. Следователно тавтологията е доказана.

(ii.1) $\varphi = \exists x \psi$. Тогава $\varphi_s = \psi[x/c_\varphi]$.
Нека $\mathcal{A} \models \varphi$. Следователно за произволна оценка $v$ имаме: $\mathcal{A} \underset{v}\models \exists x \psi$. От семантиката на $\exists$ получаваме, че съществува обект от универсума $a \in A$, такъв че $\mathcal{A} \underset{v^x_a}\models \psi$. Нека си построим структура $\mathcal{A}_s$ такава че $c^{\mathcal{A}_s}_\varphi = a$. Използвайки това твърдение получаваме, че $\| \psi[x/c_\varphi] \|^{\mathcal{A}_s}[v] = \| \psi \|^{\mathcal{A}_s}[v^x_a]$, и сега използвайки това получаваме, че $\| \psi \|^{\mathcal{A}_s}[v^x_a] = \| \psi \|^{\mathcal{A}}[v^x_a] = \mathrm{t}$. Следователно $\| \psi[x/c_\varphi] \|^{\mathcal{A}_s}[v] = \mathrm{t} \leftrightarrow \mathcal{A}_s \underset{v}\models \varphi_s$. Понеже направихме разсъждението за произволна оценка, то то е вярно за всяка, с което твърдението е доказано.
(ii.2) $\varphi = \forall x_1 \dots \forall x_n \exists x \psi$. Тогава $\varphi_s = \forall x_1 \dots \forall x_n \psi[x/f_\varphi(x_1, \dots, x_n)]$.
Нека $\mathcal{A} \models \varphi$. Следователно за произволна оценка $v$ имаме: $\mathcal{A} \underset{v}\models \forall x_1 \dots \forall x_n \exists x \psi$. От семантиката на $\forall$ получаваме, че за произволни n обекта от универсума $a_1, \dots, a_n \in A$ е изпълнено $\mathcal{A} \underset{v^{x_1 \dots x_n}_{a_1 \dots a_n}}\models \exists x \psi$. Нека $w \rightleftharpoons v^{x_1 \dots x_n}_{a_1 \dots a_n}$ (за да не пишем много). Сега като използваме и семантиката на $\exists$ получаваме, че съществува елемент $a \in A$, такъв че $\mathcal{A} \underset{w^x_a}\models \psi$. Нека да си отбележим това изображение където на n обекта от универсума $a_1, \dots , a_n$ съпоставяме обекта $a$ с функцията $F : A^n \to A$6:

(3)
\begin{align} F(a_1, \dots, a_n) = a \end{align}

Сега остава да дефинираме функцията $f_\varphi$ в структурата $\mathcal{A}_s$: $f_\varphi^{\mathcal{A}_s}(a_1, \dots, a_n) \rightleftharpoons F(a_1, \dots, a_n)$. Ще докажем, че $\mathcal{A}_s \underset{v}\models \varphi_s$.
Нека първо да проверим, че $\mathcal{A}_s \underset{w^x_a}\models \psi[x/f_\varphi(x_1, \dots, x_n)]$. Отново използваме това твърдение, но първо ще покажем, че $\| f_\varphi(x_1, \dots, x_n)\|^{\mathcal{A}_s}[w] = a$:

(4)
\begin{eqnarray} \| f_\varphi(x_1, \dots, x_n)\|^{\mathcal{A}_s}[w] &=& f^{\mathcal{A}_s}_\varphi(\|x_1\|^{\mathcal{A}_s}[w], \dots, \|x_n\|^{\mathcal{A}_s}[w]) \\ &=& f^{\mathcal{A}_s}_\varphi(\|x_1\|^{\mathcal{A}_s}[v^{x_1 \dots x_n}_{a_1 \dots a_n}], \dots, \|x_n\|^{\mathcal{A}_s}[v^{x_1 \dots x_n}_{a_1 \dots a_n}]) \\ &=& f^{\mathcal{A}_s}_\varphi(a_1, \dots, a_n) \\ &=& F(a_1, \dots, a_n) \\ &=& a \end{eqnarray}

Следователно $\| \psi[x/f_\varphi(x_1, \dots, x_n)] \|^{\mathcal{A}_s}[w] = \| \psi \|^{\mathcal{A}_s}[w^x_a] = \mathrm{t}$ (накрая използваме и това). Сега остава просто да се върнем назад:

(5)
\begin{eqnarray} \mathcal{A}_s \underset{w^x_a}\models \psi[x/f_\varphi(x_1, \dots, x_n)] &\overset{(\star)}\rightarrow& \mathcal{A}_s \underset{w}\models \exists x \psi \\ &\leftrightarrow& \mathcal{A}_s \underset{v}\models \forall x_1 \dots \forall x_n \exists x \psi \end{eqnarray}

$(\star)$ идва от тавталогията.
С това твърдението е доказано.
(iii) Следва от предните две:
Ако $\varphi$ е изпълнима, тогава съществува структура $\mathcal{A}$ , в която да е истина (няма нужда от оценка, понеже формулата е затворена). Сега използваме (ii) и получаваме, че съществува друга структура $\mathcal{A}_s$ в която $\varphi_s$ е вярна. Следователно $\varphi_s$ е изпълнима.
Ако $\varphi_s$ е изпълнима, тогава съществува структура $\mathcal{A}_s$, в която е вярна. Сега използваме (i) и заключаваме, че в структурата $\mathcal{A}_s$ е вярна и $\varphi$ (защото импликацията е истина, предпоставката е истина, следователно и това което следва е истина). Следователно $\varphi$ е изпълнима.

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

Нека $\varphi$ е затворена формула в ПНФ. Тогава:
(i) $\models \varphi^S \Rightarrow \varphi$
(ii) Ако $\mathcal{A}$ е структура и $\mathcal{A} \models \varphi$, то съществува обогатяване $\mathcal{A}^S$, такова че $\mathcal{A}^S \models \varphi^S$
(iii) $\varphi$ е изпълнима т.с.т.к. $\varphi^S$ е изпълнима.

Доказателство: Просто прилагаме многократно свойствата за едностъпкова скулемизация.

Следствие за множество формули

Нека $\Gamma$ е множество от затворени формули в ПНФ. Нека $\Gamma^S \rightleftharpoons \{ \varphi^S\ |\ \varphi \in \Gamma \}$, то:
(i) Ако $\mathcal{B} \models \Gamma^S$, то $\mathcal{B} \models \Gamma$;
(ii) Ако $\mathcal{A} \models \Gamma$, то съществува обогатяване $\mathcal{A}^S$ на $\mathcal{A}$, такова че $\mathcal{A}^S \models \Gamma^S$;
(iii) $\Gamma$ е изпълнимо т.с.т.к. $\Gamma^S$ е изпълнимо.

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