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

Предисловие

В този предмет ще разглеждаме математическите теории и обектите в тях (теореми, задачи, доказателства). Т.е. ще опитаме да обясним математиката с … математика (да - рекурсивно е :-/). Ще се споменават доста пъти думи като синтаксис и семантика. Ще опитам да обясня веднъж завинаги кое какво означава:

Синтаксис

Синтаксисът се грижи за начина, по който записваме нещата. Обикновенно когато се говори за синтаксис става дума за букви и думи. Буква е най-малката градивна частица която се използва, докато дума е просто последователност от букви. Не се обърквайте с аналогията от реалния свят - буква може да бъде всеки специален символ - да речем $\Rightarrow$ и $)$ - всичко зависи как си дефинираме азбуката, върху която работим.

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

Занимавахме се с подобни неща на курса по Дискретна Математика и ЕАИ - ставаше дума за формални езици, принадлежност на думи към език, регулярни езици и т.н. Тук ще използваме само най-базовите понятия.

Семантика

Семантиката се грижи за това какъв смисъл имат думите. Да разгледаме следните думи:

• a+b
• (+ a b)
• събираме променливата a с променливата b
• add eax bax
• 010010101100010001111101…

Всички те са просто последователности от букви (разгледани от синтактична гледна точка). Освен това всички те са различни, защото няма никои две думи, които да съдържат еднакви букви в еднаква последователност.
Но от семантична гледна точка тези последователности може и да са еднакви:

a+b	C++
(+ a b)	Scheme / Lisp
събираме променливата a с променливата b	човек
add eax bax	асемблер
010010101100010001111101…	машинен код

Т.е. ако кажем подходящите думи на нещо, което ги интерпретира/разбира по някакъв начин може да се окаже, че различни думи имат еднакъв смисъл.
Всъщност придаването на семантика на синтаксиса е превод от един формален език на друг. Например, ако компилаторите на C++ и Lisp получат съответната дума може би ще я преобразуват до асемблер кода, който пък ще бъде превърнат до машинен код, който накрая ще бъде изпълнен от компютър. Ако човек прочете коя да е от думите и е наясно със съответния компилатор, той ще си я преведе на "човешки език" - "събираме променливата a с променливата b" (в случая разглеждаме човешкия език като формален … за простота на изложението :)).

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

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

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

Може да разбием всеки ЕПС на логическа и нелогическа част. Най-общо казано, логическата част е една и съща за всички езици, докато нелогическата част може да се мени от един език до друг.

Логическа част

(1) Индивидни променливи

$\mathrm{Var} = \{ x_0, x_1, \cdots \}$ е изброимо множество от индивидни променливи.

(2) Съждителни връзки

Съждителна връзка (означение)	Наименование
$\lnot$	не
$\And$	конюнкция
$\lor$	дизюнкция
$\Rightarrow$	импликация
$\iff$	еквивалентност

(3) Квантори

Означение	Наименование
$\forall$	квантор за всеобщност
$\exists$	квантор за съществуване

(4) Помощни символи

Лява и дясна кръгли скоби и запетайка: $(\ )\ ,$

(5) Формално равенство

Ще бележим $\dot=$.
Това е незадължителен двуместен предикатен символ със специална семантика.

Нелогическа част

(1) Индивидни константи

Ще бележим азбуката на индивидните константи с $\mathbb{C}\mathrm{onst}$. Това са просто букви, с които ще се отбелязват интересни елементи в езика - например единичният елемент на групата $e$ или $0, 1$ в поле.

(2) Предикатни символи

Ще бележим азбуката на предикатните символи с $\mathbb{P}\mathrm{red}$.

(3) Функционалните символи

Ще бележим азбуката на фукционалните символи с $\mathbb{F}\mathrm{unc}$.

(4) Функция за арност (брой аргументи)

Дефинираме функция $\sharp : \mathbb{P}\mathrm{red} \cup \mathbb{F}\mathrm{unc} \to \{ 0, 1, 2, \cdots \}$, която ще указва всеки предикат или функционален символ по колко аргумента приема. Например ако $p \in \mathbb{P}\mathrm{red}$ и $\sharp[p] = 2$, това означава, че може да пишем $p(x, y)$, но за това по-подробно след малко.

Ако един език съдържа всички букви посочени по-горе, ще го наричаме Език на предикатното смятане, и ще го бележим с $\mathcal{L}$.

Пример

Езикът на групите

Т.е. това е формалният език, с който се разглеждат групите (алгебра):

• $Var = G$
• съждителни връзки $\varnothing$
• квантори $\varnothing$
• ранвество - да
• помощни символи - скоби
• $\mathbb{C}\mathrm{onst} = \{ e \}$ - ще бележим с $e$ единичния елемент на групата;
• $\mathbb{P}\mathrm{red} = \varnothing$ - няма предикати;
• $\mathbb{F}\mathrm{unc} = \{ \cdot \}$ - единствената операция в групата;
• $\sharp[\cdot] = 2$ - операцията е бинарна.

Езикът на Пеановата аритметика

• $Var =$
• съждителни връзки ? ${}$
• квантори $\varnothing$
• ранвество - да
• помощни символи - ${+, (,)}$
• $\mathbb{C}\mathrm{onst} = \{ 0 \}$ - нулата е специален елемент за нас;
• $\mathbb{P}\mathrm{red} = \{ < \}$ - знака по-малко;
• $\mathbb{F}\mathrm{unc} = \{ +, \cdot, S \}$ - събиране, умножение и 'наследник', 'следващ' (successor) - $S(x) = x + 1$;
• $\sharp[+] = \sharp[\cdot] = \sharp[<] = 2 \quad \sharp[S] = 1$.

Предикат

Имаме множество $C$ от обекти.
Изображението $p: C^n \to \{true, false\}$ наричаме предикат.

Функции

Имаме множество $C$ от обекти.
Изображението $f: C^n \to C$ наричаме функция.

Символи над азбука

Символите ги мислете като думи от азбука, но реално са още по-гъвкави понятия.
Имаме някакво множество $A$ от букви.
Правим ново множество като композираме елементи от $A$ и го наричаме $Symbols(A)$ за кратко $S_A$ - символите от азбуката $A$.

Сигнатура

Наредената $( A, \mathrm{S}_{f}, \mathrm{S}_{p}, \# )$ нарчаме сигнатура $\mathcal{S}$, ако:
$A$ - азбука
$\mathrm{S}_{f} \subset Symbols(A)$ - функционални символи
$\mathrm{S}_{p} \subset Symbols(A)$ - предикатни символи
$\#$ - функция за броя аргументи

$\mathrm{S}_{const} \subset \mathrm{S}_{f}$ за $s_f \in \mathrm{S}_{f}, \#[ s_f] = 0$ - константите са функции с нула брой аргументи.

$\mathrm{S}_{f} \cup \mathrm{S}_{p} = \varnothing$
има безкрайно много символи в $Symbols(A)$ непринадлежащи на $\mathrm{S}_{f} \cup \mathrm{S}_{p}$

Забележка: $\mathrm{S}_{f}$ е само множество от думички, но функцията $\#$ може да съпостави на тези думички брой аргументи.

Лексика

Наредената $\langle A, \mathrm{S}_{f}, \mathrm{S}_{p}, \#, \mathrm{S}_{v} \rangle$ нарчаме Лексика $\mathcal{L}$, ако:
$A$ - азбука(множество, което не съдържа символи за скоби примерно, но може да се правят манджи и с тях)
$\mathrm{S}_{f} \subset Symbols(A)$
$\mathrm{S}_{p} \subset Symbols(A)$
$\#$ - функция за броя аргументи
$\mathrm{S}_{v} \subset Symbols(A)$ - индивидни променливи(символи изпозлвани за имена на променливи)

$\mathrm{S}_{f} \cup \mathrm{S}_{p} = \varnothing$ същото и с $\mathrm{S}_{v}$
има безкрайно много думи в $Symbols(A)$ непринадлежащи на $\mathrm{S}_{f} \cup \mathrm{S}_{p}$ същото и с $\mathrm{S}_{v}$

Структура за лексика

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

Нека $\mathcal{L}$ e лексика(език на предикатно смятане).

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

• $C \neq \varnothing$ - универсум на структурата(множеството от обекти с което ще работим в нашия език);
• $\mathbb{I}$ е интерпретация, където: (множеството от функции и предикати, с който ще работим в нашия език)

* $\mathbb{I}[s_p] : C^k \to \{ true, false \}$, където $s_p \in \mathrm{S}_{p}$ и $\sharp[s_p] = k$;
* $\mathbb{I}[s_f] : C^{k} \to C$, където $s_f \in \mathrm{S}_{f}$ и $\sharp[s_f] = k$.

Структурата задава за всеки символ на функция - истинска функция. Аналогично за предикати.
Тези функции/предикати работят с членове на множеството $C$.

Обикновено като пишем структура ще изброяваме интерпретациите на константите, функциите и предикатите в този ред:

(1)

\begin{align} \mathcal{C} = \langle C, \mathbb{I}[f_1], \mathbb{I}[f_2], \cdots, \mathbb{I}[p_1], \cdots \rangle \end{align}

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

Примери

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

(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{C}$ е структура за $\mathcal{L}$.
Оценка $v$ в $\mathcal{C}$ наричаме изображението $v : \mathrm{\mathrm{S}_{v}} \to C$, т.е $v(s_v) \in C$.
За всяка индивидна променлива задаваме стойност от множеството $C$ от структурата $\mathcal{C}$