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

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

Из леммы 2.12 следует, что настоящая лемма выполняетсядля любой секвенции , выводимой по схеме аксиомпомощью схемы аксиом–секвенцию, чтоТеперь пустьисчисленияисчисленияявляется примеромисчисления: сможно вывести такую.получена применением некоторого правила вывода. Примем по индукционному предположению, что лемма176выполняется для всех посылок этого применения правила. Требуется доказать,что отсюда следует выполнение леммы для его заключения.Рассмотрим случай применения правилаисчисления, дляостальных случаев доказательство несущественно отличается от доказательствлемм 4.2 и 3.16 из работы [68].

Для упрощения изложения будем считать, чтопосылка содержит только две формулы.Пусть секвенцияполучена применением правила. Пользуясьлеммой 2.12, будем записывать формулы в секвенциях в видеподстановка, а, где—— вхождение подформулы в :где.Обозначим посылку как, а заключение как .По индукционному предположению существует такая выводимая в–секвенцияисчислениипримером, чтоявляется. Необходимо доказать существование такой выводимой в–секвенции, чтоявляется примеромБез ограничения общности будем считать, что.является правильной–секвенцией, иначе воспользуемся леммами 2.13 и 2.14 и заменим ее такойправильной –секвенцией, которая получается изприменением правили.Так какявляется примером, то найдется такая подстановкаиИз правильности, что.следует, чтои. Поэтому, не умаляя общности, можносчитать, чтовзять подстановку: в противном случае вместо.можно177Докажем, что подстановка, где,унификаторомподстановоки–секвенцииисвойствизДействительно,.являетсяизподстановкиправильностиследует,чтои.Так как подстановкииунифицируемы, то существует их наиболееи к –секвенцииобщий унификатор (обозначим его какправило выводаисчисленияОбозначим заключение какприменимо:.

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

Пусть, что. Далее, по свойствуимеемпримеромТак. Поитакже.— ее основной пример. Тогда если, то секвенция— вывод –секвенциииввыводима в, то существует вывод, в котором порядок применения логических правил вывода вточности соответствует порядку применения одноименных правил в выводе .Доказательство индукцией по построению вывода в исчисленииБаза индукции. Если –секвенцияполучена применением схемы аксиом, то в этом случае основной примерпомощью одноименной схемы аксиом..выводим в исчислениис178Теперь пустьисчисленияполучена применением некоторого правила вывода. Примем по индукционному предположению, что леммавыполняется для всех посылок этого применения правила.

Требуется доказать,что отсюда следует выполнение леммы для его заключения. Разберем несколькохарактерных случаев, в зависимости от вида примененного правила:;;;;;;.Для упрощения изложения будем считать, что посылка правиласодержит только две формулы, а все посылки логических правил вывода содержаттолько одну формулу (доказательство в общем случае отличается незначительно).Случай 1. Применение правилагде в заключении стоит –секвенция:.–секвенцийВ этом случае основные примерыисовпадают сточностью до переименования переменных, поэтому по лемме 2.11 извыводимости первого из них следует выводимость второго в исчислениипричем с использованием тех же логических правил в том же порядке.Случай 2.

Применение правилагде в заключении стоит –секвенция:.Этот случай тривиален, так как основные примерыСлучай 3. Применение правила:исовпадают.,179где в заключении стоит –секвенцияОбозначим посылку каксеквенцию.. Рассмотрим основной пример, а также основной пример. По индукционному предположению секвенцияНеобходимо доказать, что секвенция— секвенциювыводима в..По лемме 2.11 вывод секвенцииможно перестроить в вывод секвенциив исчислении, не нарушая порядка применениялогических правил.

Посколькуивыводима в—— наиболее общий унификатор подстановок, тосеквенции, поэтомуправилоисчисленияТаким образом, секвенция. Применим к:выводима вСлучай 4. Применение правила.:По индукционному предположению секвенциявыводима в. Требуется показать, что секвенцияПрименим к секвенцииТаким образом, секвенциявыводима вправилоисчислениявыводима вСлучай 5. Применение правилагде в заключении стоит –секвенция.:.:.Обозначим левую и правую посылки какиндукционному предположению основные примерыисоответственно. По–секвенцийи180выводимыв.Выпишемсоответствующиеосновныепримеры:.

Требуется показать, что в,основной пример –секвенциивыводим, т. е. секвенцияПо лемме 2.11 выводы секвенций.ив исчисленииперестроить в выводы секвенцийможноисоответственно, не нарушая порядка применения логических правил. Применим ксеквенциямиПосколькуправилоисчисления— наиболее общий унификатор подстановок,следует,:ипоэтому.что,, тоОтсюдапоэтомуполученная секвенция совпадает с секвенцией .Случай 6.

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

Также поограничению на собственную переменную для применения правилак181переменнаяне входит свободно всобственную переменнуюсвободна дляв. Поэтому ограничение навыполняется и для применения правилак:и не входит свободно в заключение. При этом заключениесовпадает с искомой секвенцией .Случай 7. Применение правила. Рассматривается аналогичнопредыдущему случаю, только не нужно проверять выполнение ограничения насобственную переменную.Во всех случаях порядок применения логических правил сохраняется припереходе от исчисленияк исчислению.182ПРИЛОЖЕНИЕ Б.

ДОКАЗАТЕЛЬСТВА ПРОМЕЖУТОЧНЫХУТВЕРЖДЕНИЙ ИЗ ГЛАВЫ 3Далее приводятся формулировки и доказательства некоторых лемм из главы3, вынесенные в приложения из-за объемности доказательств. Используются те жетермины и соглашения, что и в главе 3.Лемма 3.2. Отношениеявляется отношением поглощения для исчисления.Второе условие из определения отношения поглощения выполняется:если,иявляется правильной –секвенцией, тоТретье условие также выполняется, так как из отношенийследует.и.Для проверки первого условия следует рассмотреть случаи применениякаждого из правил вывода исчисления.

Рассмотрим следующие правилавывода (случаи применения других правил отличаются незначительно):;;;;;;.Для доказательства леммы требуется показать, что в каждом случаевыполняется одно из условий 1.а или 1.б из определения отношения поглощения(далее будем ссылаться на эти условия как на условия «1.а» и «1.б»).Случай 1. Применение правила переименования:183Пустьотношения, где–секвенция. Тогда по определению— правильнаясуществует такая подстановка , что. Отсюдаи.

Таким образом, выполняется условие «1.а».Случай 2. Применение правила нормализацииПустьподстановка, где–секвенция. Тогда существует такая— правильная, что:. Отсюдаи. Такимобразом, выполняется условие «1.а».Случай 3. Применение правила сокращенияОбозначим посылку какправильная –секвенция, что. Обозначим секвенцию:, а заключение как.