Глава 02. Формальные теории

Определение формальной теории

Формальная теория T — это:

1. множество А символов, образующих Алфавит;

2. множество F слов в алфавите А, которые называются Формулами;

3. множество B формул в F, которые называются Аксиомами;

4. множество R отношений R На множестве формул, которые называются Правилами вывода.

Множество символов А Может быть конечным или бесконечным. Обычно для образования символов используют конечное множество букв, к которым, если нужно, приписываются в качестве индексов натуральные числа.

Множество формул F обычно задается индуктивным определением, например, с помощью формальной грамматики. Как правило, это множество бесконечно. Множества А и F В совокупности определяют Язык, Или Сигнатуру, Формальной теории.

Множество аксиом B может быть конечным или бесконечным. Если множество аксиом бесконечно, то, как правило, оно задается с помощью конечного множе­ства Схем Аксиом и правил порождения конкретных аксиом из схемы аксиом. Обычно аксиомы делятся на два вида: Логические Аксиомы (общие для целого класса формальных теорий) и Нелогические (или Собственные) Аксиомы (опреде­ляющие специфику и содержание конкретной теории). Множество правил вывода R, Как правило, конечно.

Выводимость

Пусть F1, ..., Fn, G — Формулы теории T, То есть F1, ..., Fn. Если существует такое правило вывода R Из R, то говорят, что формула G непосредственно выводима Из формул F1,..., Fn По правилу выво­да R. Обычно этот факт записывают следующим образом:

Где формулы F1,...,Fn Называются Посылками, А формула G — Заключением.

Если в теории T существует вывод формулы G Из формул F1, ..., Fn, То это записывают следующим образом:

F1, ..., Fn T G,

Где формулы F1,...,Fn Называются Гипотезами Вывода. Если теория T подразу­мевается, то ее обозначение обычно опускают.

< Предыдущая		Следующая >