Математическая логика и теория алгоритмов. Для изучающих компьютерные науки

эффективно, т.е. существует правило (метод), позволяющее для произвольной формулы за конечное число действий выяснить, является она теоремой или нет. Теорема 4.7. Исчисление высказываний (теория L) является разрешимой теорией. Доказательство. Было доказано, что каждая теорема теории L является тавтологией и (обратно) каждая формула, являющаяся тавтологией, есть теорема. Таким образом, формула^ теории L является теоремой тогда и только тогда, когда она является тавтологией. Следовательно, для того, чтобы выяснить, А теорема или нет, достаточно выяснить, А тавтология или нет. Последнее легко определить, например, с помощью таблиц истинности или приведением к к.н.ф. В результате имеем требуемое правило, позволяющее для каждой формулы А за конечное число шагов выяснить: А теорема или нет. Итак, исчисление высказываний является непротиворечивой, полной в широком и узком смыслах, разрешимой и эффективно аксиоматизированной формальной теорией с независимой системой аксиом. § 12. Другие аксиоматизации исчисления высказываний В предыдущих параграфах рассматривался пример формальной аксиоматической теории - исчисление высказываний (теория L), которая была задана множеством символов, формул, аксиом и правил вывода. Теперь рассмотрим некоторую формализованную теорию С. Для задания формализованной теории необходимо задать ее символы, формулы (правильно построенные выражения) и из множества формул выделить подмножество, элементы которого считаются «истинными» формулами. Пусть формализованная теория С задана так, что 1) алфавиты теорий L и С совпадают, т.е. алфавитом для С является следующее множество символов; —i, ), {,Ai,A2,...; 2) множества формул L и С совпадают {0^=0 с , где Фь(Фс ) - множество формул теории L{C)). Таким образом, формулой в С является всякая пропозициональная форма, построенная из букв^7, А2,... с помощью связок —i и 3) "истинными" формулами в теории С считаются те и только те формулы теории С, которые являются тавтологиями. Пусть Ус обозначает множество "истинных" формул теории С. В исчислении высказываний было задано Ti - множество теорем (с помощью аксиом А1-АЗ и правила вывода MP). При этом теоремами в L оказались те и только те формулы из L, которые являются тавтологиями. Следовательно, множество теорем формальной теории L совпадает с множеством "истинных" формул формализованной теории С\ Ti =Vc . 121