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

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

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

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

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

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

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

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

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