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

а) из множества формул (правильно построенных выражений) выделяется подмножество А, элементы которого называются аксиомами (аксиом может быть как конечное число, так и бесконечное); б) правила вывода (методы доказательства) теорем считаются известными из опыта изучения математики. При таком задании теорем дедуктивной теории говорим, что задана полуформальная аксиоматическая теория. III. Аксиом нет, а задается только конечное число правил выводов, с помощью которых и получают теоремы. Такую дедуктивную теорию называют теорией естественного вывода. Случай, когда нет аксиом и нет правил вывода, не рассматривается в логике. Применяя один из указанных способов задания теорем, будем получать множества теорем Ti, Т2^ Тз соответственно. Сразу возникают вопросы: когда эти множества Ti, Т2, и Тз совпадают? Когда некоторые ш Tj, или Т2, или Тз дедуктивной теории В совпадают или покрывают класс "истинных" формул теории Bj при условии совпадения для В я Вj, алфавитов и формул. Эти вопросы оказываются не всегда простыми и в рамках этого курса затрагиваются незначительно. § 3. Свойства дедуктивных теорий Выберем один из трех способов задания теорем дедуктивной теории. Изменяя аксиомы или правила вывода (в случае, когда они задаются), можно получать различные множества теорем Т. Это множество Т - множество теорем (множество доказуемых формул) является существенной характеристикой дедуктивной теории. Может оказаться, что множество теорем Т покрывает все множество формул (правильно построенных выражений) теории. Последнее означает, что доказуема любая формула и если в теории есть отрицание, то из доказуемости какой-то формулы тут же следует доказуемость ее отрицания. Следовательно, в этом случае доказуем какой-то факт и его отрицание. Ясно, что теории, в которых можно доказать что угодно, не представляют интерес. Дедуктивные теории, в которых множество теорем покрывает все множество формул, называются противоречивыми, в противном случае - непротиворечивыми. Выяснение непротиворечивости дедуктивной теории является одной из важнейших проблем. К сожалению, эта проблема оказывается и одной из очень сложных. Пусть множество теорем Т является частью, не совпадающей со всем множеством формул Ф (правильно построенных выражений), т.е. наша дедуктивная теория непротиворечива. Тогда можно уже интересоваться, а какую часть Ф занимают теоремы. Для этого вводят свойство полноты теории. Свойство полноты дедуктивной теории характеризует достаточность теорем 102