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

Съкращение:
FOL означава First-Order Predicate Language.

Терм

Дефиниция (терм)

Индуктивна дефиниция (спомнете си дефиницията на кореново дърво от ДМ):

1. Всяка индивидна променлива е терм;
2. Всяка индивидна константа е терм;
3. Ако $\tau_1, \tau_2, \cdots, \tau_n$ са термове, а $f \in \mathbb{F}\mathrm{unc}$ и $\sharp[f] = n$, то $f(\tau_1, \tau_2, \cdots, \tau_n)$ също е терм.

Ще бележим термовете над езика $\mathcal{L}$ с $\mathcal{T}_\mathcal{L}$.
Забележка: Терм е чисто синтактично понятие. Когато казваме, че $f(\tau_1, \cdots, \tau_n)$ е терм, имаме предвид, че ако поставим буквата $f$ (която всъщност е буква за отбелязване на функции), последвана от буквата $($, последвана от думата $\tau_1$, последвана от запетайка ($,$) и т.н., ще получим нова дума и тази дума ще бъде терм според дефиницията.

Примери

Следните думи са термове в езика на Пеановата аритметика: $x$, $e$, $\cdot(x, x)$, $\cdot(x, \cdot(x, x))$, $S(0)$, $+(S(x), S(S(0)))$.
Забележка: Под $\cdot(x, x)$ всъщност 'разбираме' $x \cdot x$ (кога е правилно операцията да стои отпред и кога - между аргументите си, ще спорим друг път).

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

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

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

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

Структура за език на предикатното смятане

Дефиниция (структура за език)

Нека $\mathcal{L}$ e FOL.
Структура за $\mathcal{L}$ ще наричаме наредена двойка $\mathcal{A} = \langle A, \mathbb{I} \rangle$, където:

• $A \neq \varnothing$ - универсум на структурата;
• $\mathbb{I}$ е интерпретация, където:
  • $\mathbb{I}[c] \in A$, за всяка константа $c \in \mathbb{C}\mathrm{onst}$;
  • $\mathbb{I}[p] \subseteq A \times A \times \cdots \times A = A^k$, където $p \in \mathbb{P}\mathrm{red}$ и $\sharp[p] = k$;
  • $\mathbb{I}[f] : A^{\sharp[f]} \to A$, където $f \in \mathbb{F}\mathrm{unc}$.

Структура на един език просто задава универсум (свят, в който се намират елементите) и 'смисъл' на константите, функциите и предикатите.
Обикновено като пишем структура ще изброяваме интерпретациите на константите, функциите и предикатите в този ред:

(1)

\begin{align} \mathcal{A} = \langle A, \mathbb{I}[c_1], \mathbb{I}[c_2], \cdots, \mathbb{I}[f_1], \cdots, \mathbb{I}[p_1], \cdots \rangle \end{align}

Забележка: Понякога вместо $\mathbb{I}[x]$ ще пишем просто $x^\mathcal{A}$, което означава точно интерпретацията на $x$ в структурата $\mathcal{A}$ (тъй като интерпретацията $\mathbb{I}$ е част от структурата $\mathcal{A}$).

Примери

Структура на Пеановата аритметика:

(2)

\begin{align} \langle \mathbb{N}, 0, \cdot, +, < \rangle \end{align}

Структура на Пеановата аритметика само с 1 елемент:

(3)

\begin{align} \langle \{ \pi \}, \pi, H, H, Id, \{ \langle \pi, \pi \rangle \} \rangle \quad H(\pi, \pi) = \pi \end{align}

Измислена структура с 3 елемента:

(4)

\begin{eqnarray} A &=& \{ 5, 17, 205 \} \\ \mathcal{A} &=& \langle A, 17, F \rangle \\ F&:& A \times A \to A \\ F(a, b) &=& 205 \end{eqnarray}

Оценка в език на предикатното смятане от 1ви ред

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

Нека $\mathcal{L}$ е FOL.
Нека $\mathcal{A}$ е структура за $\mathcal{L}$.
Оценка $v$ в $\mathcal{A}$ наричаме изображението $v : \mathrm{Var} \to A$, т.е $v(x) \in A$.

Дефиниция (стойност на терм)

Нека $\mathcal{L}$ е FOL, $\mathcal{A}$ е структура за $\mathcal{L}$ и $v$ е оценка. За всеки терм $\tau$ от $\mathcal{L}$ дефинираме стойност на $\tau$ в $\mathcal{A}$ при оценка $v$. Ако $\tau$ е терм, стойноста му в структура $\mathcal{A}$ и оценка $v$ ще отбелязваме с $\|\tau\|^\mathcal{A}[v]$. Дефиницията ще извършим по индукция:

• Ако $\tau$ е индивидна променлива $\tau = x$, тогава стойността е просто оценката на $x$ : $\|x\|^\mathcal{A}[v] \leftrightharpoons v(x)$;
• Ако $\tau$ е индивидна константа $\tau = c$, стойността не зависи от оценката, а само от интерпретацията (т.е. от $\mathcal{A}$): $\|c||^\mathcal{A}[v] \leftrightharpoons c^\mathcal{A}$;
• И в общия случай, когато $\tau$ е функция приложена към няколко терма $\tau = f(\tau_1, \cdots, \tau_n)$, където $\sharp[f] = n$, $f \in \mathbb{F}\mathrm{unc}$ и $\tau_i$ са термове, за който $\|\tau_i\|^\mathcal{A}[v]$ е дефинирано, тогава просто заместваме $f$ с неговата интерпретация и термовете с техните оценки:

(5)

\begin{align} \|f(\tau_1, \cdots, \tau_n) \|^\mathcal{A}[v] \leftrightharpoons f^\mathcal{A}(\|\tau_1\|^\mathcal{A}[v], \cdots, \|\tau_n\|^\mathcal{A}[v]) \end{align}

Забележка: $\leftrightharpoons$ означава "равно по дефиниция". Ще го използваме консистентно оттук нататък.

Дефиниция (Var[t])

Нека $\tau$ е терм. С $\mathrm{Var}[\tau]$ ще отбелязваме всички променливи, срещащи се в $\tau$. Строгата дефиниция е по индукция:

• $\mathrm{Var}[x] \leftrightharpoons \{ x \} \quad x \in \mathrm{Var}$
• $\mathrm{Var}[c] \leftrightharpoons \varnothing \quad c \in \mathbb{C}\mathrm{onst}$
• $\mathrm{Var}[f(\tau_1, \cdots, \tau_n)] \leftrightharpoons \mathrm{Var}[\tau_1] \cup \cdots \cup \mathrm{Var}[\tau_n]$

Дефиниция (рестрикция)

Нека $f : A \to B$ е функция и $R \subseteq A$ е подмножество на дефиниционното множество на $f$.
$f \upharpoonright R$ или рестрикция на $f$ до $R$ наричаме функцията $f' : R \to B$, за която $f'(x) = f(x)\ \forall x \in R$.
С други думи рестрикцията на функция до множество е нова функция която има по-ограничено дефиниционно множество (не е дефинирана навсякъде, където е дефинирана оригиналната функция), но стойностите които заема са същите като оригиналната функция.

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

Нека $v_1$ и $v_2$ са оценки в $\mathcal{A}$ и $\tau$ е терм.
Ако $v_1 \upharpoonright \mathrm{Var}[\tau] = v_2 \upharpoonright \mathrm{Var}[\tau]$, то $\|\tau\|^\mathcal{A}[v_1] = \|\tau\|^\mathcal{A}[v_2]$.
Т.е. ако имаме две оценки (функции, свързващи всяка индивидна променлива с обект от универсума) и те съпоставят едни и същи обекти на индивидните променливи които се срещат в $\tau$, то стойностите на $\tau$ при $v_1$ и $v_2$ съвпадат.
Доказателство: Ще извършим доказателство по индуктивното построение на $\tau$.

• Нека $\tau = x$. Да видим какво означава $v_1 \upharpoonright \mathrm{Var}[\tau] = v_2 \upharpoonright \mathrm{Var}[\tau]$:

(6)

\begin{eqnarray} v_1 \upharpoonright \mathrm{Var}[\tau] &=& v_2 \upharpoonright \mathrm{Var}[\tau] \iff \\ v_1 \upharpoonright \{ x \} &=& v_2 \upharpoonright \{ x \} \overset{\star}\iff \\ v_1(x) &=& v_2(x) \iff \\ \|x\|^\mathcal{A}[v_1] &=& \|x\|^\mathcal{A}[v_2] \end{eqnarray}

$\star$ - рестрикцията на функция до $\{ x \}$ - интересуваме се от функционалната стойност на $x$. Затова и $v_1(x) = v_2(x)$.

• Нека $\tau = c$. Оценката на индивидните константи не зависи от оценката $v_i$:

(7)

\begin{align} \|c\|^\mathcal{A}[v_1] = c^\mathcal{A} = \|c\|^\mathcal{A}[v_2] \end{align}

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

Първо ще докажем, че стойностите на $\tau_i$ при двете оценки се запазват - за целта трябва да покажем, че $v_1 \upharpoonright \mathrm{Var}[\tau_i] = v_2 \upharpoonright \mathrm{Var}[\tau_i]$ за всяко $\tau_i$ и да използваме индуктивното предположение. От дефиницията на $\mathrm{Var}[\tau]$ имаме:

(8)

\begin{align} \mathrm{Var}[\tau] = \mathrm{Var}[\tau_1] \cup \cdots \cup \mathrm{Var}[\tau_n] \supseteq \mathrm{Var}[\tau_i] \quad \forall i \end{align}

Комбинираме с даденото:

(9)

\begin{align} \left\{\begin{array}{rcl} v_1 \upharpoonright \mathrm{Var}[\tau] &=& v_2 \upharpoonright \mathrm{Var}[\tau] \\ \mathrm{Var}[\tau_i] &\subseteq& \mathrm{Var}[\tau] \\ \end{array}\right\} \Rightarrow v_1 \upharpoonright \mathrm{Var}[\tau_i] &=& v_2 \upharpoonright \mathrm{Var}[\tau_i] \end{align}

Оттук веднага получаваме, че $\|\tau_i\|^\mathcal{A}[v_1] = \|\tau_i\|^\mathcal{A}[v_2]$. Сега остава да разпишем стойността на $\tau$ при двете оценки:

(10)

\begin{align} \left\{\begin{array}{rcccl} \|\tau\|^\mathcal{A}[v_1] &=& \|f(\tau_1, \cdots, \tau_n)\|^\mathcal{A}[v_1] &=& f^\mathcal{A}(\|\tau_1\|^\mathcal{A}[v_1], \cdots, \|\tau_n\|^\mathcal{A}[v_1]) \\ \|\tau\|^\mathcal{A}[v_2] &=& \|f(\tau_1, \cdots, \tau_n)\|^\mathcal{A}[v_2] &=& f^\mathcal{A}(\|\tau_1\|^\mathcal{A}[v_2], \cdots, \|\tau_n\|^\mathcal{A}[v_2]) \\ \end{array}\right\} \Rightarrow \|\tau\|^\mathcal{A}[v_1] = \|\tau\|^\mathcal{A}[v_2] \end{align}

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

Нека $\tau$ е терм. Казваме, че той е затворен ако $\mathrm{Var}[\tau] = \varnothing$.

Следствие (от горното твърдение за затворен терм)

Ако $\tau$ е затворен терм и $v_1, v_2$ са две оценки в структура $\mathcal{A}$, то $\|\tau\|^\mathcal{A}[v_1] = \|\tau\|^\mathcal{A}[v_2] = \tau^\mathcal{A}$.
Т.е. ако термът няма никакви индивидни променливи, неговата стойност зависи единствено от структурата, затова може да записваме $\tau^\mathcal{A}$.

Дефиниция

Ще дефинираме $\tau^\mathcal{A}[[a_1, \cdots, a_k]]$.¹
Нека $x_1, \cdots, x_k$ са индивидни променливи и $\{ x_1, \cdots, x_k \} \supseteq \mathrm{Var}[\tau]$.
Нека $a_1, \cdots, a_k$ са произволни обекти от универсума $A$.
Нека $v_1, v_2$ са две произволни оценки, за които $v_1(x_i) = a_i = v_2(x_i)$ (това е по-силно от $v_1 \upharpoonright \{ x_1, \cdots, x_k \} = v_2 \upharpoonright \{ x_1, \cdots, x_k \}$, защото искаме функциите да съвпадат върху ограниченото множество и специфично задаваме функционалните им стойности).
Сега използваме предното твърдение: $\| \tau \|^\mathcal{A}[v_1] = \|\tau\|^\mathcal{A}[v_2]$. Следователно за произволна оценка, изпълняваща горните условия имаме, че стойността на терма $\tau$ е една и съща. Тя зависи единствено от избора на обекти от универсума $a_1, \cdots, a_k$. Следователно на всеки един такъв избор на обекти може да съпоставим стойност на терма $\tau$ при оценка изпълняваща горепосочените условия. Ще записваме тази съпоставена стойност като $\tau^\mathcal{A}[[ a_1, \cdots, a_k ]]$.

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

Нека $\mathcal{A} = \langle A, \mathbb{I} \rangle$ е структура за $\mathcal{L}$.
Нека $F : A^k \to A$ е функция. Ще казваме, че $F$ е термална, ако съществува терм $\tau$ с $k$ индивидни променливи ($\sharp[\tau] = k$) $x_1, \cdots, x_k$ и
$F(a_1, \cdots, a_k) = \tau^\mathcal{A}[[a_1, \cdots, a_k]]$

Пример

Нека $\mathcal{N} = \langle \{ 0, 1, \cdots \}, 0, S, +, \cdot, < \rangle$ е структура на Пеановата аритметика.

• полиномите с $\mathbb{N}$ коефициенти са термални функции в $\mathcal{N}$;
• функцията $f(x) = 2^x$ не е термална в $\mathcal{N}$;
• функцията $f(x) = x$ е термална;
• функцията $f(x) = c$ е термална, само ако $c \in \mathbb{C}\mathrm{onst}$;

Footnotes

1. За сега си няма име! Ако някой измисли да го допише. Иначе ще го използваме само в следващата дефиниция, така че не е фатално да си остане без име :-)