Скачать 13.21 Кбайт
Обратный метод С.Ю. Маслова
После этого исходная секвенция ® Ф разбивается на две (® Ф1 и ® Ф2), в которых исходная формула Ф упрощается (до Ф1 и Ф2, соответственно) за счет применения правила исключения однолитерных дизъюнктов (см. выше лемму 2). Это является эквивалентным преобразованием формулы.
Классическое правило расщепления (1) в секвенциальном исчислении выглядит так:
® Ф1 (C) ® Ф2 (~C)
® Ф, C ® Ф, ~C
® Ф, C & ~C
® Ф
Здесь Ф1 (Ф2) — результат применения леммы 2 к формуле Ф Ъ C (Ф Ъ ~C).
Отметим при этом, что в секвенциальном исчислении правило расщепления структурно (как и ранее — правило Б ОМ) соответствует контрприменению правила сечения, или является аналогом контрприменения правила резолюции.
Такое представление правила расщепления позволяет предложить еще одно допустимое — за счет идеологии правила Б обратного метода — правило вывода, в котором происходит «расщепление» не по противоречивому дизъюнкту C & ~C как в оригинальном правиле расщепления, а по некоторому дизъюнкту исходной формулы Ф (допустимость этого правила основана на том, что приписывание к исходной формуле Ф любого числа ее дизъюнктов — это сделано на втором уровне секвенциального дерева (см. ниже)— является эквивалентном преобразованием формулы). Правило расщепления (2) по некоторому дизъюнкту формулы Ф выглядит так:
® Ф1 (C) ® Ф2 (B)
® Ф, C ® Ф, B
® Ф, C & B
® Ф
Установив сходство правила расщепления и правила Б мы можем промоделировать правило расщепления (1) и (2) за счет «расширения» сферы действия тривиального применения правила Б обратного метода (вернее, тривиального применения правила Б* с учетом моделирования правила резолюций). Назовем его правилом Б**:
ТРИВИАЛЬНЫМ ПРИМЕНЕНИЕМ ПРАВИЛО Б* назовем такое его применение к некоторому благоприятному набору с зависимостью, в результате которого некоторое число с индексом (на обязательно с индексом ноль как в исходном тривиальном правиле Б — см. выше) исключается из состава набора и переносится в его зависимость.
Для сохранения теоремы о полноте сформулируем следующую лемму:
ЛЕММА 4
Любой вывод с применением правила Б** соответствует выводу такой секвенции Ф*, которая получена добавлением к формуле Ф некоторых ее литер, соответствующих числам с индексами в зависимости пустого благоприятного набора.
Для более строгого обоснования допустимости применения расширенного правила Б** построим метаисчисление благоприятных наборов — исчисление зависимостей.
Объектами этого метаисчисления будут выступать пустые благоприятные наборы с зависимостями — т.е. выводы — исходного исчисления благоприятных наборов, которые будем обозначать набором чисел в круглых скобках, например: (А, …, В, С). Назовем такие объекты зависимостями.
ПРАВИЛО С (задает базис метаисчисления): зависимости, полученные при выводах исходного исчисления благоприятных наборов — т.е. при нольчленных благоприятных наборах с применением правил А и Б — являются исходными благоприятными зависимостями.
ПРАВИЛО В (правило вывода метаисчисления, которое задает механизм образования новых благоприятных зависимостей): если зависимости (An ... H1), (Bp ... H2), .., (Сm ... Hp) являются благоприятными зависимостями и H1, ..., Hp составляют совокупность литер, которая либо содержит контрарную пару литер (исходное правило (1) расщепления), либо графически равна некоторому дизъюнкту исходной формуле (правило (2) расщепления), то зависимость (Аn , … Bp , …, Сm) также является благоприятной зависимостью.
ВЫВОДОМ называется линейная последовательность благоприятных зависимостей, последним членом которой является пустая благоприятная зависимость ( ) — зависимость без чисел с индексами (это — как видно — соответствует выводу в исходном исчислении благоприятных наборов; см. доказательство теоремы о полноте ниже).
ТЕОРЕМА О ПОЛНОТЕ
Любой вывод исчисления зависимостей (с учетом использования правила Б**) может быть перестроен в вывод секвенциального исчисления с правилом расщепления (правилами (1) и (2) расщепления) и наоборот.
Доказательство теоремы основано на лемме 4. Дадим здесь идею доказательства. Исходные зависимости (как это задано в правиле С метаисчисления) соответствуют выводам формул Ф* в секвенциальном исчислении, которые возможно получены из Ф приписыванием дополнительных однолитерных дизъюнктов из числа литер формулы, а применение правила В — допустимому правилу расщепления. Если получена пустая благоприятная зависимость, т.е. зависимость, содержащая в своем составе только числа без индекса, то получен вывод либо самой формулы Ф, либо более сильной формулы без некоторых дизъюнктов формулы Ф. Обратный переход секвенциальных выводов основан на алгоритме прополке (см. теорему о полноте исчисления благоприятных наборов) и структурному сходству правила Б** правилу расщепления, которое допустимо в секвенциальном исчислении.
Приведем два примера выводам в метаисчислении, которые соответствуют различным стратегиям правила расщепления — правилу (1) и правилу (2) расщепления.
Классическое правило расщепления (1) в секвенциальном исчислении выглядит так:
® Ф1 (C) ® Ф2 (~C)
® Ф, C ® Ф, ~C
® Ф, C & ~C
® Ф
Здесь Ф1 (Ф2) — результат применения леммы 2 к формуле Ф Ъ C (Ф Ъ ~C).
Отметим при этом, что в секвенциальном исчислении правило расщепления структурно (как и ранее — правило Б ОМ) соответствует контрприменению правила сечения, или является аналогом контрприменения правила резолюции.
Такое представление правила расщепления позволяет предложить еще одно допустимое — за счет идеологии правила Б обратного метода — правило вывода, в котором происходит «расщепление» не по противоречивому дизъюнкту C & ~C как в оригинальном правиле расщепления, а по некоторому дизъюнкту исходной формулы Ф (допустимость этого правила основана на том, что приписывание к исходной формуле Ф любого числа ее дизъюнктов — это сделано на втором уровне секвенциального дерева (см. ниже)— является эквивалентном преобразованием формулы). Правило расщепления (2) по некоторому дизъюнкту формулы Ф выглядит так:
® Ф1 (C) ® Ф2 (B)
® Ф, C ® Ф, B
® Ф, C & B
® Ф
Установив сходство правила расщепления и правила Б мы можем промоделировать правило расщепления (1) и (2) за счет «расширения» сферы действия тривиального применения правила Б обратного метода (вернее, тривиального применения правила Б* с учетом моделирования правила резолюций). Назовем его правилом Б**:
ТРИВИАЛЬНЫМ ПРИМЕНЕНИЕМ ПРАВИЛО Б* назовем такое его применение к некоторому благоприятному набору с зависимостью, в результате которого некоторое число с индексом (на обязательно с индексом ноль как в исходном тривиальном правиле Б — см. выше) исключается из состава набора и переносится в его зависимость.
Для сохранения теоремы о полноте сформулируем следующую лемму:
ЛЕММА 4
Любой вывод с применением правила Б** соответствует выводу такой секвенции Ф*, которая получена добавлением к формуле Ф некоторых ее литер, соответствующих числам с индексами в зависимости пустого благоприятного набора.
Для более строгого обоснования допустимости применения расширенного правила Б** построим метаисчисление благоприятных наборов — исчисление зависимостей.
Объектами этого метаисчисления будут выступать пустые благоприятные наборы с зависимостями — т.е. выводы — исходного исчисления благоприятных наборов, которые будем обозначать набором чисел в круглых скобках, например: (А, …, В, С). Назовем такие объекты зависимостями.
ПРАВИЛО С (задает базис метаисчисления): зависимости, полученные при выводах исходного исчисления благоприятных наборов — т.е. при нольчленных благоприятных наборах с применением правил А и Б — являются исходными благоприятными зависимостями.
ПРАВИЛО В (правило вывода метаисчисления, которое задает механизм образования новых благоприятных зависимостей): если зависимости (An ... H1), (Bp ... H2), .., (Сm ... Hp) являются благоприятными зависимостями и H1, ..., Hp составляют совокупность литер, которая либо содержит контрарную пару литер (исходное правило (1) расщепления), либо графически равна некоторому дизъюнкту исходной формуле (правило (2) расщепления), то зависимость (Аn , … Bp , …, Сm) также является благоприятной зависимостью.
ВЫВОДОМ называется линейная последовательность благоприятных зависимостей, последним членом которой является пустая благоприятная зависимость ( ) — зависимость без чисел с индексами (это — как видно — соответствует выводу в исходном исчислении благоприятных наборов; см. доказательство теоремы о полноте ниже).
ТЕОРЕМА О ПОЛНОТЕ
Любой вывод исчисления зависимостей (с учетом использования правила Б**) может быть перестроен в вывод секвенциального исчисления с правилом расщепления (правилами (1) и (2) расщепления) и наоборот.
Доказательство теоремы основано на лемме 4. Дадим здесь идею доказательства. Исходные зависимости (как это задано в правиле С метаисчисления) соответствуют выводам формул Ф* в секвенциальном исчислении, которые возможно получены из Ф приписыванием дополнительных однолитерных дизъюнктов из числа литер формулы, а применение правила В — допустимому правилу расщепления. Если получена пустая благоприятная зависимость, т.е. зависимость, содержащая в своем составе только числа без индекса, то получен вывод либо самой формулы Ф, либо более сильной формулы без некоторых дизъюнктов формулы Ф. Обратный переход секвенциальных выводов основан на алгоритме прополке (см. теорему о полноте исчисления благоприятных наборов) и структурному сходству правила Б** правилу расщепления, которое допустимо в секвенциальном исчислении.
Приведем два примера выводам в метаисчислении, которые соответствуют различным стратегиям правила расщепления — правилу (1) и правилу (2) расщепления.
|
|