Математическое введение в декларативное программирование. Зюзысов В.М. - 26 стр.

UptoLike

ВУЗ: 

ТГУ | Томск

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

Рубрика: 

∃x(A(x)&C) = ∃xA(x)&C, ∃x(A(x)∨C) = ∃xA(x)∨C;
C⊃∀xA(x) = ∀x(C⊃A(x)), C⊃∃xA(x) = ∃x(C⊃A(x));
∀xA(x)⊃C ⇒ ∃x(A(x)⊃C).
Имеет место следующее утверждение:
Если теория первого порядка (формально) противоречива, то в ней выводима лю-
бая формула.
Доказательство. В самом деле, пусть формулы A и ¬A выводимы в теории. Форму-
ла ¬A⊃(A⊃B) является тавтологией в исчислении высказываний, следовательно, она вы-
водима. Её вывод, поскольку он содержит только MP, остается выводом и в любой теории
первого порядка. Поэтому формула ¬A⊃(A⊃B) выводима в теории первого порядка. Два-
жды применяя MP, мы получаем вывод произвольной формулы B.
Таким образом, для доказательства непротиворечивости какой-либо теории перво-
го порядка достаточно установить невыводимость в этой теории хотя бы одной формулы.
Теорема 3. (Гёдель, 1930). Всякая общезначимая формула теории T первого поряд-
ка является теоремой теории T.
Значительная часть теорем логики состоит в доказательстве утверждений вида
«Γ|–P» или «не Γ|–P» для разных теорий первого порядка, множеств Γ и разных (классов)
формул P.
Результат «Γ|–P» может доказываться посредством предъявления описания вывода
формулы P из Γ. Однако в мало-мальски сложных случаях оно оказывается настолько
длинным, что заменяется инструкцией по составлению такого описания, более или менее
полной. Наконец, доказательство «Γ|–P» может вообще не сопровождаться предъявлением
вывода P из Γ, хотя бы и неполного. В этом случае мы «не доказываем P, а доказываем,
что существует доказательство P».
Результат «не Γ|–P» в редких случаях может устанавливаться чисто синтаксиче-
ским рассуждением, но обычно доказательство опирается на конструкцию модели, т.е. ин-
терпретации, в которой Γ истинно, а P ложно.
4.4 Непротиворечивость, полнота и неразрешимость исчис-
ления предикатов
Теорема 4. Исчисление предикатов первого порядка непротиворечиво.
Теорема 5. (о полноте исчисления предикатов). В исчислении предикатов первого
порядка теоремами являются те и только те формулы, которые общезначимы.
Теорема 6. (Теорема Чёрча о неразрешимости исчисления предикатов, 1936). Не
существует алгоритма, который для любой формулы исчисления предикатов первого по-
рядка устанавливает, общезначима она или нет.
Теорема Чёрча остается в силе и для любой теории первого порядка, содержащей
все формулы исчисления предикатов первого порядка.
Теорема 5 показывает, что в логике предикатов синтаксический метод теорий пер-
вого порядка равносилен семантическому методу, использующему понятие интерпрета-
ции, модели, общезначимости и т. п. Для исчисления высказываний имеет место анало-
гичная эквивалентность семантических (тавтология и др.) и синтаксических (теорема и
др.) понятий. Отметим также, что для исчисления высказываний теорема о полноте систе-
мы приводит к решению проблемы разрешения. Однако для теорий первого порядка мы
не можем получить разрешающий алгоритм для общезначимости или, что тоже самое, для
выводимости в любом исчислении предикатов первого порядка.
26

Страницы