Теория алгоритмов. Зюзысов В.М. - 24 стр.

UptoLike

ВУЗ: 

ТГУ | Томск

Составители: 

Рубрика: 

...эмпирические системы утрачивают свою
актуальность, математические же – никогда.
Их бессмертие – в их «пустоте».
Станислав Лем,
Сумма технологии
3 Формальные аксиоматические теории
Формальная теория представляет собой множество чисто абстрактных объектов
(не связанных с внешним миром), в которой представлены правила оперирования
множеством символов в чисто синтаксической трактовке без учета смыслового
содержания (или семантики).
Исторически понятие формальной теории было разработано в период интенсивных
исследований в области оснований математики для формализации собственно логики и
теории
доказательства. Сейчас этот аппарат широко используется при создании
специальных исчислений для решения конкретных прикладных задач. Одним из таких
приложений является логическое программирование.
Формальную теорию иногда называют аксиоматикой или формальной
аксиоматической теорией. Родоначальником аксиоматических теорией можно считать
«Начала» Евклида.
3.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
называется эффективно аксиоматизированной теорией.

Страницы