СВ: Новая страница: «{{Определение |definition= Формальная теория {{---}} это совокупность четырех объектов: * Алфавит...»

2026-10-25T11:43:06Z

Новая страница: «{{Определение |definition= Формальная теория {{---}} это совокупность четырех объектов: * Алфавит...»

Новая страница

{{Определение
|definition=
Формальная теория {{---}} это совокупность четырех объектов:

* Алфавит $\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>
R \subseteq \underbrace{
\mathfrak F\times\mathfrak F\times \cdots \times\mathfrak F}_{k+1}.
</math>

}}
{{Определение
|definition=
Пусть $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$.
}}
{{Определение
|definition=
Вывод {{---}} это последовательность формул $\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$, по некоторому правилу вывода данной формальной теории.
}}
{{Определение
|definition=
Говорят, что формула $\mathcal A$ формальной теории $T$ является теоремой
(выводима в формальной теории $T$), если для нее существует вывод $\mathcal A_1$, $\mathcal A_2$, ...,$\mathcal A_n=\mathcal A$.

Пишут $\vdash_T \mathcal A$.
}}
{{Определение
|definition=
Аксиоматическая теория {{---}} формальная теория, в которой существует алгоритм, позволяющий для любой формулы $\mathcal A$ определить, является ли $\mathcal A$ аксиомой.
}}
{{Определение
|definition=
Разрешимая теория {{---}} формальная теория, в которой существует алгоритм, позволяющий для любой формулы $\mathcal A$ определить, является ли $\mathcal A$ теоремой.

Неразрешимая теория {{---}} теория не являющаяся разрешимой.
}}
{{Определение
|definition=
Пусть $\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$.
}}

{{Пример
|content=Формальная теория $M$:

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

2) Формулы {{---}} последовательности из символа | произвольной длины:

$\mathfrak F = \mathfrak A^*$

3) Аксиома: <math>\mathfrak B = \{||\}</math>.

4) Правило вывода: <math>R=\{(\alpha,\beta) | \alpha - \textrm{ формула}, \beta=\alpha\alpha\}</math>.

Вывод:

1. <math>||</math> {{---}} аксиома.

2. <math>||||</math> {{---}} из строки 1 по правилу вывода $R$.

3. <math>||||||||</math> {{---}} из строки 2 по правилу вывода $R$.

Таким образом, теоремами этой формальной теории являются последовательности из символа $|$ длины $2^t$ для любого $t\in\mathbb{N}$.

Формальная теория $M$ является аксиоматической и разрешимой.
}}

[[Файл:p47-01-theory-structure.svg|frame|none|900px|alt=Вложенные алфавит, формулы и аксиомы, правила вывода и пример вывода в теории M|Рис. 1. Четыре части теории вложены друг в друга: <math>B \subseteq F \subseteq A^*</math>, а правила <math>R</math> порождают новые формулы из старых. Справа — вывод в теории <math>M</math>: из аксиомы <math>||</math> правилом <math>\alpha \mapsto \alpha\alpha</math> получаются строки длины <math>2, 4, 8, \ldots</math>]]

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

Формальные теории - История изменений

СВ: Новая страница: «{{Определение |definition= Формальная теория {{---}} это совокупность четырех объектов: * Алфавит...»