Полнота, независимость и разрешимость

Пусть множество M является моделью формальной теории Т. Формальная теория Т называется полной (или адекватной), если каждому истинному высказыванию M соответствует теорема теории Т.

Если для множества (алгебраической системы) M существует формальная полная непротиворечивая теория Т, то M называется аксиоматизируемым (или формализуемым) множеством.

Система аксиом (или аксиоматизация) формально непротиворечивой теории Т называется независимой, если никакая из аксиом не выводима из остальных по правилам вывода теории Т.

Еще одна важная характеристика формальной теории – это ее разрешимость. Формальная теория Т называется разрешимой, если существует алгоритм, который для любой формулы языка определяет, является она теоремой в Т или нет.

Например, исчисление высказываний разрешимо, а исчисление предикатов неразрешимо. Разрешающий алгоритм для формулы F Исчисления высказываний заключается в вычислении значений F на всех наборах значений ее переменных. Ввиду полноты исчисления высказываний F является его теоремой, если и только если она истинна на всех наборах.

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

4. Метатеория формальных систем.

При изучении формальных теорий мы имеем дело с дву­мя типами высказываний. Во-первых, с высказываниями самой теории (теоремами), которые рассматриваются как чисто формальные объекты, определенные ранее, а во-вто­рых, с высказываниями о теории (о свойствах ее теорем, доказательств и т.д.), которые формулируются на языке, внешнем по отношению к теории, - метаязыке и называ­ются метатеоремами. Различие между теоремами и метатеоремами не всегда будет проводиться явно, но его обяза­тельно надо иметь в виду.

Интерпретацией формальной теории Т в область интерпретации M называется функция I : Á ® M, которая каждой формуле формальной теории Т однозначно сопоставляет некоторое содержательное высказывание относительно объектов множества (алгебраической системы) M. Это высказывание может быть истинным или ложным (или не иметь истинностного значения). Если соответствующее высказывание является истинным, то говорят, что формула выполняется в М.

Интерпретация I называется моделью множества формул G, если все формулы этого множества выполняются в интерпретации I. Интерпретация I называется моделью формальной теории Т, если все теоремы этой теории выполняются в интерпретации I (то есть все выводимые формулы оказываются истинными в данной интерпретации).

Непротиворечивость. Напомним, что формула называется противоречивой, если она ложна в любой интерпретации. Такое определение противоречивой формулы является семантическим, т.е. связывающим непротиворечивость с истинностью. Исходя из него, можно сформулировать понятие семантически непротиворечивой теории:

Формальная теория Т называется семантически непротиворечивой, если ни одна ее теорема не является противоречием. Таким образом, формальная теория пригодна для описания тех множеств (алгебраических систем), которые являются ее моделями. Модель для формальной теории Т существует тогда и только тогда, когда Т семантически непротиворечива.

Формальная теория Т называется формально непротиворечивой, если в ней не являются выводимыми одновременно формулы F и ØF. Теория Т формально непротиворечива тогда и только тогда, когда она семантически непротиворечива.

С помощью введенных понятий можно сформулировать следующий тезис, что теория Т пригодна для описания тех множеств, которые являются ее моделями. Модель для теории Т существует тогда и только тогда, когда Т семантически непротиворечива. Чисто логические теории – исчисление высказываний и исчисление предикатов пригодны для описания любых множеств, что соответствует общенаучному принципу универсальности законов логики. Лейбниц формулировал его как выполнимость логических законов во всех «мыслимых мирах». Аналогом этого критерия, сформулированным в терминах самих формальных теорий без привлечения семантических понятий, является формальная или дедуктивная непротиворечивость.