Основные понятия и методы теории формальных систем. Волохович А.В. - 21 стр.

   непротиворечивым такое исчисление, в котором не выводимы
никакие две ППФ, из которых одна является отрицанием другой.
   Теорема.     Исчисление     предикатов     первого    порядка
непротиворечиво.
   Так как аксиомам исчисления предикатов соответствуют
выводимые ППФ исчисления высказываний, то, очевидно, что
всякой выводимой ППФ исчисления предикатов соответствует
выводимая ППФ исчисления высказываний. Из полноты исчисления
высказываний и непротиворечивости исчисления предикатов
вытекает, что всякая ППФ исчисления высказываний, выводимая из
исчисления предикатов, является выводимой ППФ исчисления
высказываний.
   Теорема. Во всяком исчислении предикатов первого порядка
всякая теорема является общезначимой ППФ.
   Теорема (Геделя о полноте). Во всяком исчислении предикатов
первого порядка всякая общезначимая ППФ является теоремой.



                  Пренексные нормальные формы

   В исчислении предикатов имеется пренексная нормальная форма
(ПНФ). Необходимость введения ПНФ будет обусловлена в
дальнейшем упрощением процедуры доказательства теорем.
   Сначала рассмотрим некоторые равносильные формулы в
исчислении предикатов. Напомним, что две формулы F и Ф
равносильны, т. е. F = Ф тогда и только тогда, когда истинностные
значения этих формул совпадают при любой интерпретации F и Ф.
Для подчеркивания факта, что переменная х входит в формулу F,
будем писать F[х], хотя F может содержать и другие переменные.
   Имеем следующие пары равносильных формул:

                   ∀ x F[х] ∨ Ф = ∀ x( F[х]    ∨ Ф);
                   ∀ x F[х] & Ф = ∀ x( F[х]    & Ф);
                   ∃ x F[х] ∨ Ф = ∃ x( F[х]    ∨ Ф);
                    ∃ x F[х] & Ф = ∃ x( F[х]   & Ф)

при условии, что переменная х не входит свободно в формулу Ф.
   Равносильность этих формул очевидна, так как формула Ф не
содержит свободно х и поэтому не входит в область действия
кванторов.
   Далее имеем
                 ∀ x F[х] & ∀ x Ф[х] = ∀ x( F[х] & Ф),
                  ∃ x F[х] ∨ Ф[х] = ∃ x( F[х] ∨ Ф[х]).



21