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

Форма́льная тео́рия — это понятие, разработанное в рамках формальной логики в качестве основы для формализации теории доказательства.

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

Формальная теория \mathcal{T} — это:

  1. множество \mathcal{A} символов, образующих алфавит;
  2. множество \mathcal{F} слов в алфавите \mathcal{A}, \mathcal{F}\sub \mathcal{A}, которые называются формулами;
  3. подмножество \mathcal{B} формул, \mathcal{F}\sub \mathcal{A}, которые называются аксиомами;
  4. множество \mathcal{R} отношений R\,\! на множестве формул, R \in \mathcal{R}, R \sub \mathcal{F}^{n+1}, которые называются правилами вывода.

Множество символов \mathcal{A} может быть конечным или бесконечным. Обычно для образования символов используют конечное множество букв, к которым при необходимости, приписываются в качестве индексов целые числа или выражения.

Множество формул \mathcal{F} обычно задаётся индуктивным определением, например, с помощью формальной грамматики. Как правило, это множество бесконечно. Множества \mathcal{A} и \mathcal{F} в совокупности определяют язык или сигнатуру формальной теории.

Множество аксиом \mathcal{B} может быть конечным или бесконечным. Если множество аксиом бесконечно, то, как правило, оно задаётся с помощью конечного числа схем аксиом и правил порождения конкретных аксиом из схемы аксиом. Обычно аксиомы делятся на два вида: логические аксиомы (общие для целого класса формальных теорий) и нелогические или собственные аксиомы (определяющие специфику и содержание конкретной теории).

Множество правил вывода \mathcal{R}, как правило, конечно.

 
Начальная страница  » 
А Б В Г Д Е Ж З И Й К Л М Н О П Р С Т У Ф Х Ц Ч Ш Щ Ы Э Ю Я
A B C D E F G H I J K L M N O P Q R S T U V W X Y Z
0 1 2 3 4 5 6 7 8 9 Home