Интернет магазин китайских планшетных компьютеров

Компьютеры - Формальная система - Определение и разновидности

Дедуктивная теория считается заданной, если:

1. Задан алфавит и правила образования выражений в этом алфавите.
2. Заданы правила образования формул.
3. Из множества формул некоторым способом выделено подмножество T теорем.

Разновидности дедуктивных теорий

В зависимости от способа построения множества теорем:

Задание аксиом и правил вывода

В множестве формул выделяется подмножество аксиом, и задается конечное число правил вывода — таких правил, с помощью которых из аксиом и ранее выведенных теорем можно образовать новые теоремы. Все аксиомы также входят в число теорем. Иногда теория содержит бесконечное количество аксиом, задающихся при помощи одной или нескольких схем аксиом. Аксиомы иногда называют «скрытыми определениями». Таким способом задается формальная теория исчисление).

Задание только аксиом

Задаются только аксиомы, правила вывода считаются общеизвестными.

При таком задании теорем говорят, что задана полуформальная аксиоматическая теория.

Примеры

Геометрия

Задание только правил вывода

Аксиом нет, задаются только правила вывода.

По сути, заданная таким образом теория — частный случай формальной, но имеет собственное название: теория естественного вывода.