Математическая логика и теория алгоритмов. Сергиевская И.М. - 35 стр.

  Соотношение выполнено при любых значениях xi .                          Подставим этот набор
  значений в терм t : t ( x10 , x20 ,..., xi ,..., xn0 ) . Подставим последнее выражение в
  предикат A( x10 , x20 ,..., xi ,..., xn0 ) . Получим:
  A( x10 , x20 ,..., t ( x10 , x20 ,..., xi ,..., xn0 ),..., xn0 ) = 1 .
  Но, поскольку терм t свободен для переменной xi в формуле A , получаем:
   A( x10 , x20 ,..., t ( x10 , x20 ,..., xi ,..., xn0 ),..., xn0 ) = A(t )( x10 , x20 ,..., x n0 ) = 1.
  Следовательно, по свойству импликации получаем, что B0 = 1 , что и требовалось
  доказать.

     Теорема. Пусть xi не является свободной переменной в формуле A , B –
некоторая формула. Тогда формула ∀xi ( A → B ) → ( A → ∀xi B ) общезначима.
     Доказательство аналогично доказательству предыдущей теоремы.

     Теперь мы можем вернуться к построению теории первого порядка.

     3. Аксиомы теории первого порядка делятся на два класса:
• Логические аксиомы:
  1) A → (B → A) .
  2) ( A → (B → C )) → (( A → B ) → ( A → C )).
  3) (¬B → ¬A) → ((¬B → A) → B ) .
  4) ∀xi A( xi ) → A(t ) , где терм t свободен для переменной xi в формуле A( xi ) .
  5) ∀xi ( A → B ) → ( A → ∀xi B ) , где xi – несвободная переменная в формуле A .
         Отметим, что аксиомы 1) – 3) – тавтологии, 4) и 5) – общезначимые
  формулы.
• Собственные аксиомы.
         У каждой теории первого порядка свои собственные аксиомы.

     4. Правила вывода.
1) Modus ponens (МР).
   A, A → B ├ B .
2) Правило обобщения Gen.
    A ├ ∀xA .

     Определение. Теория первого порядка без собственных аксиом называется
исчислением предикатов первого порядка (или чистым исчислением предикатов).

     Без доказательства приведем теоремы.

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




                                                    40