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

Ю. Маслова [24].«Универсальный рецепт» состоит из трех основных этапов:1. Построение подходящего логического исчисления, предназначенного длявывода произвольных замкнутых формул в направлении «сверху вниз». Длярешенияэтойзадачиудобновыбратькакое-либосуществующеесеквенциальное исчисление, предназначенное для поиска вывода «снизувверх» (базовое секвенциальное исчисление), и «перестроить» его для поискавывода в противоположном направлении. Поскольку полученное на этомэтапе исчисление не является окончательным, будем называть егопромежуточным.2.

Определение свойства подформульности и процедуры унификации, послечегопереходотпромежуточногоисчислениякокончательномуисчислению обратного метода с унификацией. Это исчисление строитсяиндивидуально для каждой конкретной формулы, которую требуетсядоказать. При этом выводимые в исчислении секвенции должны содержатьтолько подформулы доказываемой формулы.3. Дополнение полученного исчисления стратегиями поиска вывода.В этой главе указанная методика используется для построения новогоинтуиционистского исчисления обратного метода для вывода формул логикипервого порядка.

Основная особенность этого исчисления заключается в том, чтооно является многосукцедентным. При доказательстве вспомогательных лемм и57теорем о полноте окончательного и промежуточного исчислений используютсяидеи доказательств из труда А. Дегтярева и А. Воронкова [68].2.4. Пример односукцедентного исчисления обратного методаВ работе А. Дегтярева и А. Воронкова [68] с помощью «универсальногорецепта» строится интуиционистское исчисление обратного методадлявывода замкнутых очищенных формул логики первого порядка.

В качествебазового секвенциального исчисления авторы указанной работы выбралиисчисление G3, сформулированное С. К. Клини [13, с. 425]. Исчислениестроится индивидуально для каждой доказываемой формулы . Исходя из видааксиом и правил выводасвязку, можно заключить, что формулаи логические константытексте. Таким образом, формулаИсчислениеине содержит, хотя это условие явно не указано всоответствует требованиям из соглашения 2.1.можно рассматривать как исправленный и улучшенныйвариант исчисления из статьи [139].В [68] при записи секвенций используются поляризованные формулы, т.

е.перед каждой формулой явно указывается метка с ее знаком:или. Так,классическая секвенция в промежуточном логическом исчислении определяетсякак конечное мультимножество поляризованных формул:(2.3)При этом интуиционистская секвенция определена как секвенция (2.3),содержащая не более одной формулы вида(т. е. это сингулярная секвенция).Таким же образом записываются секвенции исчисления:(2.4)где— подформулы , а— подстановки.В диссертационной работе используются другие формы представлениясеквенций, приведенные в формулах (2.1) и (2.2).58Замечание 2.1. Исчисления из работы [68] можно переформулировать сиспользованием секвенций вида (2.1) и (2.2).

При этом аксиомы и правила выводапреобразуются следующим образом: каждая поляризованная формула видасеквенции (2.3) переходит в формулуформула вида— в формулуизв антецеденте секвенции (2.1), а каждаяв сукцеденте секвенции (2.1). Секвенции (2.4)аналогичным образом преобразуются к виду, приведенному в формуле (2.2).Полученные в результате исчисления будут применимы для вывода секвенцийвидаили. Заметим, что оригинальные исчисления из работы [68]предназначены для вывода секвенций видаили.В таблице 2.1 представлены аксиомы и правила вывода46 исчисленияпереформулированныевтерминахнастоящейкандидатскойработы,,сиспользованием –секвенций. Здесь и далее названия аксиом и правил выводалогических исчислений указываются справа в круглых скобках.Во всех правилах из таблицы 2.1 посылки и заключения являютсясингулярными –секвенциями.

Также во всех правилах посылки не имеют общихсвободных переменных друг с другом и с множествомявляется единственной аксиомой исчисления, гдеподстановкапереименовывает в, а подстановкаиявляются–атомами,переменные, совпадающие с переменными из— наиболее общий унификатор формул— наиболее общий унификатор подстановокинаиболее общий унификатор упорядоченных пари. Правилои.

Подстановка. Подстановкаи—. Символы ,обозначают мультимножества, содержащие не более одной формулы. Вправилеобъединениемсимволиобозначаетпри условии, чтомультимножество,содержит не более одной формулы (впротивном случае правило неприменимо). В правилах46Особенно интересно правилостатье В. П. Оревкова [35].полученноеидолжно, имеющее необычный вид. Подобное правило также встречается в59выполняться ограничение на собственную переменную:— это переменная, невходящая в заключение.Таблица 2.1. ИсчислениеКроме указанных в таблице 2.1 правил, в исчислении также разрешаетсяприменять правило переименования переменных в секвенциях.60В работе [68] доказана равнообъемность исчислений(гдесоответствует соглашению 2.1) выводима вкогда эта секвенция выводима ви: секвенциятогда и только тогда,.

В той же работе отмечено, что исчисление неявляется полным в случае вывода секвенций произвольного вида.Исчислениеявляется односукцедентным. В следующем параграфебудет строиться другое интуиционистское исчисление обратного метода, котороеявляется многосукцедентным.2.5. Построение многосукцедентного исчисления обратного метода2.5.1. Базовое секвенциальное исчисление для вывода замкнутыхсеквенций в направлении «снизу вверх»Применим«универсальныйинтуиционистскому исчислениюприведены в таблице 2.2.Таблица 2.2. Исчислениерецепт»кмногосукцедентному, аксиомы и правила вывода которого61В аксиомеитермиз таблицы 2.2 P — это атомарная формула.

В правилахсвободен дляв. В правилахиудовлетворяет ограничению на собственную переменную:переменнаясвободна дляви не входит свободно в заключение.Исчислениесовпадает с исчислениемиз работы В. П. Оревкова[39]. Также это исчисление несущественно отличается от исчисления GHPCА. Г.

Драгалина [10] и от исчисления m-G3i из книги А. С. Трулстра иГ. Швихтенберга [149, с. 82]. Исчисления m-G3i и GHPC имеют следующуюособенность: вместо связкив них используется логическая константаОтрицание при этом определяется через импликацию:Исчислениесеквенциимогут..является многосукцедентным: выводимые в немсодержатьболееоднойформулывсукцеденте.Многосукцедентные интуиционистские исчисления используются в ряде трудовпо математической логике и основаниям математики. Кроме приведенных вышеработ, можно также отметить [102, 66, 73, 71].Замечание 2.2. Ограничения на собственные переменные в исчислениях, m-G3i и GHPC сформулированы по-разному. Однако при выводеочищенных секвенций (а именно этот случай интересует нас в этой главе) этиограничения эквивалентны.

Учитывая это наблюдение, исчислениепривыводе очищенных секвенций получается из исчисления GHPC заменой правилаправиломи, удалением аксиомы. Для удобства приведем здесь правилоОтличие этого правила от правилаи добавлением правилисчисления GHPC:исчислениязаключается вотсутствии  в сукцеденте левой посылки.Доказательство следующих четырех лемм о свойствах выводимостисеквенций в исчислениинезначительно отличается от доказательства лемм3.1.1, 3.1.3, 3.1.4 и 3.1.5 из монографии [10].62Лемма 2.1. Допустимость правила подстановки. Если всеквенция S и  — подстановка, допустимая для S, то ввыводиматакже выводимасеквенция S, причем с помощью вывода той же высоты.Лемма 2.2.

Допустимость правила утончения. Если всеквенция, то выводима и секвенциявыводима, причем с помощьювывода той же высоты.Лемма 2.3. Обратимость правил вывода. Все правила выводакроме правили,,, обратимы: из выводимости заключенияследует выводимость каждой из посылок.Рассмотрим подробнее правилаиисчисленияотличаются от правил исчисления GHPC. При этом правилотолько левой посылкой.

Обратимость правила, которыеотличаетсяследует из леммы 2.2. Из тойже леммы следует выводимость левой посылки правилав случаевыводимости заключения этого правила. В остальных случаях доказательствовыполняется в соответствии со схемой, намеченной в лемме 3.1.4 из [10].Лемма 2.4. Допустимость правила сокращения. Если всеквенция, то выводима и секвенциявывода той же высоты. То же верно для секвенцийвыводима, причем с помощьюи.Леммы 2.5 — 2.6 о преобразовании выводов в исчислениитакжебудут полезны в дальнейшем. В этих леммах мы будем использоватьтерминологию из статьи С. К.

Клини [16], где исследуется перестановочностьприменений логических правил в исчислении G, которое незначительноотличается от исчисления G2 из книги [13]. В частности, будем говорить, чтоприменение правила (или схемы аксиом)применению правиланепосредственно предшествует, если между ними отсутствуют применения другихправил.Пусть список,правиласостоит из следующих правил вывода исчисления. Пусть список,,и.включает все правила из списка:, а также63Лемма 2.5.

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

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