ВУЗ:
Составители:
2 Формальные аксиоматические теории
Формальная теория представляет собой множество чисто абстрактных объектов
(не связанных с внешним миром), в которой представлены правила оперирования множе-
ством символов в чисто синтаксической трактовке без учета смыслового содержания (или
семантики).
Исторически понятие формальной теории было разработано в период интенсивных
исследований в области оснований математики для формализации собственно логики и
теории доказательства. Сейчас этот аппарат широко используется при создании специаль-
ных исчислений для решения конкретных прикладных задач. Одним из таких приложений
является логическое программирование.
Формальную теорию иногда называют аксиоматикой или формальной
аксиоматической теорией. Родоначальником аксиоматических теорией можно считать
«Начала» Евклида.
2.1 Определение формальной теории
Формальная теория T считается определенной, если:
• задано некоторое счетное множество A символов − символов теории T; конечные по-
следовательности символов теории T называются выражениями теории T (множество
выражений обозначают через A*);
• имеется подмножество F ⊂ A* выражений теории T, называемых формулами теории T;
• выделено некоторое множество B ⊂ F формул, называемых аксиомами теории T;
• имеется конечное множество {R
1
, R
2
, …, R
m
} отношений между формулами, называе-
мых правилами вывода. Правила вывода позволяют получать из некоторого конечного
множества формул другое множество формул.
Множество символов A − алфавит теории − может быть конечным или бесконеч-
ным. Обычно для образования символов используют конечное множество букв, к кото-
рым, если нужно, приписывают в качестве индексов натуральные числа.
Множество формул F обычно задается индуктивным определением, например, с
помощью формальной грамматики. Как правило, это множество бесконечно. Множества
A и F в совокупности определяют язык формальной теории.
Множество аксиом B может быть конечным или бесконечным. Если множество ак-
сиом бесконечно, то, как правило, оно задается с помощью конечного множества схем ак-
сиом и правил порождения конкретных аксиом из схемы аксиом. Обычно аксиомы делят-
ся на два вида: логические аксиомы (общие для целого класса формальных теорий) и
нелогические (или собственные) аксиомы (определяющие специфику и содержание кон-
кретной теории).
Обычно для формальной теории имеется алгоритм, позволяющий по данному вы-
ражению определить, является ли оно формулой. Точно также, чаще всего существует ал-
горитм, выясняющий, является ли данная формула теории T аксиомой; в таком случае T
называется эффективно аксиоматизированной теорией.
2.2 Выводимость
Пусть A
1
, A
2
,…, A
n
, A − формулы теории T. Если существует такое правило вывода
R, что < A
1
, A
2
,…, A
n
, A> ∈ R, то говорят, что формула A непосредственно выводима из
формул A
1
, A
2
,…, A
n
по правилу вывода R. Обычно этот факт записывают следующим об-
разом:
8
Страницы
- « первая
- ‹ предыдущая
- …
- 6
- 7
- 8
- 9
- 10
- …
- следующая ›
- последняя »
