Форма́льная тео́рия — это понятие, разработанное в рамках формальной логики в качестве основы для формализации теории доказательства.
Определение:
Формальная теория 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}}}
, как правило, конечно.