Математическая логика и теория алгоритмов. Стенюшкина В.А. - 21 стр.

покажем, что Г|−L А→Еi; тогда при i =n прямая теорема будет доказана. Итак,
пусть i = 1 (база индукции).
      Рассмотрим вывод:
        1) Е1; аксиома или посылка:
        2) Е1 → (А → Е1); А1:{А/В, Е1 /А};
        3) А → Е1; МР: 1,2.
        То есть Г|−LА → Е1
        Далее по методу предположим, что Г|−LА → Еi для всех i < k и рассмот-
рим Ek.. Здесь возможны случаи: либо Ek аксиома или посылка, тогда доказа-
тельство повторяет предыдущее, либо Еk получена по правилу МР из Ei, Ej;
причем i, j < k, и Ej: = Еi → Еk. В последнем случае, так как i, j < k , то для Ei
, Ej имеются выводы Г|−LА → Еi и Г|−LА → (Еi → Еk ). Объединим эти выводы
в один и достроим его до требуемого вывода:
        α1) A → Ei;
        α2) A → (Ei → Ek);
        α3) (A → (Ei → Ek)) →((A → Ei) → (A → Ek)); A2: {Ej./В, Ek /Сj};
        α4) (А → Еi) → (А →Аk); МР: α2 α3;
        α5) A → Ek МР: α1 α4.
        Итак, для Ek вывод построен. Тогда по методу математической индукции
заключаем, что для любого n имеет место выводимость Г|−LА → Еn. Поскольку
Еn:=В, то Г|−LА→B. Прямая теорема доказана.
        Доказательство обратной теоремы. Пусть имеем вывод Г|−LА → B, сос-
тоящий из β формул. Достроим его:
        β 1) А → В;
        β 2) А; гипотеза;
        β 3) В; МР: β 2, β 3.
        Таким образом, имеет место выводимость Г|−LА→B. Обратная теорема
доказана. Теорема доказана.
        Cледствие Если А|−LВ, то |−L A → В и обратно. Доказательство Г: =∅.

       5.4 Применение ТД

      Теорема 5.3 Имеет место выводимость: А → В, В → С|−LА → С.
      Доказательство Сначала докажем выводимость А → В, В → С|−L → С:
      1) А → В; гипотеза;
      2) В → С; гипотеза;
      3) А; гипотеза;
      4) В; МР: 3,1;
      5) С; МР: 4,2.
      Вывод для С построен. Теперь по теореме дедукции заключаем, что А →
В, В → С|−LА → С. Теорема доказана. Эта теорема дает производное правило
A → B, B → C
              Tr , называемое правилом транзитивности:
    A→C