Математическая логика и теория алгоритмов

Может оказаться, что множество теорем Т покрывает все мно­ жество формул (правильно построенных выражений) теории. Иначе, это означает, что доказуема любая формула (правильно построенное выражение) и если в теории есть отрицание, то из доказуемости какой-то формулы тут же следует доказуемость ее отрицания. Следо­ вательно, в этом случае доказуем какой-то факт и его отрицание. Ясно, что теории, в которых можно доказать что угодно, не пред­ ставляют интерес. Дедуктивные теории, в которых множество теорем покрывает все множество формул (правильно построенных выражений), называ­ ются противоречивыми, в противном случае - непротиворечивыми. Выяснение непротиворечивости дедуктивной теории является одной из важнейших проблем. К сожалению, эта проблема оказывается и одной из очень сложных. Пусть множество теорем Т является частью, не совпадающей со всем множеством формул Ф (правильно построенных выражений), т.е. наша дедуктивная теория непротиворечива. Тогда можно уже интересоваться, а какую часть Ф занимают теоремы. Для этого вводят свойство полноты теории. Свойство полноты дедуктивной теории характеризует достаточность теорем для каких-то целей. В зависимо­ сти от того, для каких целей должно быть достаточно теорем, будем в дальнейшем вводить различные понятия полрюты. Рассмотренные свойства - непротиворечивость и полнота, яв­ ляются важнейшими свойствами дедуктивной теории. Кроме этих свойств, имеется и ряд других свойств. Рассмотрим еще два свойства дедуктивной теории. Независимость аксиом теории. Отдельная аксиома дедуктивной теории называется независимой, если эту аксиому нельзя вывести в этой теории из остальных аксиом. Система аксиом называется неза­ висимой, если каждую из них нельзя вывести из остальных. Разрешимость теории. Дедуктивная теория называется разре­ шимой, если в этой теории понятие теоремы эффективно, т.е. сущест­ вует правило (метод), позволяющее для произвольной формулы за ко­ нечное число действий выяснить, является она теоремой или нет. 140

RkJQdWJsaXNoZXIy MTY0OTYy