ML: Логіка та ймовірність. Частина I

Вступ

Здатність до логічних міркувань в умовах невизначеності є важливою складовою будь-якого інтелектуального агента. За допомогою теорії ймовірностей можна узагальнити бінарну логіку на випадок імовірнісних моделей, що буде продемонстровано в наступних статтях. Перед читанням корисно ознайомитися з вступом до логіки, короткому нагадуванню якого і присвячено цей документ.

Теорія про Алісу і Боба

Аліса і Боб живуть у будинку, де у кожного є своя спальня і спільна вітальня. Гостей вони не приймають. У спальні дозволено перебувати тільки її власнику, а у вітальні можуть збиратися обидва мешканці. Відомо, що у вітальні хтось є і Аліса у себе в спальні. Необхідно прийти до висновку, що у вітальні знаходиться Боб.

Твердження теорії будемо записувати за допомогою логічного заперечення $\bar{A}$ (не $A$), кон'юнкції $A\,\&\,B$ (логічного І), диз'юнкції $A\vee B$ (логічного АБО) і імплікації $P\to Q$, що скорочує фразу "якщо $P$, то $Q$". Нагадаємо, що, якщо $\T$ - це істинне твердження, а $\F$ - хибне, то для будь-якого висловлювання $P$: $$ \left\{ \begin{array}{lcl} \T~\,\&\,P & \equiv & P\\ \F~\&\,P &\equiv & \F \end{array} \right. ~~~~~~~~~~~~~~~ \left\{ \begin{array}{lcl} \F\,\vee P &\equiv & P\\ \T\,\,\vee P & \equiv & \T \end{array} \right. ~~~~~~~~~~~~~~~ \left\{ \begin{array}{lclcl} \T\,\to \F &\equiv& \F\\ \T\,\to \T &\equiv& \F\,\to P &\equiv& \T, \end{array} \right. $$ де $\T\,\&\,P \equiv P$ при $P\equiv \F$ і $P\equiv \T$ відповідає $\T\,\&\,\F \equiv \F$ (істина і хиба - це хиба) і $\T\,\&\,\T \equiv \T$. Таким чином, ці формули є коротким записом таблиць істинності для логічних бінарних операцій $\&,~\vee,~\to$.

Позначимо через $A$ висловлювання: "Аліса у себе в спальні", через $B$ - "Боб у себе в спальні" і $L$ - "хтось один з них або обидва знаходяться у вітальні". Як аксіоми, що описують цей світ, виберемо такі факти:

Вихідні посилки: $L$ (хтось у вітальні), $A$ (Аліса в спальні) і аксіома $\mathbf{A_1}$ дозволяють зробити необхідний висновок, який складається з трьох кроків: $$ \begin{array}{llclll} 1. & L,~~~~L\to \bar{A}\vee \bar{B} & \Rightarrow & \bar{A}\vee \bar{B} & ~~~~~~~~~~~& L,\mathbf{A_1},~(\text{MP})\\ 2. & \bar{A}\vee \bar{B} & \Leftrightarrow & A \to \bar{B} & & 1,~\text{def}\\ 3. & A,~~~~A \to \bar{B} & \Rightarrow & \bar{B} & & A,2,~(\text{MP}) \end{array} $$ На першому кроці застосовано правило логічного виведення modus ponens (MP): $$ P,~~P\to Q~~~~\Rightarrow~~~~Q. $$ Це правило звучить так: "якщо істинна формула $P$ і з $P$ випливає формула $Q$, то істинна і $Q$". Його справедливість пов'язана з властивістю імплікації, яка хибна тільки для $\T\to \F~~$ ("з істини $\T $ не можна отримати хибу $\F $"). Тому, якщо $P~\equiv~\T$ і $P\to Q~\equiv~\T $, тобто $\T\to Q~\equiv~\T $, то для $Q$ можливо тільки: $Q\equiv~\T $.
На другому кроці виведення враховано запис імплікації через диз'юнкцію. Це також правило виведення (отримання нової формули). На відміну від modus ponens, воно двостороннє: $~~P\to Q~~~\Rightarrow~~~\bar{P}\vee Q~~$ і $~~\bar{P}\vee Q~~~\Rightarrow~~~P\to Q$.
Наприкінці знову використано (MP). Таким чином, за допомогою формальних дій із символами, ми приходимо до правильного висновку про те, що $\bar{B}$: "Боб не знаходиться у себе в спальні". Для цього нам знадобилася тільки перша аксіома, тим не менш усі три аксіоми є незалежними і необхідні для опису цього світу.

Теорії предикатів першого порядку

У неформальних теоріях ми використовуємо природну мову для опису об'єктів і їхніх властивостей. При цьому неминучі неоднозначності, притаманні нашому мисленню. Формалізація предметної теорії означає запис усіх її тверджень у вигляді формул за допомогою однозначних символів. Отримання одних тверджень з інших виконується за також однозначними правилами. У результаті синтаксис теорії (її форма) відривається від семантики (змісту) і жодні "очевидності" неявно привнесені бути не можуть. Логічний вивід такої теорії може перевірити, наприклад, комп'ютер, який нічого не знає про сенс її символів.

Побудова формальної предметної теорії починається з її сигнатури, у якій перелічуються типи предметів, константи, функції і предикати. Типи предметів визначаються множинами сутностей з якими буде оперувати теорія. В арифметиці це множина чисел, а в планіметрії - дві множини: точки $x,y,...\in \mathcal{P}$ і прямі $\alpha,\beta,...\in \mathcal{L}$. Частина сутностей можуть оголошуватися виділеними предметними константами (наприклад, $0$ в арифметиці). У сигнатурі теорії можливі також предметні функції $f(x)$, $g(x,y)$, $h(x,y,z)$,..., що ставлять у відповідність одним предметам - інші (наприклад, $\text{sum}(x,y)$ або коротко $x+y$ в арифметиці). Константи, змінні і функції називаються термами. Приклад терма: $h(0,x,g(x,y))+f(z)$.

Важливою і обов'язковою частиною сигнатури є предикати - логічні функції, що залежать від предметних величин: $A(x)$, $B(x,y)$,.... і набувають значень істини $\T $ або хиби $\F $. Логічні висловлювання, подібні до $A,B,L$, розглянуті в попередньому розділі, це окремі випадки константних предикатів без аргументів.
Властивість - предикат з одним аргументом $A(x)$. Він задає деяку підмножину $\{x\,|\,A(x)\}\subseteq\mathcal{X}$ предметів.
Відношення - предикат $R(x,y)$ з двома аргументами. Їх часто записують в операційному вигляді $(x\, R\, y)$.
В арифметиці предикатами є: рівність чисел $x=y$ і їхній порядок $x\lt y$. У буденних знаннях, наприклад, $\text{Mather}(x,y):$ "хтось $x$ є матір'ю $y$" або $(x~\text{in}~y):$ "об'єкт $x$ знаходиться всередині об'єкта $y$".

Після фіксування сигнатури, записується набір формул, які визначають властивості констант, функцій і предикатів. Ці формули називаються предметними аксіомами. Крім них існують загальнологічні аксіоми, застосовні до будь-яких предметних теорій і правила виведення (способи отримання нових формул).

Булева алгебра

При записі тверджень теорії (аксіом і теорем), крім символів сигнатури беруть участь логічні зв'язки: заперечення $\neg A$ або коротко $\bar{A}$ (не $A$, $A$ - невірно), диз'юнкція $A\vee B$ (істинно або $A$, або $B$, або обидва) і кон'юнкція $A\,\&\,B$ (істинно і $A$, і $B$). Диз'юнкція і кон'юнкція мають "звичайні" властивості комутативності і асоціативності, подібно до додавання чи множення. Між собою вони пов'язані законами дистрибутивності і правилами де Моргана:

$$ \left\{ \begin{array}{lcl} A\,\&\,(B\vee C) &\leftrightarrow& (A\,\&\,B)\vee (A\,\&\,C)\\ A\vee(B\,\&\, C) &\leftrightarrow& (A\vee B)\,\&\, (A\vee C) \end{array} \right. ~~~~~~~~~~~~~~~~~~~~~~ \left\{ \begin{array}{lcl} \neg(A\,\&\,B) &\leftrightarrow& \neg A\vee \neg B \\ \neg(A\vee B) &\leftrightarrow& \neg A\,\&\, \neg B \end{array} \right. $$ Стрілка в обидва боки $A\leftrightarrow B$ (або що те саме $A\equiv B$) позначає булеву операцію логічної еквівалентності, яка істинна тільки при збігу значень аргументів. Наприклад, $\T\leftrightarrow \T$ дорівнює $\T,~~$ а $~~\F\leftrightarrow \T$ дорівнює $\F$.
Ця операція виражається через імплікацію, а імплікація, у свою чергу, виражається через диз'юнкцію: $$ A\leftrightarrow B ~~~~~\Leftrightarrow ~~~~~(A\to B)\,\&\,(B\to A), ~~~~~~~~~~~~~~~~~~~~~~~~ A\to B ~~~~~\Leftrightarrow ~~~~~\neg A\vee B. $$ Подвійна стрілка $\Leftrightarrow$ позначає замінюваність однієї формули на іншу і навпаки. Це можливо, тому що при будь-яких фіксованих істиннісних значеннях $A,B$ формули зліва і справа від стрілки $\Leftrightarrow$ набувають однакових значень $\T$ або $\F$. У принципі, у законах дистрибутивності і правилах де Моргана також можна використовувати $\Leftrightarrow$, тоді вони будуть не формулами, а правилами виведення (способами отримання нових формул). Зазначимо також специфічні для булевої алгебри правила поглинання і завжди хибні та істинні формули: $$ \left\{ \begin{array}{lcl} A\,\&\,A &\leftrightarrow& A\\ A\vee A &\leftrightarrow& A \end{array} \right. ~~~~~~~~~~~~~~~~~~~~~ \left\{ \begin{array}{lcl} A\,\&\,(A\vee B) &\leftrightarrow& A \\ A\vee (A\,\&\,B) &\leftrightarrow& A \end{array} \right. ~~~~~~~~~~~~~~~~~~~~~ \left\{ \begin{array}{lcl} A\,\&\,\neg A &\equiv& \F \\ A\vee \neg A &\equiv& \T \end{array} \right. $$ Всі ці приклади тотожностей булевої алгебри є тавтологіями (завжди істинними формулами), що перевіряються за допомогою таблиць істинності (перебираються всі значення $\F,~\T$ висловлювань, що входять до них).

Імплікація $A\to B$ у формулах часто використовується для вираження словесних конструкцій типу "якщо $A$, то $B$".
Хоча імплікація істинна і для тверджень "Якщо Париж столиця Англії, то Земля пласка" ($\F \to \F$ істинно), але зазвичай існує деякий причинний зв'язок між посилкою $A$ і наслідком $B$. Важливо пам'ятати, що стверджуване в імплікації передбачає істинність посилки. Що буде при її хибності - замовчується. Фраза "Якщо Машу не чіпати, то вона буде щаслива", нічого не повідомляє про те, що станеться, якщо Машу торкнутися.
Аналогічно, в арифметиці при будь-якому $x$, істинна формула $(x\lt 2) \to (x\lt 4)$. Коли посилка істинна ($x=1$), істинний і наслідок. Якщо посилка хибна, то наслідок може бути як істинним ($x=3$), так і хибним ($x=5$).

Квантори

Важливу роль при побудові формул формальної теорії відіграють квантори:

Для скінченних множин $x\in\{a_1,\,...,\,a_n\}$ квантори еквівалентні ланцюжку диз'юнкцій і кон'юнкцій: $$ \exists_x \,P(x)~~~\Leftrightarrow~~~P(a_1)\vee P(a_2)\vee .... \vee P(a_n),~~~~~~~~~~~~~~~ \forall_x \,P(x)~~~\Leftrightarrow~~~P(a_1)\,\&\, P(a_2)\,\&\, .... \,\&\, P(a_n). $$ Дійсно, "існує" означає, що або $P(a_1)$ істинне, або $P(a_2)$ істинне, або,...(хоча б одне з них). Аналогічно повинні бути істинними всі $P(a_i)$ для квантора загальності.

Для скінченних множин $\exists_x \,P(x)$ і $\forall_x \,P(x)$ можна обчислити, знаючи істинність предиката $P(x)$ для кожного $x$. Для нескінченних множин це вже не так. Точніше, якщо множина зліченна і об'єкт з властивістю $P(x)$, існує, то рано чи пізно він зустрінеться в ланцюжку $P(a_1)\vee P(a_2)\vee...$ Якщо ж такого об'єкта немає, "переборний алгоритм" ніколи не зупиниться. Аналогічно, якщо формула $\forall_x\, P(x)$ істинна, то перебором цього перевірити не можна, хоча можна встановити її хибність, отримавши $P(a_i)\equiv 0$.

Квантори аналогічні знаку підсумовування і їхній "індекс" може бути позначений будь-якою змінною.
Формула, у якій усі змінні пов'язані кванторами, називається замкнутою (що не містить вільних змінних). Наприклад, нехай квантори у виразах мають найвищий пріоритет (діють першими). Тоді формула $\forall_x\,P(x,y)~\to~\exists_y\,Q(x,y)$ - це предикат $F(x,y)$ з двома аргументами: $ \bigr(\forall_u\,P(u,y)\bigr)~\to~\bigr(\exists_v\,Q(x,v)\bigr). $
Вільні змінні (вище $x,y$) називають параметрами формули, а пов'язані ($u,v$) - просто змінними.

Однотипні квантори можна переставляти місцями (і також для квантора існування $\exists$): $$ \forall_x\,\forall_y \,P(x,y) ~~~~~\Leftrightarrow~~~~~ \forall_y\,\forall_x\, P(x,y)~~~~~\Leftrightarrow~~~~~ \forall_{x,y}\, P(x,y). $$ Різнотипні квантори у загальному випадку переставляти не можна. Так, $\forall_y\, \exists_x \,\text{Mather}(x,y)$ означає, що у кожного $y$ є мати $x$, а $\exists_x\,\forall_y\, \text{Mather}(x,y)$ означає, що існує така $x$, яка є матір'ю всіх, включаючи саму себе.

Для кванторів, за допомогою булевої алгебри, неважко отримувати різні тотожності. Наприклад, з правил де Моргана випливає, що не існує такого $x$, що $P(x)$ істинне, еквівалентно, що для всіх $P(x)$ хибне: $$ \neg\exists_x\,P(x)~~~\Leftrightarrow~~~\forall_x\,\neg P(x), ~~~~~~~~~~~~~~~~~~~ \neg\forall_x\,P(x)~~~\Leftrightarrow~~~\exists_x\,\neg P(x). $$ Для будь-якого квантора ($\text{K}_x$ це $\forall_x$ або $\exists_x$) виконуються правила розширення дії, а для "споріднених" операцій ($\&$ для $\forall$ і $\vee$ для $\exists$) - правила об'єднання: $$ \left\{ \begin{array}{lcl} \text{K}_x\, P(x)\,\&\, Q~~~&\Leftrightarrow&~~~ \text{K}_x\, \bigr(P(x)\,\&\, Q\bigr)\\ \text{K}_x\, P(x)\vee Q~~~&\Leftrightarrow&~~~ \text{K}_x\, \bigr(P(x)\vee Q\bigr)\\ \end{array} \right. ~~~~~~~~~~~~~~~~~~~ \left\{ \begin{array}{lcl} \forall_{x}\,P(x)~\,\&~\forall_{y}\,Q(y)~~~&\Leftrightarrow&~~~\forall_{x}\,\bigr(P(x)\,\&\,Q(x)\bigr) \\ \exists_{x}\,P(x)\,\vee\,\exists_{y}\,Q(y)~~~&\Leftrightarrow&~~~ \exists_{x}\,\bigr(P(x)\vee Q(x)\bigr) \end{array} \right. $$ У правилах розширення важливо, що формула $Q$ не залежить від змінної $x$ (але може залежати від параметрів). Завдяки цьому, $Q$ дорівнює або $\T$, або $\F$. Перебираючи ці два варіанти легко перевірити істинність цих правил.

◊ Нехай $x\in \mathbb{Z}=\{0,\pm 1,\pm 2,...\}$ (цілі числа), функція додавання $x+y$ і предикат рівності $x=y$ визначені звичайним чином. Для наведених нижче формул перші дві істинні, а другі дві - хибні: $$ (a)~~~\exists_{x,y}\,[x+y=5],~~~~~~~~~~(b)~~~\forall_x\,\exists_y\,[x+y = 5],~~~~~~~~(c)~~~\forall_{x,y}\,[x+y = 5],~~~~~~~(d)~~~\exists_y\,\forall_x\,[x+y = 5]. $$ Для $(a)$ існують, наприклад $x=2$, $y=3$. У $(b)$, для будь-якого $x$ існує $y=5-x$.

◊ Для натуральних чисел $x\in\mathbb{N}=\{0,1,2,...\}$ виразимо (визначимо) відношення $x\mid y:$ "число $x$ ділиться на $y$" через функцію множення $x\cdot y$ і запишемо такі твердження: "Деякі парні числа діляться на $4$"; "Кожне число, що ділиться на $4$, ділиться і на $2$": $$ (x\mid y) ~~~\Leftrightarrow~~~\exists_z\,(x=y\cdot z)~~\&~~y\neq 0,~~~~~~~~~~~~ \exists_x\,\bigr[\, (x\mid 2)~\&~(x\mid 4)\,\bigr],~~~~~~~~~~~~ \forall_x\,\bigr[\,(x\mid 4) ~\to~(x\mid 2)\,\bigr]. $$

Пренексною формою формули називається її еквівалентний запис у якому дія всіх кванторів охоплює формулу. Наприклад, $$ \forall_x\, P(x)\,\&\,\exists_y\,Q(y)~\to~\exists_z\,R(z)~~~~~\Leftrightarrow~~~~~~ \exists_x\, \bar{P}(x)~\vee~ \forall_y\,\bar{Q}(y)~\vee~\exists_z\,R(z) ~~~~~\Leftrightarrow~~~~~~\exists_x\,\forall_y\,\bigr[ P(x)\,\&\,\,Q(y)~\to~R(x)\bigr], $$ де після усунення імплікації, застосовано правило об'єднання для $\exists_x,\,\exists_y$, а потім правила розширення.

Інтерпретації теорії

Інтерпретація формальної теорії - це надання елементам сигнатури змістовного сенсу (семантики).
Для цього задаються конкретні непорожні множини (зі скінченного або нескінченного числа елементів). На цих множинах визначаються константи, дії функцій і значення ($\F ,\T $) предикатів.

Якщо в сигнатурі є тільки висловлювання, то загальнозначуща формула називається тавтологією ($A\vee \neg A$).
Якщо підформули довільної формули можна позначити як висловлювання таким чином, щоб вийшла тавтологія, то ця формула загальнозначуща. Наприклад, $\forall_x\,P(x) \,\vee\, \neg \forall_y\,P(y)$ - це тавтологія. У той же час загальнозначуща формула $\forall_x P(x)\,\to \exists_y\,P(y)$ тавтологією не є.

Модель формули - це інтерпретація в якій ця формула істинна. Якщо модель є, то формула виконувана.
Модель теорії - це інтерпретація в якій істинні всі аксіоми і теореми теорії.

◊ Розглянемо предметну теорію з двома предикатами: $x=y$ (рівність), $x \prec y$ (порядок) і однією функцією: $x\circ y$ (що б вона не позначала). Візьмемо множину з трьох елементів, які пронумеруємо числами: $\mathbb{X}=\{0,1,2\}$. На цій множині визначимо дві різні інтерпретації:

У таблицях для предикатів точка позначає істину, а хрестик - хибу. Наприклад $2=2$ істинно, $2=1$ - хибно. Предикат $x=y$ в обох інтерпретаціях визначений однаково, а решта об'єктів сигнатури мають різні значення. Легко перевірити, що в обох сигнатурах істинна формула $\forall_{x,y}\,[ (x\circ y) = (y\circ x) ]$ (комутативність). Формула $\forall_x\,\exists_y\, (x\prec y)$ хибна в першій інтерпретації і істинна в другій, а $\exists_x\,\forall_y\,(x\prec y)~\to~\forall_y\,\exists_x\,(x\prec y)$ істинна в обох інтерпретаціях (насправді це загальнозначуща формула).

Логічне слідування

Уявімо собі множину інтерпретацій $\mathcal{I}$, елементами якої є предметні множини із заданими на них інтерпретаціями. Дві однакові множини, на яких по-різному визначені функції і предикати - це різні елементи множини $\mathcal{I}$. Будемо вважати, що будь-яка замкнута формула (без параметрів) у даній інтерпретації або істинна, або хибна (для скінченних множин це очевидно). Тоді на множині інтерпретацій $\mathcal{I}$ існують підмножини істинності кожної формули (множина її моделей).

З формули $P$ логічно випливає формула $Q$, якщо завжди, коли істинна $P$, буде також істинна і $Q$. На множині інтерпретацій область істинності $P$ - це підмножина істинності $Q$. Наслідок прийнято позначати так: $P\vDash Q$, а якщо $Q$ загальнозначуща, то: $\vDash Q$.

Логічний вивід $\mathcal{P}\Rightarrow Q$ - це отримання з формул $\mathcal{P}$ нової формули $Q$, так що $\mathcal{P}\vDash Q$. Наприклад, у modus ponens: $P,~P\to Q~ \Rightarrow~ Q$ (MP), з формул $P$ і $P\to Q$ виводима $Q$. При цьому $Q$ істинна щонайменше на тих же інтерпретаціях, де істинні $P$ і $P\to Q$.

Визначення логічного виводу і імплікації призводять до такого корисного твердження:

якщо $~~P\Rightarrow Q,~~$ то $~~~\vDash~P\to Q~~$ (формула є загальнозначущою) і навпаки за (MP).
Наприклад, вивід за modus ponens еквівалентний загальнозначущій формулі $(P\,\&\,(P\to Q)) \to Q$, яка, у свою чергу, еквівалентна $(P\,\&\,Q)\,\to\,Q$.

Ще одна загальнозначуща формула $P\to (P\vee Q)$ відповідає логічному виводу $P~\Rightarrow~ P\vee Q$ (якщо істинно $P$, то незалежно від значення формули $Q$ буде істинним і $P\vee Q$).

Праворуч на малюнку наведена деяка теорія з двома аксіомами $A_1,A_2$. Їхні області істинності обмежені жирними лініями. З аксіом випливають три формули (= теореми) $T_1, T_2, T_3$. Це так, тому, що перетин областей істинності аксіом $A_1$, $A_2$ (зафарбована область) є підмножиною областей істинності всіх трьох теорем. Крім цього, існує вивід $T_1\Rightarrow T_2$, однак з $T_1$ або $T_2$ не випливає (і не може бути виведена) $T_3$. Для виводу теорем $T_1$, $T_2$, необхідні обидві аксіоми $A_1$ і $A_2$. Для виводу $T_3$ достатньо тільки аксіоми $A_2$. Формула $T_4$ завжди хибна в даній теорії (логічно випливає і виводиться її заперечення $\neg T_4$).

✒ Наведемо приклади односторонніх правил логічного виводу для формул з кванторами: $$ \forall_x\,P(x)~~~\Rightarrow~~~ P(x)~~~\Rightarrow~~~ P(t)~~~\Rightarrow~~~ \exists_x\,P(x). $$ Перше правило опускання квантора загальності $\forall_x\,P(x)~\Rightarrow~ P(x)$ означає, що якщо твердження $P(x)$ істинне при будь-якому $x$, то формула $P(x)$ буде загальнозначущою (завжди істинною), яке б значення $x$ у неї не підставили. Зворотне слідування, взагалі кажучи, не вірне. Зокрема $P(x)\,\to\,\forall_y\,P(y)$ не загальнозначуща, наприклад для $x\in\{a_1,a_2\}$ для $P(a_1)\equiv\T$, $P(a_2)\equiv\F$ при $x=a_1$. А ось $\forall_y\,P(y)~\to~ P(x)$ - це загальнозначуща формула.

Наступне слідування $P(x)~~\Rightarrow~~ P(t)$ означає можливість підстановки на місце змінної $x$ у вже виведеній формулі $P(x)$ замість параметра $x$ будь-якого терма $t$ (константи, іншої змінної або функції). Так, з формули $x+y=y+x$ виводиться $x+(x+1)=(x+1)+x$ при одночасній заміні $y$ на $x+1$.

Останнє одностороннє слідування $P(t)~\Rightarrow~\exists_x\,P(x)$ означає що, якщо $P(t)$ істинно при даному значенні терма $t$, то це значення (хоча б одне) і існує. У зворотному напрямку таке слідство, у загальному випадку, також невірне і формула $\exists_y\,P(y)~\to~P(x)$ не загальнозначуща (невиконувана на $P(a_1)\equiv \T$, $P(a_2)\equiv \F$ при $x=a_2$).

Якщо формула $Q(x)$ виведена безпосередньо з аксіом (без використання посилок) після опускання квантора загальності $\forall_x\,P(x)~\Rightarrow~ P(x)~\Rightarrow~...~\Rightarrow~Q(x)$, то вона справедлива для будь-якого $x$ і можна застосувати правило узагальнення $Q(x)~\Rightarrow~\forall_x\,Q(x)$.

☯ На жаль, поняття істинності формули на даній інтерпретації добре визначено тільки для скінченних множин. Для нескінченних множин "обчислити" її істинність не завжди можливо. При цьому, є формули, істинні на всіх скінченних множинах і хибні на нескінченних. Наприклад, на скінченних, лінійно впорядкованих множинах з відношенням $x\preceq y$ завжди є найбільші елементи: $\exists_y\forall_x (x\preceq y)$. Для нескінченних множин, наприклад, натуральних чисел - це вже не так.

Тим не менш, концепція існування підмножин істинності формул на множині інтерпретацій важлива для розуміння аксіоматичних властивостей формальних теорій і іноді виявляється корисною на практиці. Наприклад, замість побудови виводу формули з аксіом, інтелектуальна система може переконатися в її "емпіричній істинності", виконавши перевірку логічного слідування на великому числі інтерпретацій.

Доведення від протилежного

Малюнок праворуч ілюструє дуже потужний спосіб доведення від протилежного.
Замість виводу $P \Rightarrow Q$, береться заперечення $Q$ ("нехай $Q$ невірно..."). Якщо в результаті логічних виводів з цих формул виходить суперечність $P,\,\neg{Q}~\Rightarrow~\F$ , то тоді $P \Rightarrow Q$. Дійсно, якщо $P \Rightarrow Q$, то область істинності $P$ є підмножиною $Q$ і не має спільної моделі з областю істинності $\neg Q$. Тому множина формул $\{P,\,\neg{Q}\}$ або формула $P\,\&\,\neg{Q}$ невиконувана, тобто суперечлива.

Для багатьох тверджень пряме доведення або невідоме, або довше доведення від протилежного (особливо при роздумах про існування або неіснування об'єктів з деякими властивостями).

◊ Класичний приклад - це доведення того, що $\sqrt{2}$ не подається у вигляді $n/m$, де $n,m\in \mathbb{N}^+=\{1,2,...\}$.
Як $P$ виступають аксіоми арифметики. Доведемо формулу $Q:~\sqrt{2}\neq n/m$, де $n/m$ нескоротний дріб.
Нехай $\bar{Q}: ~\sqrt{2}=n/m$. Підносячи до квадрата маємо $n^2=2\,m^2$ і отже $n$ - парне, тобто подається як $n=2\,k$.
Але тоді $(2k)^2 = 2m^2$ або $m^2 = 2k^2$, тобто $m$ - також парне, а це суперечить нескоротності дробу $n/m$.

У теорії предикатів доведення від протилежного дозволяє позбавлятися від кванторів і зводити логічний вивід до простої процедури, яку зазвичай використовують у програмах машинного доведення теорем.

Розглянемо спочатку формулу вигляду $S:~\exists_x\,P(x)$. Нехай необхідно довести, що вона невиконувана. Додамо в сигнатуру теорії нову константу $a$ і запишемо формулу $S':~P(a)$. Формули $S$ і $S'$ не еквівалентні і зокрема $\exists_x\,P(x)~\to~P(a)$ незагальнозначуща (її спростовувана інтерпретація: $x\in\{a,b\}$, $P(a)\equiv \F$, $P(b)\equiv \T$).
Це і зрозуміло. Формула $\exists_x\,P(x)$ не стверджує, що існуючий $x$ єдиний, тоді як у $P(a)$ існуюча константа введена в єдиному екземплярі.

Тим не менш, справедливе таке твердження "якщо $S'$ невиконувана, то невиконуваною буде і формула $S$."
Дійсно, нехай $P(a)$ невиконувана, а $\exists_x\,P(x)$ виконувана, тобто існує модель у якій $\exists_x\,P(x)$ істинно.
Це можливо, тільки якщо є такий $x$, що $P(x)$ істинно, що суперечить невиконуваності формули $P(a)$.

У загальному випадку усунення кванторів вимагає введення не тільки констант а й нових сколемівських функцій. Наприклад, формула $\forall_x\,\exists_y\,P(x,y)$ означає, що для кожного $x$ існує такий $y=f(x)$, що $P(x,f(y))$ істинно. Як і з константами, такий перехід не є логічним виводом. Однак, якщо $P(x,f(y))$ буде невиконувано, то невиконуваною буде і формула $\forall_x\,\exists_y\,P(x,y)$.

Введення сколемівських констант і функцій проводиться зліва-направо (стрілка $\mapsto$ це не імплікація, а перехід від формули $S$ до формули $S'$): $$ \exists_x\,\forall_{y,z}\,\exists_u\,\forall_v\,\exists_w\,P(x,y,z,u,v,w) ~~~~\mapsto~~~~ \forall_{y,z,v}\,\exists_w\,P(a,y,z,f(x,y),v,w) ~~~~\mapsto~~~~ \forall_{y,z,v}\,P(a,y,z,f(y,z),v,g(y,z,v)), $$ де для константи $a$ і функцій $f$, $g$ необхідно використовувати символи відмінні від тих, що задані в сигнатурі. При цьому в $\exists_{x,y}\,P(x,y)~~\mapsto~~P(a,b)$ константи повинні бути різними.

◊ Доведемо загальнозначущість такої формули: $\exists_x\,\forall_y\,R(x,y)~\to~\forall_y\,\exists_x\,R(x,y)$ від протилежного, взявши її заперечення: $\neg(A\to B)~~\Leftrightarrow~~ \neg(\neg A\vee B)~~\Leftrightarrow~~ A\,\&\,\neg B$ і ввівши сколемівські константи $a,b$: $$ \exists_x\,\forall_y\,R(x,y)~\,\&\,~\exists_y\,\forall_x\,\bar{R}(x,y) ~~~~\Leftrightarrow~~~~~ \exists_x\,\forall_y\,R(x,y),~~~~~\exists_y\,\forall_x\,\bar{R}(x,y) ~~~~~\mapsto~~~~~ \forall_y\,R(a,y),~~~~~\forall_x\bar{R}(x,b). $$ Оскільки ці дві формули повинні бути істинними при будь-яких $x,y$, можна покласти $y=b$ і $x=a$, отримавши суперечність: $R(a,b),~~\bar{R}(a,b)$.

Числення і вивідність

Вершиною формалізації математики є "Гра в слова". У цій грі фіксується алфавіт символів $\Sigma$ з яких формуються слова. Деяка підмножина $\mathcal{L}\subseteq \Sigma^{*}$ усіх можливих слів $\Sigma^{*}$ називається мовою (це "синтаксично правильні" слова). Частина слів мови $\mathcal{A} \subset \mathcal{L}$ оголошується аксіомами. Потім фіксуються правила виводу, які за деяким набором слів породжують нове слово з $\mathcal{L}$. Якщо з даної множини слів $\mathcal{P}\subset \mathcal{L}$ і аксіом $\mathcal{A}$, за допомогою правил виводу, породжується ланцюжок слів, який закінчується словом $Q$, то кажуть, що воно виводиме з множини слів: $\mathcal{P} \vdash Q$. Якщо для виводу $Q$ необхідні тільки аксіоми, то кажуть, що $Q$ просто виводиме: $\vdash Q$. Трійка {мова, аксіоми, правила виводу} називається численням.
Вивід $\vdash Q$ у численні є суто синтаксичною процедурою, що не використовує семантики теорії типу істинності або хибності формул (на відміну від семантики логічного виводу $\mathcal{P}\Rightarrow Q$).

◊ Нехай словник складається з двох символів $\Sigma=\{a,b\}$, а множина аксіом з чотирьох слів $\mathcal{A}=\{a,~b,~aa,~bb\}$ і є два правила виводу: $W~\vdash~ aWa$ і $W~\vdash~ bWb$, де $W$ - будь-яке виведене раніше слово. Це числення породжує всі двобуквені паліндроми типу $aba$, $abbba$, $bbaaabbaaabb$ і т.д.

Розв'язною називається теорія, для якої існує алгоритм, що дозволяє з'ясувати - виводима дана формула з аксіом чи ні. Якщо такого алгоритму немає, теорія називається нерозв'язною. Теорія з паліндромами з прикладу вище, очевидно, розв'язна.

У деяких теоріях можна перелічити всі її теореми. Такі теорії називаються напіврозв'язними. У них за скінченне число кроків можна підтвердити, що теорема виводима (знайти її в списку перелічення), але алгоритм ніколи не зупиниться для невивідних формул. На жаль, багато змістовних теорій нерозв'язні.

Важливу роль відіграє числення предикатів і його окремий випадок - числення висловлювань. Як слова в численні предикатів виступають формули, що складаються із символів $\Sigma=\{\neg~\,\&~\vee~\to~\leftrightarrow~\forall\,~\exists\,~A~f~x~c~(~~)~,\}$. Довільні предметні змінні $x$, $xx$, $xxx$ для стислості позначаються як $x,~y,~z$ і аналогічно для предикатних $A$, функціональних $f$ і константних символів $c$. Мова (синтаксично вірні формули) визначається за індукцією: "якщо $P$ і $Q$ формули, то $(P\vee Q)$ теж формула", і т.д.

На відміну від предметних теорій із заданою сигнатурою, аксіоми числення предикатів є "очевидно" загальнозначущими формулами (істинними на всіх інтерпретаціях). Правила виводу вибирають так, щоб загальнозначущість зберігалася. Тому загальнозначущими є і всі виводимі теореми числення. Наприклад формула $\exists_x\,\forall_y\,A(x,y)~\to~\forall_y\,\exists_x\,A(x,y)$ - це теорема числення, а $\forall_y\,\exists_x\,A(x,y)~\to~\exists_x\,\forall_y\,A(x,y)$ - вже ні (вона не загальнозначуща). Роль $A$ може відігравати будь-який предикат або формула конкретної предметної теорії. Теореми числення предикатів є підмножиною теорем будь-якої предметної теорії. Області істинності теорем числення - це весь простір інтерпретацій (на відміну від змістовних теорем предметної теорії). Так, $\forall_{x,y}[(x\lt y)\,\to\,\neg(y\lt x)]$ це теорема в предметній теорії (наприклад, в арифметиці), а $\forall_{x,y}[(x\lt y)\,\vee\,\neg(x\lt y)]$ це загальнозначуща теорема числення.

У принципі, в численні предикатів символи вивідності $\vdash$ і $\Rightarrow$ рівносильні. Коли пишуть більш загальний символ $\vdash$, прийнятий у довільних численнях, підкреслюють, що при виводі істинність формул ролі не грає, а просто йде "гра в слова". Але в будь-якому випадку, усі виводимі в численні предикатів формули загальнозначущі. Справедливе також зворотне твердження Геделя про повноту:

якщо формула $P$ загальнозначуща: $\vDash~P$, то вона виводима: $\vdash~P$.
У численні висловлювань твердження достатньо очевидне. Його теореми є тотожностями булевої алгебри. Приведення будь-якої формули за допомогою цієї алгебри до кон'юнктивної нормальної форми: $(P_1\vee P_2\vee...)\,\&\,(Q_1\vee Q_2\vee...)\,\&\,...$ дозволяє довести її істинність.

◊ Доведемо, що $P\to(\bar{P}\to Q)$ загальнозначуща. Переходячи від імплікації до диз'юнкції, маємо: $$ P\to(\bar{P}\to Q)~~~\Leftrightarrow~~~\bar{P}\vee (P\vee Q)~~~\Leftrightarrow~~~(\bar{P}\vee P)\vee Q~~~\Leftrightarrow~~~\T\vee Q ~~~\Leftrightarrow~~~\T. $$ Рухаючись у зворотному напрямку, з "аксіом" $\bar{P}\vee P$, $~~~\T\vee P$, правил $P~\Rightarrow~P\vee Q$, $P\vee Q~\Rightarrow~Q\vee P$ і т.п. можна вивести вихідну формулу.

Завжди становить інтерес формулювання незалежних аксіом і правил виводу. Для числення предикатів, наприклад, можна вибрати такі слова: $$ \begin{array}{lcl} P~\to~(Q\to P),\\ (P~\to~(Q\to R))~\to~((P\to Q)\to(P\to R)),\\ (\neg Q\to \neg P) ~\to~((\neg Q\to P)\to Q), \end{array} ~~~~~~~~~~~~~~~~~~~ \begin{array}{lcl} \forall_x\,A(x)~\to~A(t),\\ \forall_x\,(P\to Q(x))~\to~(P\to\forall_x\,Q(x))\\ ~\\ \end{array}, $$ де $P,Q,R$ - будь-які вже отримані раніше слова і в останній аксіомі в $P$ немає $x$. Такий нескінченний набір аксіом називається схемою аксіом. Як правила виводу достатньо взяти правило modus pones і правило узагальнення: $$ P,~~P\to Q~~~~~\vdash~~~~~Q,~~~~~~~~~~~~~~~~~~~~~~P(x)~~~\vdash~~~\forall_x\,P(x). $$ Ці аксіоми і правила дозволяють вивести всі рядки, які в семантичному трактуванні є загальнозначущими формулами числення предикатів.

Несуперечливість і незалежність аксіом

Назвемо теорією будь-яку скінченну або нескінченну множину $\mathcal{T}$ замкнутих, синтаксично правильних формул.
Вивід у теорії $\mathcal{T}$ формули $Q$ (з формул $\mathcal{T}$ і будь-яких загальнозначущих формул) позначимо як $\mathcal{T}\vdash Q$.
У загальному випадку $Q$ не загальнозначуща: $\not\vDash Q$, але, логічно випливає з теорії $\mathcal{T}\vDash Q$ (перетин областей істинності формул $\mathcal{T}$ є підмножиною області істинності $Q$). Частину формул $\mathcal{A}\subseteq \mathcal{T}$ можна назвати аксіомами. Аксіоми будь-якої, поважаючої себе предметної теорії, повинні бути несуперечливими, незалежними і, за можливості, повними.

✒ Теорія несуперечлива, якщо її аксіоми $A_1$, $A_2,...$ на множині інтерпретацій $\mathcal{I}$ перетинаються, тобто (існує хоча б одна інтерпретація $=$ модель на якій аксіоми одночасно істинні (праворуч точка $M$). У несуперечливій теорії $\mathcal{T}$, за допомогою виводу, не можна отримати деяке твердження $P$ і його заперечення $\bar{P}$. Дійсно, якщо з аксіом логічно випливає $P$, то область перетину аксіом (якщо вона є!) є його підмножиною і не може бути підмножиною $\bar{P}$, і навпаки (див. малюнок).

У суперечливій теорії $\mathcal{T}$ існує таке $P$, що $\mathcal{T} \vdash P$ і $\mathcal{T} \vdash \bar{P}$. У подібній теорії можна вивести будь-яке твердження, тому користі від неї небагато. Дійсно, з $P,\,\bar{P}$ і тавтології $P\to(\bar{P}\to Q)$ двічі за правилом modus ponens випливає $Q$ (довільна формула).

✒ Незалежність означає, що жодна аксіома не може бути виведена з інших аксіом.
Зокрема, множини істинності таких аксіом не включають повністю в себе інші аксіоми. Щоб довести незалежність аксіоми $A_1$ від аксіом $A_2,A_3,...$, необхідно побудувати таку інтерпретацію, у якій усі $A_2,A_3,...$ істинні, а $A_1$ - хибна. Це і означає, що область істинності $A_1$ не є підмножиною перетину областей істинності аксіом $A_2,A_3,...$.

Якщо дана теорія несуперечлива, а її аксіоми $A_1,...,A_n$ незалежні, то нова теорія, у якій одна з аксіом замінена на її заперечення, також є несуперечливою. Праворуч зафарбована область істинності перетину аксіом $A_2,...,A_n$. Межа істинності аксіоми $A_1$ ділить її на дві частини. У першій частині $(1)$ знаходяться моделі вихідної теорії, а в другій $(2)$ - моделі нової теорії, у якій $A_1\mapsto \bar{A}_1$.

Чим "більше" моделей у теорії, тим "слабша", зазвичай, система аксіом. Дійсно, при "великій" області перетину аксіом потенційно існує менше формул (теорем), для яких ця область є підмножиною і які в цій теорії можна вивести.

Повнота теорії

Предметна теорія $\mathcal{T}$ повна, якщо вона:

1) несуперечлива
2) будь-яка замкнута формула $P$ або виводима: $\mathcal{T}\vdash P$, або виводиме її заперечення: $\mathcal{T}\vdash \bar{P}$.
Повнота достатньо нетривіальна властивість формальної теорії і скоріше необхідно дивуватися існуванню повних теорій, ніж неповних.

На малюнку наведено приклад неповної теорії, у якій формули $P$ і $Q$ перетинають зафарбовану область перетину істинності аксіом (множина моделей теорії). Ці формули логічно не випливають з аксіом, і тому не можуть бути ні виведені, ні спростовані. Якщо їх додати до аксіом, то вийде теорія з меншим числом моделей (темно-сірий колір). Однак, якщо є нескінченна множина подібних формул, то і їхнє додавання до аксіом може не призводити до повної теорії (незаповнювана неповнота).

Конкретна неформальна предметна теорія зазвичай працює з визначеною множиною, на якій зафіксовані функції і предикати сигнатури (модель теорії). Наприклад, в арифметиці це нескінченна множина натуральних чисел $\mathbb{N}=\{\,0,\,1,\,2,\,...\,\}$. На ньому "звичайним чином" визначений предикат рівності $x=y$ і функції додавання $x+y$ і множення $x\cdot y$. Всі вони утворюють інтерпретацію $I_{\mathbb{N}}$, яка на малюнку вище позначена жирною точкою (знаходиться в області істинності аксіом арифметики). Цілком природно допустити існування таких формул, які істинні на $I_{\mathbb{N}}$, але при цьому невивідні (вище формула $P$).
У цьому полягає зміст теореми Геделя про неповноту арифметики з аксіомами Пеано (PA).

◈ Чудовим наслідком теореми про повноту числення предикатів (якщо $\vDash P$, то $\vdash P$) є еквівалентність логічного наслідку і вивідності в будь-якій теорії $\mathcal{T}$:

Якщо $~~~\mathcal{T}\vDash~P,~~~$ то $~~~\mathcal{T} \vdash~P~~~$ і навпаки.
Дійсно, нехай перетин областей істинності формул $\mathcal{T}$ це підмножина області істинності $P$.
Тоді за визначенням імплікації формула $\mathcal{T} \to P$ є тавтологією: $\mathcal{T}\vDash Q~~\Rightarrow~~\vDash \mathcal{T}\to Q~~$ (під $\mathcal{T}$ у формулі можна розуміти кон'юнкцію всіх формул $\mathcal{T}$). А раз так, то за теоремою про повноту числення вона виводима з загальнологічних аксіом (тавтологій): $\vdash \mathcal{T} \to P$. Відповідно, за правилом modus ponens отримуємо $\mathcal{T},~\mathcal{T} \to P ~\vdash~ P$ або (опускаючи, як зазвичай, загальнозначущу формулу) $\mathcal{T}\vdash P$. У зворотну сторону наслідок очевидний за побудовою правил виводу, які зберігають властивість логічного наслідку.

◊ Простим прикладом неповної теорії є теорія еквівалентності, сигнатура якої містить відношення $x\sim y$, що задовольняє аксіомам рефлексивності, симетричності і транзитивності: $$ \forall_x\,(x\sim x),~~~~~~~~~~~~~\forall_{x,y}\,\bigr[(x\sim y)~\to~(y\sim x)\bigr],~~~~~~~~~~~~\forall_{x,y,z}\,\bigr[(x\sim y)\,\&\,(y\sim z)~\to~(x\sim z)\bigr]. $$ У цій теорії невивідна формула $T:~\forall_{x,y}\,(x\sim y)$ так як вона хибна на будь-якій множині з двох і більше елементів, де $x\sim y$ це "звичайна" рівність (аксіоми на цих інтерпретаціях виконувані). У той же час її заперечення $\bar{T}:~\exists_{x,y}\,\neg(x\sim y)$ хибне на одноелементній множині $\mathbb{M}=\{a \}$ з $(a\sim a)\equiv \T$ (усі аксіоми при цьому також виконуються).

Відношення рівності $x=y$ задовольняє тим же аксіомам, що і відношення еквівалентності $x\sim y$. Крім цього додається нескінченний набір формул (схеми аксіом) що стверджують, що якщо збігаються аргументи у функцій або предикатів сигнатур, то повинні збігатися і їхні значення. Наприклад, якщо в сигнатурі є функція $f(x,y)$ і предикат $P(x)$, то додаються аксіоми: $$ \forall_{x_1,y_1,x_2,y_2}\,\bigr[(x_1=x_2)\,\&\,(y_1=y_2)~\to~f(x_1,y_1)=f(x_2,y_2)\bigr], ~~~~~~~ \forall_{x_1,x_2}\,\bigr[(x_1=x_2)~~\to~~ (P(x_1) \leftrightarrow P(x_2))\bigr]. $$ Теорія, у сигнатурі якої присутнє відношення рівності називається нормальною. У таких теоріях аксіоми рівності не повторюють, але передбачають їхню наявність.

◊ Найпростіший приклад повної теорії складається з "порожньої" сигнатури, у якій є тільки рівність $x=y$, аксіоми якої доповнені формулою $\forall_{x,y}\,(x=y)$. Єдиною моделлю цієї теорії є одноелементна множина $\{a\}$ з $a=a$ рівним $\T$. Будь-яка формула цю модель або включає (формула виводима), або ні (формула невивідна).

Аксіоматичний аналіз Аліси і Боба

Повернемося до теорії про Алісу і Боба і доведемо несуперечливість і незалежність її аксіом. У сигнатурі теорії є тільки твердження (константні предикати) $A,B,L$. Для доведення несуперечливості достатньо пред'явити приклад значень висловлювань, при яких усі аксіоми істинні. У нормальній формі ці аксіоми мають такий вигляд: $$ (\mathbf{A_1}):~~~~\bar{L}\vee \bar{A}\vee \bar{B},~~~~~~~~~~~~~~(\mathbf{A_2}):~~~~~L\vee A,~~~~~~~~~~~~~(\mathbf{A_3}):~~~~~L\vee B. $$ Неважко побачити, що для $A=B=\T $ і $L=\F $ вони істинні ($\T \vee Q \equiv \T $).

Щоб показати незалежність аксіом, необхідно побудувати інтерпретацію у якій усі аксіоми істинні, крім однієї. У цьому простому світі легко описати всю множину інтерпретацій у табличній формі. Кожен її елемент - це присвоєння логічним висловлюванням $A,B,L$ логічних значень $\T $ або $\F $:

Точки в таблицях позначають істину ($\T $). Їхня сукупність - це множина істинності формули. На решті інтерпретацій (хрестик) - формула хибна ($\F $). Перша аксіома хибна в єдиній моделі $A=B=L=\T $ (правий нижній кут першої таблиці з хрестиком). У цій же моделі друга і третя аксіоми істинні. Тому $A_1$ не можна вивести з $A_2$ і $A_3$. Аналогічно неважко знайти інтерпретації для доведення незалежності $A_2$ від $A_1,A_3$ і $A_3$ від $A_1,A_2$. Оскільки в нормальній формі висловлювання пов'язані диз'юнкціями, області істинності - це просто об'єднання областей істинності висловлювань (на другій таблиці пунктирами виділені істинності $L$ і $A$).

В останній таблиці наведена область істинності перетину всіх трьох аксіом кон'юнкцією, що відповідає семантиці нашої задачі. Зазначимо, що в історії про Алісу і Боба існує очевидний зв'язок $L \leftrightarrow \bar{A}\vee \bar{B}$, виконання якого і визначає множину істинності задачі. Щоб вивести цю формулу зліва направо $L\Rightarrow \bar{A}\vee \bar{B}$, необхідна перша аксіома, а для виводу в зворотному напрямку $\bar{A}\vee \bar{B} \Rightarrow L$, необхідні решта дві: $$ L,~\mathbf{A_1}~\Rightarrow~\bar{A}\vee\bar{B},~~~~~~~~~~~~~~~~~~~\bar{A}\vee\bar{B},~\mathbf{A_2},~\mathbf{A_3},~\Rightarrow~L. $$

Розглянемо як виглядає вивід твердження $\bar{B}$ з початку документа на мові множини інтерпретацій:

У першій таблиці наведена множина істинності вихідних посилок $L,A$, друга таблиця - це аксіома $\mathbf{A_1}$ і в третій - їхній перетин за допомогою логічного І. Ця область істинності (з однієї точки) є підмножиною області істинності твердження $\bar{B}$. Тому воно логічно випливає з посилок і аксіоми $\mathbf{A_1}$, що було продемонстровано побудовою відповідного виводу.

Теорія моделей

Нагадаємо, що теорія $\mathcal{T}$ - це будь-яка множина замкнутих формул. Теорія несуперечлива, якщо існує інтерпретація (модель $M$) у якій усі формули $\mathcal{T}$ істинні. Це позначається таким чином: $M\vDash \mathcal{T}$.

Елементарною теорією $\text{Th}(M)$ моделі $M$ називається множина всіх істинних у $M$ формул. У загальному випадку теорія $\mathcal{T}$ з моделлю $M\vDash \mathcal{T}$ може містити "менше" формул, ніж елементарна теорія: $\mathcal{T} \subseteq \text{Th}(M)$.

Всі формули, що випливають (і виводяться) з даної теорії $\mathcal{T}$ позначаються як $[\mathcal{T}]$. Наприклад, як $\mathcal{T}$ можна взяти аксіоми теорії. Тоді множина $[\mathcal{T}]$ містить як аксіоми, так і всі виводимі з них теореми.

◈ Для будь-якої моделі $M$ теорія $\text{Th}(M)$ повна.

$\triangleleft$ Дійсно, $\text{Th}(M)$ несуперечлива, оскільки в неї є модель. Будь-яка формула $P$ у моделі $M$ або істинна: $M\vDash P$ або хибна: $M\vDash \neg P$, звідки, або $P\in \text{Th}(M)$, або $\neg P\in \text{Th}(M)$. $\square$

◈ Якщо теорія $\mathcal{T}$ повна і $M$ її модель: $M\vDash \mathcal{T}$, то $[\mathcal{T}]=\text{Th}(M)$ і навпаки

$\triangleleft$ Від протилежного. Нехай $P\in \text{Th}(M)$ і $\mathcal{T}\not\vdash P$ (множини $[\mathcal{T}]$ і $\text{Th}(M)$ не збігаються). Тоді, в силу повноти, $\mathcal{T}\vdash \neg P$. Тому $M\vDash \neg P$ і $M\not \vDash P$, що суперечить $P\in \text{Th}(M)$. У зворотну сторону за попереднім твердженням. $\square$

Нехай предмети теорії належать одній множині. Інтерпретації $M$ і $N$ називають ізоморфними: $M\simeq N$, якщо між усіма елементами $m\in M$ і $n\in N$ є взаємооднозначна відповідність: $n=\alpha(m)$, $m=\alpha^{-1}(n)$ і для всіх констант $c_N=\alpha(c_M)$, всіх предикатів $A_M(m_1,m_2,...) \leftrightarrow A_N(\alpha(m_1),\alpha(m_2),...)$ і функцій $\alpha\bigr(f_M(m_1,m_2,...)\bigr)=f_N(\alpha(m_1),\alpha(m_2),...)$. Іншими словами, в ізоморфних інтерпретаціях всі елементи сигнатури визначені однаково з точністю до перепозначення елементів множин. Для скінченних множин число елементів у $M$ і $N$ повинні бути однаковими. Для нескінченних множин ситуація може бути хитрішою:

◊ Нехай є сигнатура з функцією $f(x,y)$ і константою $c$. Визначимо дві інтерпретації. Перша інтерпретація $M$ - це множина дійсних чисел $\mathbb{R}$, з функцією у вигляді звичайного додавання $f(x,y)=x+y$ і $c=0$. У другій $N$ - множина невід'ємних дійсних чисел $\mathbb{R}^+ \ge 0$ з функцією $f(x,y)=x\cdot y$ і константою $c=1$. Неважко побачити, що $M\simeq N$ з такою відповідністю: $n=e^{m}$.

Ізоморфізм $M\simeq N$ має властивості еквівалентності (рефлексивно, симетрично і транзитивно), і всі ізоморфні інтерпретації можна вважати "однаковими".

Моделі $M$ і $N$ називаються елементарно еквівалентними: $M\leftrightarrow N$, якщо $\text{Th}(M)=\text{Th}(N)$, тобто в них істинні одні й ті самі формули. Ізоморфні моделі елементарно еквівалентні: $M\simeq N~~\Rightarrow~~M\leftrightarrow N$, але не завжди навпаки.

◈ Якщо всі моделі теорії $\mathcal{T}$ елементарно еквівалентні, то $\mathcal{T}$ - повна теорія і навпаки.

$\triangleleft$ Від протилежного. Нехай $\mathcal{T}$ неповна. Тоді існує формула $P$ для якої $\mathcal{T}\vDash P$ і $\mathcal{T}\vDash \neg P$. Тоді обидві теорії ${\mathcal{T},~P}$ і ${\mathcal{T},~\neg P}$ виконувані, тобто мають не елементарно еквівалентні моделі (теорії різні).
Але тоді ці моделі будуть і моделями $\mathcal{T}$, що суперечить посилці. $\square$