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