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

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

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

Определение

Формальная теория считается определенной, если:

1. Задано счетное множество произвольных символов. Конечные последовательности символов называются выражениями теории.
2. Имеется подмножество выражений, называемых формулами.
3. Выделено подмножество формул, называемых аксиомами.
4. Имеется конечное множество отношений между формулами, называемых правилами вывода. Для каждого правила вывода R и для каждой формулы A эффективно решается вопрос о том, находится ли выбранный набор формул в отношенни R с формулой A, и если да, то A называется непосредственным следствием данных формул по правилу R.

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

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

См. также

• Дедуктивная теория
• Логика высказываний
• Логика первого порядка

Литература

• Ф. А. Новиков. Дискретная математика для программистов. — СПб.: Питер, 2000. — 304 с.: ил. ISBN 5-272-00183-4.ru:Формальные системы