Формальные теории

Определение:

Формальная теория — это совокупность четырех объектов:

• Алфавит $\mathfrak A$ — произвольное множество элементов, которые, в этом случае, называют символами.
• Множество формул $\mathfrak F$ — некоторое множество слов в алфавите $\mathfrak A$:

$\mathfrak F\subseteq \mathfrak A^* = \bigcup_{i=1}^{\infty} \mathfrak A^i.$

• Множество аксиом $\mathfrak B$ — некоторое множество формул: $\mathfrak B\subseteq \mathfrak F.$
• Множество правил вывода $\mathfrak R$ — множество отношений $R$ на множестве формул:

[math]\displaystyle{ R \subseteq \underbrace{ \mathfrak F\times\mathfrak F\times \cdots \times\mathfrak F}_{k+1}. }[/math]

Определение:

Пусть $R\in \mathfrak R$ — некоторое \mbox{$k+1$}-арное правило вывода.

Если $\mathcal A_1$, $\mathcal A_2$, ..., $\mathcal A_k$, $\mathcal A_{k+1}$ — формулы из $\mathfrak F$ и $(\mathcal A_1, \mathcal A_2, ..., \mathcal A_k, \mathcal A_{k+1})\in R$, то говорят, что $\mathcal A_{k+1}$ непосредственно выводима из $\mathcal A_1$, $\mathcal A_2$, ..., $\mathcal A_k$

(или $\mathcal A_{k+1}$ непосредственное следствие $\mathcal A_1$, $\mathcal A_2$, ..., $\mathcal A_k$) по правилу вывода $R$.

Определение:

Вывод — это последовательность формул $\mathcal A_1$, $\mathcal A_2$, ..., $\mathcal A_n$, такая что для каждого $i\in\{1,...,n\}$ верно одно из двух:

a) $\mathcal A_i \in \mathfrak B$ — аксиома, или

b) $\mathcal A_i$ непосредственно выводима из формул $\mathcal A_{j_1}$, $\mathcal A_{j_2}$, ..., $\mathcal A_{j_k}$,

$1\leq j_s \lt i$, по некоторому правилу вывода данной формальной теории.

Определение:

Говорят, что формула $\mathcal A$ формальной теории $T$ является теоремой

(выводима в формальной теории $T$), если для нее существует вывод $\mathcal A_1$, $\mathcal A_2$, ...,$\mathcal A_n=\mathcal A$.

Пишут $\vdash_T \mathcal A$.

Определение:

Аксиоматическая теория — формальная теория, в которой существует алгоритм, позволяющий для любой формулы $\mathcal A$ определить, является ли $\mathcal A$ аксиомой.

Определение:

Разрешимая теория — формальная теория, в которой существует алгоритм, позволяющий для любой формулы $\mathcal A$ определить, является ли $\mathcal A$ теоремой. Неразрешимая теория — теория не являющаяся разрешимой.

Определение:

Пусть $\Gamma\subseteq \mathfrak F$ — некоторое множество формул теории $T$.

Формула $\mathcal A$ выводима в формальной теории $T$ из множества посылок $\Gamma$ ($\mathcal A$ — следствие формул множества $\Gamma$), если для нее существует последовательность формул $\mathcal A_1$, $\mathcal A_2$, ..., $\mathcal A_n=\mathcal A$, такая что для каждого $i\in\{1,...,n\}$ верно одно из трех:

• a) $\mathcal A_i \in \mathfrak B$ — аксиома,
• b) $\mathcal A_i\in\Gamma$ — посылка, или
• c) $\mathcal A_i$ непосредственно выводима из формул $\mathcal A_{j_1}$, $\mathcal A_{j_2}$, ..., $\mathcal A_{j_k}$,

$1\leq j_s \lt i$, по некоторому правилу вывода теории $T$.

Такую последовательность формул будем называть выводом из посылок $\Gamma$.

Пишут $\Gamma \vdash_T \mathcal A$.

Пример

Формальная теория $M$:

1) Алфавит: [math]\displaystyle{ \mathfrak A = \{|\} }[/math].

2) Формулы — последовательности из символа

Рис. 1. Четыре части теории вложены друг в друга: [math]\displaystyle{ B \subseteq F \subseteq A^* }[/math], а правила [math]\displaystyle{ R }[/math] порождают новые формулы из старых. Справа — вывод в теории [math]\displaystyle{ M }[/math]: из аксиомы [math]\displaystyle{ || }[/math] правилом [math]\displaystyle{ \alpha \mapsto \alpha\alpha }[/math] получаются строки длины [math]\displaystyle{ 2, 4, 8, \ldots }[/math]

Конспект: Дискретная математика