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

Необходимо найти секвенцию. Рассмотрим несколько частных случаев, в зависимости оттого, входят ли явно указанные формулы A и B в секвенциюСлучай 1.1., гдеоканчивается искомой секвенциейСлучай 1.2.,. Следующий вывод в:, гдеоканчивается искомой секвенцией.:. Следующий вывод в168Случай 1.3., гдеоканчивается искомой секвенциейСлучай 1.4.Случай 2.:, гдеПрименение.

Следующий вывод в. В этом случае можно взятьправила.Рассматривается.аналогичнопредыдущему случаю.Случай 3. Применение правилаПоиндукционному,исчисленияпредположениювыводимаяв, выводимую в.:существуетНеобходимонайтиСлучай 3.1., гдеоканчивается искомой секвенциейСлучай 3.2., гдеоканчивается искомой секвенциейСлучай 3.4.взятьсеквенцию. Рассмотрим несколько частных случаев, взависимости от того, входят ли явно указанные формулыСлучай 3.3.секвенцияив секвенцию.. Следующий вывод в:.

Следующий вывод в:, где, где. Можно взять. В этом случае также можно.Случай 4. Применение правила.исчисления:169По индукционному предположению существует выводимая всеквенция. Необходимо найти секвенциювыводимую в. Если, то можно взятьрассматривать случай, когдаправило,. Поэтому будем, гдеисчисления. Применив к секвенции(ограничение на собственную переменнуювыполняется), получим искомую секвенциюСлучай 5. Применение правила.исчисления:По индукционному предположению существуют секвенциии,выводимыев, выводимую в.

Аналогично, если.. Еслиинайти. Поэтому будемиправилосеквенцию, то можно взять, то можно взятьрассматривать случай, когда. Применим кНеобходимо, гдеисчисленияОбозначим секвенцию из заключения каки:. Поскольку, то серией применений правил сокращенияможно получить искомую секвенциюиик секвенции.Можно убедиться, что случай 1.1 — это единственный случай, когда вместоприменения одного правила исчисленияприменения логических правил исчисленияисчислениитребуется использовать дваПоэтому вывод секвенциивсодержит не более n + k применений логических правил, гдеn — общее число применений правил в исходном выводе секвенциичисло применений правила, а k—в исходном выводе.Лемма 2.8. Если очищенная секвенция, то в этом исчислении также выводима секвенциявыводима в исчислении.

При170этом если высота исходного вывода секвенциисеквенцииравна n, то существует вывод, высота которого не превышает n + 1.По лемме 2.6 существует такой выводсеквенциив исчислении,в котором каждому применению правила из списканепосредственнопредшествует применение аксиомы или правила из списка(см. определениясписковив пункте 2.5.1).

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

Секвенцияявляется аксиомой исчисленияТогда либо секвенция., либо некоторая секвенция, также является аксиомой. В первом случае секвенциюприменением правилаРассмотрим фигуруявляетсятакже является аксиомой.получена применением правила из списка .(как часть вывода ), в которой конечной секвенциейи которая содержит только применения аксиом и правил из спискапричем начальные секвенции фигурыфигуруможно вывести:Во втором случае секвенцияСлучай 2.

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

Еслине. В результате этого преобразования(той же или меньшей высоты) с конечнойсовпадает свыводом секвенции,, то заменим выводсеквенциитой же высоты (по лемме 2.2 мы это171можем сделать). Из секвенцииискомую секвенциюприменением правила. Если жепреобразовать в вывод секвенцииСлучай 3. Секвенцияилиполучим, то по лемме 2.2 выводможнотой же высоты.получена применением одного из правил,.Этот случай можно рассмотреть по аналогии со случаем 2, только фигурабудет состоять из единственного применения правила вывода.Случай 4. Секвенциявходящего в списокполучена применением правила вывода, не.Тогда посылками применения правилаявляются секвенции вида. Пользуясь индукционным предположением, заменим в каждойпосылке явно указанное вхождение формулыформулойзамену сделаем в заключении.

В результате применение правилаприменение того же правила, а вывод. Такую жеперейдет вперейдет в вывод секвенции,удовлетворяющий условиям леммы.Лемма 2.9. Если секвенциявыводима в исчислениито в этом исчислении также выводима секвенция,, причем спомощью вывода той же высоты.Доказательство индукцией по построению вывода. Если секвенцияявляется аксиомой, тотакже является аксиомой.

Если жеполучена понекоторому правилу вывода, то примем по индукционному предположению, чтолемма выполняется для всех посылок этого применения правила. Докажем, чтоотсюда следует выполнение леммы для его заключения.Рассмотримнесколькопоказательныхслучаев,остальныеслучаиотличаются незначительно.Случай 1. Применение правила:Пользуясь индукционным предположением, заменим посылку секвенцией, а само применение правила следующим применением:172Заключением нового применения правила является искомая секвенция.Случай 2. Применение правила:Это применение заменяется следующим:Заключением нового применения правила является искомая секвенция.Случай 3. Применение правила.Если рассматриваемая формулане является главной формулой этогоприменения правила, то последнее имеет следующий вид:Тогда в заключении можно заменить формулулюбой другойформулой, например формулой :Далее, по лемме 2.2 из выводимости секвенциивыводимость искомой секвенцииследует, причем с помощью выводатой же высоты.Теперь рассмотрим случай, когда формулаформулой применения правила:В этом случае по лемме 2.2 из выводимости посылкивыводимость искомой секвенциивысоты.является главнойследует, причем с помощью вывода той же173Лемма 2.10.

Если очищенная секвенция выводима в исчисленииона также выводима в исчислении, то, причем с помощью вывода той же илименьшей высоты.Доказательство индукцией по построению вывода в исчислении.Как в лемме 2.8, будем считать, что все входящие в вывод секвенции являютсяочищенными.Если секвенция является аксиомой исчисленияаксиомой исчисления, то она также является. Если же секвенция получена по некоторому правилувывода исчисления, то примем по индукционному предположению, чтолемма выполняется для всех посылок этого применения правила.

Докажем, чтоотсюда следует выполнение леммы для его заключения.Случай 1. Применение правилаилиисчисления— посылка рассматриваемого применения правила, аПо индукционному предположению. Пусть— его заключение.также выводима в исчислении.Тогда по лемме 2.4выводима вкоторую имеет вывод, т. е. высота полученного вывода не превышает высотывыводав исчислениис помощью вывода той же высоты,.Случай 2. Применение одного из правил,,или,,исчисления:— посылка рассматриваемого применения правила, азаключение. По индукционному предположениювыводима в. Применив к этой секвенции правилополучим секвенциюв исчислении— его.

Тогда полемме 2.2 (допустимость правила утончения) секвенциявыводима в,.Рассмотрим применение правилаПусть,такжеисчисления,. Высота полученного вывода не превышает высоты вывода.174Применения остальных правил рассматриваются аналогично, только вслучае применения правилиспользуется для ввода формулыии,в посылку, в случае применения правил— для ввода формулыформулыправило утончения, в случае применения, а в случае применения— для ввода— для ввода формулыСлучай 3.

Применение одного из правилили,.. Эти правилаявляются частными случаями соответствующих правил исчисленияправила(ав обоих исчислениях вообще совпадают). Отсюда автоматическиследует выполнение леммы.Случай 4. Применение двухпосылочных правилРассмотрим для примера применение правилаОбозначим левую и правую посылки какзаключение — каклемме2.2соответственно, аивыводимы всеквенцииТогда, применив к секвенциямииправило, причем с помощьюисоответственно.исчисления. При этом высота вывода секвенциипревышает высоты вывода этой секвенции в.Случай 5. Применение правилаисчисленияОбозначим посылку каксеквенция:также выводима ввыводов той же высоты, что и выводы секвенцийпредположениюисчисленияивыводимы в исчисленииполучим секвенцию.. По индукционному предположениюНеобходимо доказать, чтоПоили,, а заключение каквыводима вв,не:.

По индукционному. Тогда по лемме 2.8 ввыводима, причем с помощью вывода, высота которого не превышает высотывывода этой секвенции в исчислении.175Случай 6. Применение правилаисчисления:Обозначим посылку рассматриваемого применения правила какзаключение — как. По индукционному предположениюТогда по лемме 2.9 вправило., откуда по лемме, причем с помощью вывода,высота которого не превышает высоту вывода секвенцииПрименив квыводима ввыводима секвенция2.4 также выводима секвенция, а егоисчисленияв исчислении, получим секвенцию.. Приэтом из вышеизложенного рассуждения следует, что высота вывода секвенциивне превышает высоты вывода в.Лемма 2.15. Лемма подъема дляисчислении,а— вывод секвенциив— вхождение секвенции в вывод .