Дедуктивная теория

В математической теории огромное значение имеет дедуктивная теория. Термин дедукция происхоидт от лат. deductio — выведение. Таким образом, дедукция — это один из основных способов рассуждения и методов исследования.

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

• Задан алфавит, то есть множество, и правила образования выражений в этом алфавите.
• Заданы правила образования формул.
• Выделено подмножество теорем, которые доказывают формулу.

Существует несколько способов построения множества теорем:

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

Этот способ позволяет задавать формальные аксиоматические теории.

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

Данный способ построения теорем основывается на задании только правил вывода, поскольку множество аксиом пусто. Исходя из этого, теория, заданная таким образом, являет собой частный случай формальной теории. Позднее эта разновидность стала называться теорией естественного вывода.

Противоречивой называется теория, в которой множество теорем покрывает всё множество формул. В ином случае, теория является непротиворечивой. Главной и сложнейшей задачей формальной логики является ыыявление противоречивости теории. Противоречивые теории, как правило, не имеют дальнейшего практического и теоретического применения.

Полной называется теория, в которой для любой формулы F выводима либо сама F, либо ее отрицание -F. В том случае, если теория содержит недоказуемые утверждения, то есть утверждения, которые нельзя ни доказать, ни опровергнуть средствами самой теории, она называется неполной.

Когда отдельную аксиому теории нельзя вывести из остальных аксиом, то ее называют независимой. Зависимая аксиома является избыточна, поэтому ее извлечение из системы аксиом не отражается на теории. Система аксиом называется независимой только в том случае, если каждая аксиома в ней независима.

Когда в теории существует эффективный алгоритм, позволяющий определить количество шагов, доказывающих теорему, теория называется разрешимой.

К примеру, логика высказываний, логика первого порядка (исчисление предикатов), формальная арифметика (теория S).