- Формальное исчисление
-
Форма́льная (аксиоматическая) тео́рия, формальное исчисление — это понятие, разработанное в рамках формальной логики в качестве основы для формализации теории доказательства. Формальная теория — разновидность дедуктивной теории, где множество теорем выделяется из множества формул путем задания множества аксиом и правил вывода.
Определение
Формальная теория — это:
- конечное множество символов, образующих алфавит;
- конечное множество слов в алфавите , которые называются формулами;
- подмножество формул, , которые называются аксиомами;
- множество отношений на множестве формул, , которые называются правилами вывода.
Множество символов может быть конечным или бесконечным. Обычно для образования символов используют конечное множество букв, к которым при необходимости приписываются в качестве индексов целые числа или выражения.
Множество формул обычно задаётся индуктивным определением, например, с помощью формальной грамматики. Как правило, это множество бесконечно. Множества и в совокупности определяют язык или сигнатуру формальной теории.
Множество аксиом может быть конечным или бесконечным. Если множество аксиом бесконечно, то, как правило, оно задаётся с помощью конечного числа схем аксиом и правил порождения конкретных аксиом из схемы аксиом. Обычно аксиомы делятся на два вида: логические аксиомы (общие для целого класса формальных теорий) и нелогические или собственные аксиомы (определяющие специфику и содержание конкретной теории).
Множество правил вывода , как правило, конечно.
См. также
Литература
- Ф. А. Новиков. Дискретная математика для программистов. — СПб.: Питер, 2000. — 304 с.: ил. ISBN 5-272-00183-4.
Wikimedia Foundation. 2010.