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

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

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

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

1. множество A{displaystyle {mathcal {A}}} символов, образующих алфавит;

2. множество F{displaystyle {mathcal {F}}} слов в алфавите A,F⊂A{displaystyle {mathcal {A}},{mathcal {F}}subset {mathcal {A}}}, которые называются формулами;

3. подмножество B{displaystyle {mathcal {B}}} формул, F⊂A{displaystyle {mathcal {F}}subset {mathcal {A}}}, которые называются аксиомами;

4. множество R{displaystyle {mathcal {R}}} отношений R{displaystyle R,!} на множестве формул, R∈R,R⊂Fn+1{displaystyle Rin {mathcal {R}},Rsubset {mathcal {F}}^{n+1}}, которые называются правилами вывода.

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

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

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

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