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

Поэтому, применив к–секвенцияи–секвенцииполучается из, то любой примерисводится к случаю единственного применения правила— пример –секвенции . Покажем, чтоСлучай 1. Применение правиласовпадает сцепочкойявляется примеромИндукцией по числу применений правилгде. Пусть, получим правильную –секвенцию.правилоЛемма 2.14. ЕслиПусть. Рассмотрим. Можно убедиться, что для подстановкивыполняется–секвенции.

Применим к.данная леммаили правилаявляется примером..:.По свойствам переименования, существует такая подстановка. Тогда для любой подстановкиОтсюда следует, чтосеквенцияявляется примером –секвенцииСлучай 2. Применение правилаиз определения операции, чтосовпадает с, совпадающей с... В данном случае непосредственноследует, чтоявляется примером.Заметим, что каждому правилу вывода (аксиоме) исчислениясоответствует одноименное правило вывода (аксиома) исчисленияэтомисчислениепостроенотакимобразом,чтобысформулированная ниже лемма подъема51.Доказательства лемм 2.15 и 2.16 вынесены в приложение А.51В статье [68] соответствующая лемма для исчисленияназвана «instance lemma»..

Привыполнялась72Лемма 2.15. Лемма подъема дляисчислении,а. Пусть— вывод секвенциив— вхождение секвенции в вывод . Тогда в исчислении–секвенциявыводима такая, что–секвенциисуществует выводявляется примеромв. Кроме того,, в котором порядок применениялогических правил вывода в точности соответствует порядку примененияодноименныхправилвтойчастивывода,котораяоканчиваетсярассматриваемым вхождением секвенции .— –секвенция, аЛемма 2.16. Пусть–секвенциявыводима в исчисленииисчислениисеквенции, то секвенция— вывод –секвенции. Еслив— ее основной пример. Тогда есливвыводима в, то существует вывод, в котором порядок применения логических правил вывода вточности соответствует порядку применения одноименных правил в выводе .Теперь можно доказать теоремы о равнообъемности исчисленияисчислениями GHPC.Теорема 2.3.

Равнообъемность исчисленийвыводима в исчисленииисчислении. Формулатогда и только тогда, когда она выводима в.Необходимость.–секвенцияНеобходимо показать, что секвенцияТак каквыводим вивыводима ввыводима в исчислениивыводима вчто –секвенциявыводима вПо теореме 2.2 секвенциявыводима в.., то по лемме 2.16 ее основной пример. Согласно теореме 2.2, секвенцияДостаточность. Секвенция.выводима ввыводима в..

Необходимо показать,.выводима в. По лемме 2.15 –секвенция73Теорема 2.4. Равнообъемность исчисленийвыводима в исчислениии GHPC. Формулатогда и только тогда, когда в исчислении GHPCвыводима формула, которая получается изподформулы видаформулойзаменой каждого вхождения.Следствие теорем 2.3 и 2.1.Так как исчисление GHPC равнообъемно [10] исчислению предикатовГейтинга (HPC), то из теоремы 2.4 следует, что исчислениетакжеравнообъемно исчислению HPC.Замечание 2.3. Вообще говоря, в схеме аксиомисчислениядостаточно применять переименование только к одной формуле, как это делаетсяв схеме аксиомисчисления(см.

таблицу 2.1). Однако приведенная втаблице 2.4 схема аксиом исчисленияпреимущества: для каждогоимеет определенные технические–атома можно зафиксировать «уникальное»переименование и использовать его во всех соответствующих применениях схемыаксиом, вместо того чтобы каждый раз заново подбирать подходящеепереименование. Схему аксиомисчисленияможно видоизменитьаналогичным образом. Нетрудно убедиться, что при этом новые аксиомы будутсовпадатьсаксиомамиисходногоисчислениясточностьюдопереименования переменных.Замечание 2.4. В [68] при доказательстве лемм 3.16 и 4.2 (леммы подъемадля исчисленийисоответственно) используется соглашение, которое втерминах настоящей работы можно сформулировать так: посылки каждогоприменения правила вывода должны быть правильными–секвенциями, азаключения применений правил всегда приводятся к правильным –секвенциям.Таким образом, в исчислениидействуют те же ограничения в правилахвывода, а также в неявном виде присутствует правило нормализации секвенций,как и в исчислении.742.5.4.

Пример алгоритма поиска выводаПусть— применение правила переименования к –секвенции :Будем называтьмножестваправильным переименованием относительно конечного–секвенций–секвенции,еслиивыполняетсядлякаждой.Заметим, что правильное переименование существует для произвольных, при этом соответствующую подстановкуиможно подобрать подобно тому, какэто делалось в доказательстве леммы 2.13. Можно также убедиться, что еслиполучена изправильным переименованием относительно произвольногоявляется правильной –секвенцией.множества , тоПростейший алгоритм поиска вывода формулыв исчисленияхиможет выглядеть так52.1. Пусть S — пустое множество секвенций, а T — множество, содержащееровно по одной аксиоме исчисления() для каждой различной пары–атомов53.2.

Если множество T пусто, завершаем работу: формула невыводима. Иначепереходим к шагу 3.3. Для всех секвенций из T последовательно выполняем следующуюпроцедуру:применяемксеквенцииправильноепереименованиеотносительно секвенций из множества S, к переименованной секвенцииприменяем правило52, полученную секвенцию добавляем в S.Приведенный алгоритм является вариантом метода насыщения уровня из книги [50]. Более экономныйалгоритм рассматривается в главе 4.53Таким образом, число аксиом будет конечным за счет отождествления секвенций, которые отличаютсялишь переименованием переменных.754. Если S содержит целевую секвенцию, завершаем работу: формулавыводима.

Иначе переходим к шагу 5.5. Полагаем T = . Ко всем новым секвенциям из множества S (и к такимпарам секвенций, хотя бы одна из которых является новой) применяем вседопустимые правила вывода исчисления(), кроме правилпереименования и нормализации, полученные секвенции добавляем в T.Возвращаемся к шагу 2.В приведенном алгоритме возможность применения правилаограничена, так как в противном случае к каждой секвенции было бы применимобесконечноечислопереименований.Такжеиспользуетсянебольшаядополнительная оптимизация: в S добавляются только правильные –секвенции,не имеющие общих переменных с другими –секвенциями из S.

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

Поэтому алгоритм позволяет за конечное число шагов вывестиформулу, если эта формула выводима в исчислениислучае невыводимости формулы(). Однако валгоритм может не завершить свою работу.2.6. Особенности построенного многосукцедентного исчисленияПостроенное в параграфе 2.5 исчислениеисчисленияимеет ряд отличий отиз работы [68] (см. параграф 2.4), а также от других известныхавтору интуиционистских исчислений обратного метода. Основные отличиязаключаются в следующем: исчислениеявляется многосукцедентным, тогда как существующиеисчисления являются односукцедентными;76 исчислениев явном виде содержит правило нормализации (в работе[68] аналогичное правило для исчисленияприсутствует лишь в виденеформальных соглашений, см. подробнее в замечании 2.4); в аксиомеисчисленияпереименования выполняются в обеихформулах, тогда как в исчислениипереименование применяется толькок одной формуле.Указанное изменение в аксиоменосит технический характер (см.замечание 2.3).Можно заметить некоторые сходства исчисленияс исчислением G,которое сформулировано С.

К. Клини в [16]. Однако основные отличия состоят втом, что исчислениеформулыстроится индивидуально для каждой доказываемой, в нем используются секвенции специального вида и унификация.Кроме того, интуиционистское исчисление G является односукцедентным исодержит правила утончения в явном виде. В исчисленииприсутствуют неявно в правилах,,,иутончения.2.7. ПримерВ [68] для правилиисчислениясформулировано следующееограничение на собственную переменную: «переменнаяне входит взаключение».

Назовем это ограничение сильным ограничением на собственнуюпеременную. Для исчисленияобразом (см. пункт 2.5.3): «переменнаяэта формулировка изменена следующимне входит свободно в заключение». Этоограничение назовем слабым ограничением на собственную переменную. Прииспользовании соглашения 2.1 можно применять любую из формулировок. Дляданного примера изменим наше соглашение 2.1, разрешив вхождение в формулувырожденных кванторов. Тогда различие в двух формулировках начинает играть77существенную роль: в этом случае использование сильного ограничения можетпривести к потере свойства полноты исчисления.Пример 2.1.

Рассмотрим формулу:где кванторявляется вырожденным. Черта над одним из предикатов указанадля удобства, чтобы отличать их в выводах. Отметим, что секвенциявыводима в GHPC.Перед построением вывода формулывхождения подформул вв исчислениивыпишем всеи определим их полярность. В таблице 2.5 перечисленыэти вхождения подформул, и каждому из них для удобства назначено уникальноеимя.Таблица 2.5. Подформулы доказываемой формулыИмя (вхождения)подформулыПодформулаПолярность++++Формуласодержит два вхождения атомарных подформул:и.

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