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

Предисловие

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

Синтаксис

Синтаксисът се грижи за начина, по който записваме нещата. Обикновенно когато се говори за синтаксис става дума за букви и думи. Буква е най-малката градивна частица която се използва, докато дума е просто последователност от букви. Не се обърквайте с аналогията от реалния свят - буква може да бъде всеки специален символ - да речем $\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}$.

Пример

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

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

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

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

  • всички символи от логическата част, с формално равенство
  • $\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$.
Unless otherwise stated, the content of this page is licensed under Creative Commons Attribution-NonCommercial-ShareAlike 3.0 License