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

Пусть— такая. Тогда существует такая подстановка , чтокак.Рассмотрим два частных случая, в зависимости от того, входят ли в–формулыи.Случай 3.1. Хотя бы одна из –формулТогда, а значит,ине входит в. Отсюда.и выполняется условие«1.а».Случай 3.2. Обе –формулыТогдаивходят вимеет вид, где. Значит, подстановкиих наиболее общий унификатор.,— правильная –секвенция, то,.— наиболее общий унификатор подстановокоткуда..Так какТак какиии, то,унифицируемы, существуети при некоторой подстановкеимеет место184Применим к секвенцииправилоОбозначим заключение какподстановкеимеем:.

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

е. что переменнаяне входит свободно всеквенцию. Во-первых, переменная, так как для применения правилане входит свободно ввыполняется ограничениена собственную переменную. Во-вторых, так каки— тоже переменная. В-третьих, так каки, то, то переменная185не входит свободно в секвенциюсвободно в секвенцию, иначе переменнаявходила бы.Случай 5. Применение правила:Обозначения те же, что и для случая 4.Случай 5.1. –формулане входит вСлучай 5.2.

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

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

Пустьиисоответственно, аопределению отношения–секвенции, не— такие правильныеимеющие общих свободных переменных, чтоиисуществуют такие подстановки. Обозначим секвенциии. Поикаксоответственно.Рассмотрим два частных случая.Случай 7.1. Либо –формулане входит в..и выполняется условие «1.б».Случай 7. Применение правилазаключение как. Такне входит в, либо –формула, чтои187Рассмотрим случай, когдане входит в(альтернативный случайрассматривается аналогично).

В этом случае, откуда. Значит,выполняется условие «1.а».Случай 7.2.Тогдавходит вивходит в.имеет вид, где,иимеет вид, где,и, а.Без ограничения общности будем считать, что(иначеможносузитьобластиопределения. Тогдаи определена подстановкаэтом, а также,— правильные–секвенции.При, так какиИз вышесказанного следует, что к –формулами подстановкеподстановкаитакже являются правильными–секвенциями, так как служат посылками применения правилаиэтихпо определению –секвенцийподстановок). Такжеии.,иприменима лемма 3.1:,унифицируемы иявляется их унификатором.Применим к секвенциямиОбозначим заключение каксуществует такая подстановкаправило:. По свойству наиболее общего унификатора, что.

Тогдаи выполняетсяусловие «1.б».Лемма 3.3. Пустьи) — наборы –секвенций,(обладающие следующим свойством: для каждой –секвенции–секвенция, что. Тогда если формулабез применения схемы аксиом–секвенцийнайдется такаявыводима из–секвенций, то она также выводима избез применения схемы аксиом.188Пусть  — вывод формулыиз, не содержащий применений— произвольное вхождение –секвенции в вывод . Докажемаксиом. Пустьсуществование такой правильной–секвенции, чтоивыводима избез применения аксиом. Доказательство будем строить индукцией попостроению вывода –секвенции(как части вывода ).совпадает с одной из –секвенцийСлучай 1.леммы существует такая –секвенцияиз. Тогда по условию, что,можно вывести правильную –секвенцию.

По лемме 2.13применением правили(в силу допустимости процедуры поиска вывода на некотором шагеили поглощающая ее правильная –секвенция).действительно будет полученаИз леммы 3.2 (в частности, из транзитивности отношениявыполняется отношениеСлучай2.. Значит, можно взятьполучена, гдесуществуют такие правильныеивыводима изобщности будем считать, чтоприменением) следует, что.некоторогоправилавывода. Тогда по индукционному предположению–секвенции, что длябез применения аксиом. Без ограниченияне имеют друг с другом общихсвободных переменных.

В противном случае этого можно добиться применениемправилик(см. случай 1 и определение допустимойпроцедуры поиска вывода).Из леммы 3.2 и свойств отношения поглощения длядля некоторогоивыводима изобщности можно считать, что1). В первом случае можно взятьследует, что либо–секвенция, либо найдется такая, чтобез применения аксиом. Без ограниченияявляется правильной –секвенцией (см. случай, а во втором.Таким образом, мы доказали, что для произвольной–секвенциивходящей в вывод , существует такая правильная –секвенция , что,и189выводима избез применения аксиом. Поэтому для конечной секвенцииэто свойство также выполняется. Таким образом, существует такаяправильная–секвенция, чтоивыводима изприменения аксиом.

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

К. Клини [16]. Случаи перестановки применений правил группируютсяв соответствии с числом посылок правили: «1 посылка / 1 посылка»(11 × 8 = 88 случаев) и «2 посылки / 1 посылка» (3 × 7 + 2 = 23 случая)81.Еслиилиявляются применениями правилили, тоограничение на собственные переменные продолжает выполняться в новомвыводе за счет свойства чистоты переменных, за исключением следующихслучаев:,и,. Первые три случаяуказаны в качестве исключений в формулировке леммы, а четвертый не можетиметь места для исчисления81Случаи, когдаявляется применением одного из правилАналогично для применений правилнапример.

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

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

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