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

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

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

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

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

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

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