Теория алгоритмов. Зюзысов В.М. - 37 стр.

UptoLike

Составители:

Рубрика:

вывода P из Γ, хотя бы и неполного. В этом случае мы «не доказываем P, а доказываем,

что существует доказательство P» [16, с. 45].

Результат «не Γ|–P» в редких случаях может устанавливаться чисто

синтаксическим рассуждением, но обычно доказательство опирается на конструкцию

модели, т.е. интерпретации, в которой Γ истинно, а P

ложно.

Непротиворечивость, полнота и неразрешимость исчисления

предикатов

Теорема 16. Исчисление предикатов первого порядка непротиворечиво.

Теорема 17. (о полноте исчисления предикатов). В исчислении предикатов первого

порядка теоремами являются те и только те формулы, которые общезначимы.

Доказательство. В силу теоремы 15 достаточно доказать только, что любая

теорема исчисления предикатов первого порядка является общезначимой формулой. Но

это следует из общезначимости аксиом исчисления предикатов

и синтаксических свойств

истинности в теориях первого порядка.

Теорема 18. (Теорема Чёрча о неразрешимости исчисления предикатов, 1936). Не

существует алгоритма, который для любой формулы исчисления предикатов первого

порядка устанавливает, общезначима она или нет.

Теорема Чёрча остается в силе и для любой теории первого порядка, содержащей

все формулы исчисления предикатов первого порядка.

Теорема

17 показывает, что в логике предикатов синтаксический метод теорий

первого порядка равносилен семантическому методу, использующему понятие

интерпретации, модели, общезначимости и т. п. Для исчисления высказываний имеет

место аналогичная эквивалентность семантических (тавтология и др.) и синтаксических

(теорема и др.) понятий. Отметим также, что для исчисления высказываний теорема о

полноте системы приводит к

решению проблемы разрешения. Однако для теорий первого

порядка мы не можем получить разрешающий алгоритм для общезначимости или, то же

самое, для выводимости в любом исчислении предикатов первого порядка.