Диссертация (Автоматический логический вывод в интуиционистских логических исчислениях обратным методом Маслова), страница 12

Безобладает свойством чистотыпеременных: в любом выводе очищенной секвенции можно переименоватьпеременные требуемым образом, см. леммы 37 и 38 из § 78 книги [13].Доказательство несущественно отличается от доказательства теоремы 2 изработы С. К. Клини [16]. Назовем степенью выводаправил из списка, которые входят в выводчисло таких примененийне так, как того требует лемма.Будем строить доказательство индукцией по степени вывода.47Здесь скобки служат для группировки, а не для обозначения упорядоченной пары.

В дальнейшемподобные конструкции следует понимать именно в таком смысле, если явно не указано обратное.64При фиксированной степени вывода рассмотрим самое верхнее применениеправилаиз списка , для которого не выполняется условие леммы (если такихприменений несколько, выберем любое из них). Рассмотрим ту часть вывода,которая оканчивается применением. Рангом этой части вывода назовем числоприменений правил, которые находятся выше , но должны находиться ниже (этобудут применения правил, не входящих в список). Дальнейшее доказательствобудем выполнять индукцией по рангу.Пусть применению правилаправиланепосредственно предшествует применение. Из условия леммы следует, чтоодного из правил,,формула применения правила,может быть применением толькоили,.

При этом главнаяне совпадает ни с одной из боковых формулприменения правила .Перестановку применений правилив выводеможно выполнить также, как в лемме 7 из работы [16], за исключением следующих случаев (над чертойуказаны виды правил для, а под чертой — виды правил для ):В указанных случаях сложности возникают из-за отсутствия правиласокращения в исчислении. Однако эти трудности можно преодолеть,рассуждая как в доказательстве теоремы 3.1 из работы В. П. Оревкова [39] (вчастности, используя лемму 2.3). В случае, когдаправилаявляется применением, ограничение на собственную переменную продолжает выполнятьсяза счет свойства чистоты переменных.Послеперестановкипримененийправилоканчивающаяся новым применением правилаичастьвывода,, имеет меньший ранг, чемисходная часть вывода. Поэтому можно воспользоваться индукционнымпредположением и преобразовать эту часть вывода таким образом, чтобыполученная фигура удовлетворяла условию леммы.65Следующаятеоремафиксируетпромежуточныйрезультаторавнообъемности исчисленийи GHPC (при выводе замкнутых секвенций, сучетом определения).

Этот результат показывает, чтоподходит для построения исчисления обратного метода, равнообъемногоисчислению GHPC. Заметим, что А. Г. Драгалин в [10] показал равнообъемностьисчисления GHPC и исчисления HPC (исчисление предикатов Гейтинга).Теорема 2.1. Равнообъемность исчисленийзамкнутаясеквенция,соглашению 2.1, аформулойсеквенциясеквенцияформульныйполучается из. Секвенцияи GHPC.

Пустьобразкоторойсоответствуетзаменой каждого вхождения формулы видавыводима втогда и только тогда, когдавыводима в GHPC. Кроме того, есливыводима в—выводима в GHPC, тос помощью вывода той же или меньшей высоты.Доказательство вынесено в приложение А.2.5.2. Построение промежуточного исчисления для вывода замкнутыхформул в направлении «сверху вниз»В соответствии с «универсальным рецептом», первым шагом к построениюисчисления обратного метода на основе исчисленияявляется разработкапромежуточного исчисления для вывода замкнутых формул. Так как исчислениепредназначено для вывода в стиле табличных методов («снизу вверх»), аобратный метод работает в противоположном направлении, то в некоторыеправила вывода исчисленияисчисление назовемтребуется внести модификации.

Полученное. Схема аксиом и правила вывода этого исчисленияпредставлены в таблице 2.3.Во всех правилах из таблицы 2.3 посылки и заключения являютсясеквенциями вида (2.1). В схеме аксиомформулу. В правилахитермсимволсвободен дляобозначает атомарнуюв. Переменнаяправилахиудовлетворяет ограничению на собственную переменную:свободна дляви не входит свободно в заключение.в66Таблица 2.3.

ИсчислениеВ исчислениисокращенияиструктурными правилами вывода являются правила. Остальные правила являются логическими правиламивывода.Доказательства лемм 2.7 — 2.10 вынесены в приложение А.Лемма 2.7. Лемма о подсеквенциях. Для каждой секвенции , выводимой висчислениичто, существует такая выводимая в исчислении. При этом если выводвывода, то существует выводввсеквенция,содержит n применений правил, содержащий не более n + k примененийлогических правил, где k — число применений правилав исходном выводе.67Лемма 2.8. Если очищенная секвенциявыводима в исчислении, то в этом исчислении также выводима секвенцияэтом если высота исходного вывода секвенциисеквенции. Приравна n, то существует вывод, высота которого не превышает n + 1.Лемма 2.9. Если секвенциявыводима в исчислениито в этом исчислении также выводима секвенция,, причем спомощью вывода той же высоты.Лемма 2.10.

Если очищенная секвенция выводима в исчисленииона также выводима в исчислении, то, причем с помощью вывода той же илименьшей высоты.Теорема 2.2. Равнообъемность исчисленийвыводима ви. Секвенциятогда и только тогда, когда она выводима вНеобходимость. Секвенцияэта секвенция выводима ввыводима в..

Тогда по лемме 2.10.Достаточность. Секвенциявыводима в. Необходимо показать,Согласно лемме 2.7, существует подсеквенция, выводимая в исчислениичто она выводима в.. У секвенцииимеется только две подсеквенции: сама секвенцияпустая секвенция. Пустая секвенция невыводима в исчисленииследует, чтовыводима вивыводима секвенциявыводом секвенции. Отсюда.Лемма 2.11. Допустимость правила подстановки ввыводима ви.

Если секвенция— подстановка, допустимая для , то втакже, причем с помощью вывода, совпадающего с исходнымс точностью до применения к секвенциям подстановкии,возможно, переименования переменных.Пустьиз вывода— выводв исчислении. Применим ко всем секвенциямподстановку , переименовывая в случае необходимости связанныепеременные и собственные переменные вывода. Индукцией по высоте выводаубедимся, что в результате получится вывод секвенциив.68Перед переходом к окончательному исчислению обратного методасформулируем свойство подформульности исчисления.Лемма 2.12. Свойство подформульностисеквенциив исчислении.

Пусть— вывод. Тогда для любой входящей в выводсеквенциивыполняется следующее условие: каждая формуласеквенцию , может быть представлена в видевхождение подформулы в, где(положительное в случае, входящая в— подстановка, а—и отрицательное в)48.случаеДля самой секвенцииусловие леммы очевидным образомвыполняется. Поэтому достаточно проверить, что для каждого из правил выводавыполняется следующее условие: если заключение удовлетворяет условиюлеммы, то и все посылки удовлетворяют этому условию.Рассмотрим, например, применение правила:где для каждой формулы из заключения выполняется условие леммы.Тогда явно указанная в заключении формула, гдепредставима в виде— положительное вхождение подформулы вПусть, а— подстановка.— список всех переменных, входящих свободно в формулу:.

Тогда явно указанную в заключении формулуможно записать в виде, гдеполучается из формулывхождений переменныхТогда еслиивсоответственно. Точно так жеможно записать в виде.— (положительное) вхождение подформулы, принадлежащее вхождениюможно представить в виде48заменой всех свободныхтермамиявно указанную в посылке формулу, а формула, то указанную формулу.На самом деле в лемме утверждается чуть более сильное свойство, чем просто подформульностьисчисления. В монографии С.

Ю. Маслова [22] это свойство называется знакосохраняющим свойствомподформульности.69Остальные правила вывода рассматриваются таким же образом.2.5.3. Многосукцедентное исчисление обратного методаСледующий шаг «универсального рецепта» заключается в построенииокончательного исчисления обратного метода (для вывода замкнутых формул) сунификацией, обладающего свойством подформульности, как и исчислениеНовое секвенциальное исчисление.строится индивидуально для каждойдоказываемой формулы .Аксиомы и правила вывода исчислениявсех правилах, кромеиприведены в таблице 2.4.

Во, посылки являются правильными–секвенциями и не имеют общих свободных переменных друг с другом. Во всехправилахвидаи,и т. д.)49. В схеме аксиом50,–атомы;обозначают вхождения подформул ви(в том числе в записяхсимволыиобозначают— такие переименования, что— наиболее общий унификатор формулобщий унификатор подстановокии;. Подстановка. В правиле— наиболее— это –секвенция, а— –секвенция. В правилах— переименование.

В правиледолжно выполняться ограничение на собственную переменную:и— этопеременная, которая не входит свободно в заключение.Структурные правилаиназываются правилами сокращения, илипросто сокращением. Структурные правилаиназываются правиломпереименования и правилом нормализации соответственно.49Т. е. записи виданепосредственных подформул в50,и т. д. обозначают такие вхождения подформул в , что вхождения ихсовпадают с вхождениями, обозначенными какВ работе [45] эта схема аксиом называется.,и .70Таблица 2.4. ИсчислениеЗа счет правила переименования в исчисленииотождествляются–секвенции, отличающиеся лишь переименованием переменных. Правилонормализации введено для того, чтобы можно было сужать области определенияподстановок, если те содержат «лишние» элементы.Лемма 2.13. Из произвольной–секвенциив исчислениивывести правильную –секвенцию применениями правилиможно.71Пусть— такое переименование,чтои для всех–секвенцииправилопроизвольную –формулуподстановкас указанным переименованием, входящую в полученную –секвенциюиприменений правил.