Содержание к диссертации
Введение
1 Отраженная логика доказательств . 11
1.1 Основные определения 11
1.2 Конструкция наименьшей модели 13
1.3 Отраженный фрагмент логики доказательств 18
1.4 Сложность фрагментов логики доказательств 20
2 Типизация термов в рефлексивной комбинаторной логике . 26
2.1 Определение правильно построенных формул RCL 26
2.2 Типизация подтермов 28
2.3 Типы в RCL 32
2.4 Соответствие между правильно построенными формулами и типами 37
2.5 Восстановление типов 41
3 Выводимость в рефлексивной комбинаторной логике . 48
3.1 Выводимость из гипотез в RCL 48
3.2 Устранение сечения в RCLTG 52
3.3 Разрешимость RCLTG 67
3.4 Оценки сложности 72
- Конструкция наименьшей модели
- Сложность фрагментов логики доказательств
- Типизация подтермов
- Устранение сечения в RCLTG
Введение к работе
Актуальность темы
Под свойством интернетизации выводов для формальной системы ниже понимается ее способность формализовать рассуждения про свои собственные выводы и их связь с выводимыми ими формулами. Теории со свойством ин-тернализации выводов являются предметом рассмотрения Второй теоремы Гёделя о неполноте формальной арифметики и играют центральную роль в многочисленных исследованиях в этом направлении (см., например, [1] * ). Типичным примером теории такого рода является формальная арифметика первого порядка РА (арифметика Пеано). Гёделевская нумерация синтаксиса РА позволяет определить инъективное кодирование формул и выводов натуральными числами таким образом, что предикат доказательств
"х есть код вывода формулы с гёделевским номером у"
оказывается выразимым арифметической формулой Prf(x,y). При этом для любой арифметической формулы (р справедливо
PA h ^ -ФФ- РА Ь Prf(n, гірп) для некоторого натурального числа п.
(Здесь п — нумерал, соответствующий числу п, а гір~* — гёделевский номер формулы 1р.)
Множество всех теорем РА вида Prf(n, rtp~l) образует отраженный фрагмент РА. Фактически, он уже содержит формулировки всех доказуемых в РА утверждений, но в несколько иной форме — в виде их гёделевских номеров. В то же время он существенно проще множества всех теорем РА: отраженный фрагмент РА разрешим, в то время как множество всех теорем РА неразрешимо. Аналогичное наблюдение имеет место для всех рекурсивно аксиоматизируемых расширений Т теории РА истинными (в стандартной модели арифметики) формулами.
Факт простого устройства отраженного фрагмента для всех этих теорий уточняется как утверждение о его разрешимости, в то время как сама теория неразрешима. Такой подход неприменим в случае разрешимых теорий. Для
'[1|СморинскиЙ К. Теоремы о неполноте // В кн.: Дж. Барвайс, ред. Справочная книга по математической логике Ч IV М.- Наука, ЦЩ, ?г|»иои/, -t ,-
j БИБЛИОТЕК '
них вопрос о сравнении проблем разрешения самой теории и ее отраженного фрагмента до настоящей работы оставался открытым.
Примеры пропозициональных формализмов со свойством интернализации выводов построены в работах С.Н. Артёмова. Это логика доказательств LP [2J 2, [3] 3 и рефлексивная комбинаторная логика RCL_ [4] 4. В языках этих теорий присутствуют термы, играющие роль обозначений для выводов, и конструкция формул t:F, выражающая предикат доказательств "t есть вывод формулы F", причем формула F выводима в теории тогда и только тогда,
когда выводима формула t:F для некоторого терма t. Для логик LP и RCI ,
вопрос о сравнении сложности отраженного фрагмента (т.е. множества всех теорем вида t:F) и множества всех теорем теории остается актуальным, но требует другой формализации, так как обе системы оказались разрешимыми.
Разрешимость логики доказательств LP установлена в [5] 5 с помощью
развитой в этой работе техники символических моделей. Оценка сложности
разрешающего алгоритма для LP получена в [6J 6 : LP принадлежит клас
су Пд полиномиальной иерархии. До настоящей работы вопрос о сложности
отраженного фрагмента логики доказательств LP, а также вопросы о разре
шимости и сложности рефлексивной комбинаторной логики RCI . и ее отра
женного фрагмента не были изучены.
Определение понятия вывода в рефлексивной комбинаторной логике RCI ,
в качестве составной части содержит определение правильной построенное
формул. Эта компонента является расширением правил типизации термов
средствами комбинаторной логики Карри CI „ для которой задачи провер
ки правильности типизации и восстановления типов термов разрешимы за
полиномиальное время (см. [7] г ). Для RCL_, аналогами указанных задач
являются задачи распознавания правильной построенности формул и вос-
2[2]ARTEMOV S. Operational Modal Logic // Technical Report MSI 95-29,Cornell University, 1995
3[3]Abtemov S Explicit provability and constructive semantics // The Bulletin of Symbolic Logic, 7(1):1-36, 2001
4 [4] Артёмов С H Подход Колмогорова и Гёделя к интуиционистской логике и работы последнего десятилетия в этом направлении // Успехи матем. наук, 2004, 59, вып. 2 (356), 9-36
5[5]MKRTYCHEV A Models for the logic of proofs // Lecture Notes in Computer Science, v. 1234, 1997, 266-275
*[6JKUZNETS R On the complexity of explicit modal logics // Lecture Notes in Computer Science, v. 1862, 2000, 371-383
t[7]Troelstra A.S., Schwichtenberg H. Basic proof theory // Cambridge: Cambridge Univ. Press, 1996
становления в них типовой разметки, вопрос о сложности которых до настоящего времени оставался открытым. Получение полиномиальных верхних временных оценок для них представляется важной промежуточной задачей, необходимой для оценки сложности отношения выводимости В RCL-.
Цель работы
Целью работы является доказательство разрешимости и получение оценок сложности для ряда алгоритмических проблем, связанных с отраженным фрагментом RLP логики доказательств LP (оценить сложность разрешения),
рефлексивной комбинаторной логикой RCI , и ее отраженным фрагментом
(доказать разрешимость и оценить сложность разрешения) и задачей типизации термов средствами RCL^ (предложить полиномиальный по времени алгоритм восстановления типов).
Основные методы исследования
В диссертации использованы методы теории доказательств и теории сложности вычислений. В частности, использовались техника символических моделей для логики доказательств, усовершенствованный автором метод устранения сечения, прототипом которого явилось синтаксическое доказательство устранимости правила сечения для интуиционистской логики доказательств, сведение задачи построения вывода к задаче унификации, а также техника доказательства верхних оценок сложности, основанная на игровой характе-ризации класса PSPACE.
Научная новизна
Результаты работы являются новыми. Основными из них являются следующие:
1. Пусть LP(CS) обозначает вариант логики доказательств LP с ограниченным правилом (Nee) - дополнительно требуется, чтобы его заключение принадлежало заданному конечному множеству формул CS. Показано, что отраженный фрагмент логики доказательств LP (CS) есть теория одной символической модели. В качестве следствий установлен
ряд утверждений, упрощающих поиск выводов в LP, в частности, следующий вариант дизъюнктивного свойства:
LP (- s:F V W « LP h a:F или LP h fcG.
-
Установлено, что отраженный фрагмент логики доказательств LP принадлежит классу NP. Эта верхняя оценка ниже известной верхней оценки для всей логики LP. Аналогичная оценка доказана также для более широкого фрагмента — множества всех теорем LP, являющихся монотонными булевыми комбинациями квазиатомарных формул.
-
Для рефлексивной комбинаторной логики RCL_ предложено явное определение типов. Доказана единственность типизации термов средствами RCI ,. Установлено, что задачи восстановления типов и проверки правильной построенности формул для RCL_ разрешимы за полиномиальное время.
-
Предложено секвенциальное исчисление, формализующее отношение выводимости из гипотез в рефлексивной комбинаторной логике RCL_. Показано, что правило сечения в нем устранимо. Отсюда следует, что отраженный фрагмент рефлексивной комбинаторной логики разрешим за полиномиальное время.
5 Доказано, что отношение выводимости из гипотез в логике RCI , разре
шимо и PSPАСЕ-полно.
Апробация работы
Результаты диссертации докладывались на научно-исследовательском семинаре кафедры математической логики и теории алгоритмов Механико-математического факультета МГУ (руководители семинара — академик РАН, профессор С И. Адян и профессор В.А Успенский, 2005 г.), на семинаре лаборатории математической логики Санкт-Петербургского Отделения Математического института им. В.А.Стеклова РАН (2005 г.), на семинаре "Логические проблемы информатики"(руководители семинара — профессора С Н. Артемов, MP Пентус и доценты В.Н. Крупский. ТЛ. Яворская, неоднократно), а также на XXIV Конференции молодых ученых Механико-математического факультета МГУ (2002 г.).
Публикации
Результаты диссертации опубликованы в работах [1-5], список которых приводится в конце реферата.
Структура и объем работы
Конструкция наименьшей модели
Покажем, что выводимость в LP(CS) квазиатомарных формул можно охарактеризовать единственной моделью, которая оказывается наименьшим элементом в классе всех рефлексивных CS-моделей. Наличие наименьшей модели позволяет также установить варианты дизъюнктивного свойства, справедливые для исчислений LP (Сі?) и LP. Определение 1.2.1 На множестве всех свидетельских функций можно определить частичный порядок следующим образом: , если (t) С (t) выполняется для всех термов t Є Тт. Определение 1.2.2 Определим частичный порядок на множестве всех моделей. Пусть М — (v, , f=) и М — (і/, , = ) — модели. Тогда М М\ если и v v (последнее неравенство означает, что v(S) = True влечет vr(S) — True для каждой переменной S Є SVar). Лемма 1.2.3 Для каждой спецификации констант CS существует CS-свидетелъская функция , для которой выполняется для каждого терма і и каоїсдой формулы F. Доказательство. Пусть дана спецификация констант CS {с\ : AL, ... ,сп :Ап}. Опишем пошаговый процесс вычисления значений функции . Фиксируем последовательность термов ii,t2,.-., содержащую все термы по доказательствам, где каждый терм встречается бесконечно много раз. На шаге k = 0,1,... для каждого t Є Тт определим множество формул fc(t), причем при t 7 tk и к 0 полагаем k{t) = jfc-i( )-ШагО. Шаг /г 0, вычисление значения k(tk)-Случай ifc = hs. Положим k{tk) равным Случай tk — h + s. Положим k(h) — k-i(tk) U &(M U k(s)-Случай tk—\s. Положим k{h) = -і(йь) U {s:F [ Fe k{s)}. В остальных случаях, т.е. когда tk является переменной или константой, полагаем () = jt-i(i). Для t Є Тт определим () = Ujb=o fc( )- По построению, является Сл9-свидетельской функцией. Покажем, что В самом деле, пусть F є (і). Тогда формула F была добавлена в () на некотором шаге к и t = tk. Индукцией по к докажем, что LP (CS) Н t:F . Пусть к — 0. Тогда to = СІ ДЛЯ некоторого номера г и 0:F С5.
Таким образом, LP(OS) Ь i0:F. Пусть А; 0 и LP(GS) h ti:G для всех формул б?, добавленных в соответствующие множества (j) на шагах г &. Докажем теперь, что LP (С5) Ь :F. Терм tk не может быть переменной или константой, так как k{h) Ф k-l{tk) Случай tk = hs. Тогда F (hs). Таким образом, существует формула G и числа г, j fc такие, что Д = U, s — tj1 формула G — F была добавлена в множество (г-) на шаге і и формула G была добавлена в множество (ij) на шаге j. Тогда LP(CS) \- ti .(G — F) и LP{CS) \- tf.G. Но LP{C$) h tf:(G F) -» fe:G -+ (Mj):F) (аксиома A2). Следовательно, LP (CIS) Ь ( i/):F, что означает LP(C!S) h ifciF. Случай tk — h + s. Тогда F Є (h + s). Следовательно, h = U или s — ti для некоторого г к и формула F была добавлена в множество (ij) на шаге г. Пусть, к примеру, h U. Это означает, что LP(CS) Ь fcF. Согласно аксиоме А4 имеем: LP(CS) Ь :F - (ii+s):F. Отсюда получаем LP(GS) Ь (f(- + s):F, то есть LP(C5) Ь tk:F. Случай tk =!Д. Тогда h = U и F — tf.G для некоторого номера г fc, а формула С была добавлена в множество (h) на шаге г. Тогда LP(C5) Ь fcG. Согласно аксиоме A3 имеем: LP(C$) Ь :F - !«:(fcF). Значит, LP(C5) r-! :( :F) и LP(C5) h tk:F. Обратная импликация имеет место для каждой С&свидетельской функции. В самом деле, рассмотрим произвольную предмодель Р = г», , f=p с данной CS-свидетельской функцией . Тогда по теореме 1.1.9, т Следствие 1.2,4 Для каждой спецификации констант CS существует предмодель Р, такая что
Доказательство. Пусть даны константная спецификация CS = {с\\ Лі,..., Сц-.Ап}. Определим предмодель Р — (v, , (=р), где сеть CS-свидетельская функция из леммы 1.2.3 и v(S) := False для каждого SzSVar. Согласно теореме 1.1.9, Обратная импликация также верна. В самом деле, если Р \=р t.A, то Ae (t) и, по лемме 1.2.3, LP(GS) Ь t.A. ш С помощью теоремы 1.1.10 утверждение следствия 1.2.4 может быть перенесено на случай рефлексивных моделей. Получающаяся таким образом рефлексивная модель оказывается наименьшим элементом в классе всех рефлексивных С&моделей. Теорема 1.2.5 Для каоюдой спецификации констант CS в классе всех рефлексивных CS-моделей существует наименьший элемент М. Для этой модели выполняется:
Сложность фрагментов логики доказательств
Лучшая известная на данный момент верхняя оценка сложности логики доказательств LP установлена в работе [12]: множество всех теорем логики доказательств LP принадлежит классу П2 полиномиальной иерархии. Тривиальная нижняя оценка вытекает из того факта, что чисто пропозициональный фрагмент LP совпадает с множеством всех тавтологий классической логики высказываний (см. [12], [3]). Таким образом, множество теорем LP является ГТ -трудным. Нетривиальной нижней оценки к моменту написания настоящей работы неизвестно. Разрешающий алгоритм из работы [12] (он совпадает с приведенным в работе [16]) может быть также применен к фрагменту RLP и даст ту же верхнюю оценку сложности. Ниже мы улучшаем верхнюю оценку для исчисления RLP до NP. Для этого предлагается новый алгоритм, основанный на поиске выводов в исчислении С. Определение 1.4.1 Пусть П — сигнатура, содержащая только функциональные символы и константы, XQ,X\,... — (новые) синтаксические переменные. (Мы используем термин "синтаксические переменные", чтобы отличить их от переменных языка логики доказательств.) Задача унификации задастся конечной системой уравнений где ЛІ,ВІ — термы сигнатуры Q с переменными из множества {XQ, Xi,...}. Решением, или унификатором системы называется такая подстановка 8, для которой Аф совпадает с В{В при всех і — 1,..., п. Система называется унифицируемой, если у нес существует унификатор. Подстановка В называется наиболее общим унификатором (и.о.у.) системы, если множество подстановок {9\ \ А — произвольная подстановка} совпадает с множеством всех унификаторов системы. Замечание. Наиболее общий унификатор существует у каждой унифицируемой системы.
Первый, экспоненциальный по времени и памяти, алгоритм построения наиболее общего унификатора был предложен в [17]. Трудоемкость вычисления в нем порождалась тем обстоятельством, что длины термов, входящих в н.о.у. системы, могут расти экспоненциально. В [7] предложено использовать экономное представление термов, при котором повторяющиеся подтермы хранятся только один раз (DAG-прсдставление). Это привело к алгоритму, который распознает унифицируемость системы и вычисляет се н.о.у, за полиномиальное время. Ниже мы используем полиномиальный алгоритм унификации из [7] для поиска выводов в исчислении С. При этом в качестве П берется сигнатура, функциональными символами которой объявляются булевы связки, символ ":" и операции !, , +, а константами — все переменные и константы языка LP. При этом все термы и формулы языка LP оказываются замкнутыми термами сигнатуры П. Теорема 1.4.2 RLP принадлежит классу сложности NP. Доказательство. Достаточно доказать, что проблема выводимости для исчисления С принадлежит классу NP. Рассмотрим дерево вывода формулы t:F в исчислении С. Заметим, что количество вершин в нем ограничено количеством подтермов в терме t. Каждое применение какого-либо правила в дереве вывода соответствует вхождению некоторого подтерма s в исходный терм t и имеет вид где различные вершины дерева соответствуют различным вхождениям подтермов в терм t. Пусть tn:Fn обозначает формулу, соответствующую вершине nENode, где Node— это множество всех вершин дерева вывода. С каждой вершиной п Є Node мы ассоциируем уравнение на синтаксические переменные Fk, &JVode, которое выражает связь между посылками и заключением используемого правила вывода: для правил СІ, С2 и СЗ, соответственно (здесь щ Є Node обозначают непосредственных предшественников вершины п). Для правила (Nee) уравнение примет следующий вид: где А является соответствующей схемой одной из аксиом А0-А4; метаперсменные схемы также включены в множество синтаксических переменных.
Пусть S обозначает множество всех таких уравнений, расширенное также уравнением где по является корнем дерева вывода. Легко видеть, что система S может быть восстановлена единственным образом по формуле t:F и дереву вывода, размеченному термами tk и схемами соответствующих правил вывода (в случае правила (Ncc) добавим схему соответствующей аксиомы АО, А1, А2, A3 или А4). Подстановка, заменяющая метаперсменные на их значения, извлеченные из формул вывода, является унификатором системы S. Формула t:F выводима в исчислении С тогда и только тогда, когда существует размеченное указанным образом дерево, для которого система уравнений S унифицируема. В самом деле, выше описано, как по выводу построить размеченное дерево и унифицируемую систему уравнений. Если же дано дерево с пометками tn, п Є Node, и унифицирующая систему S подстановка [W-n]nejVodc то это жс ДсРев0 с пометками tn:ipn, п Є Node есть дерево вывода формулы t:F. Для доказательства того, что RLP є NP, осталось установить, что суммарный размер размеченного дерева и системы S, а также время, достаточное для алгоритмической проверки унифицируемости системы S для выводимой формулы i:F, полиномиально ограничены. Пусть / — длина выводимой формулы t:F, Рассмотрим размеченное дерево и систему, построенные по ее выводу. Количество вершин и количество уравнений в системе совпадают с количеством подтермов терма t, что не превосходит I.
Длины пометок tn также не превосходит I, т.к. tn — подтерм терма t. Пометки схемами аксиом и правил вывода, а также длины всех уравнений системы, кроме (2), ограничены по длине константами. Длина уравнения (2) есть 0(1). Таким образом, количество вершин размеченного дерева, длины пометок и длина системы уравнений S для выводимой формулы t:F ограничены подходящими полиномами от се длины /. Известно (см. [7]), что задача распознавания унифицируемости системы уравнений разрешима за время, оцениваемое полиномом от длины системы. В нашем случае время, достаточное для проверки унифицируемости системы S, ограничено полиномами от /. Таким образом, проблема выводимости для исчисления С принадлежит слож-ностному классу NP. я Обозначим через RLPAjV множество всех теорем исчисления LP, построенных из квазиатомарных формул с помощью связок Л, V. Верхняя оценка сложности (NP) из теоремы 1.4.2 может быть распространена на RLPAiV с помощью следующей леммы: Лемма 1.4.3 Пусть A(Si,...,Sn) — пропозициональная формула, построенная из пропозициональных переменных Si,...,Sn с помощью связок Л, V, а формула F имеет вид A(t]_:Fi,..., tn:Fn). Тогда
Типизация подтермов
Исчисление RCL-wf допускает следующие упрощения. Лемма 2.2.1 Если суоіедение "X - п.п.ф." выводимо в исчислении RCL-wf, то оно также выводимо в RCL-wf без использования правила 11. Доказательство. Рассмотрим самый короткий вывод суждения "X - п.п.ф." и первое вхождение правила 11 в этот вывод. Его посылка UF — G - п.п.ф." может быть выведена только при помощи правила 2. Но такой вывод можно упростить следующим образом: Противоречие с минимальностью вывода. Следствие 2.2.2 Формула X — Y является правильно построенной тогда и только тогда, когда формулы X и У являются правильно построенными. Доказательство. Правильная построснность формулы вида X —» Y в исчислении RCL-wf без правила 11 может быть установлена только по правилу 2, посылками которого будут формулы X - п.п.ф. и Y - п.п.ф.. Следствие 2.2.3 При замене посылок в правилах 5 и 6 исчисления RCL-wf на "F,G - п.п.ф."и "F,G,H - п.п.ф." соответственно, множество выводимых в исчислении суждений не изменится. Доказательство. Вытекает из следствия 2.2.2. Лемма 2.2.4 Если обе формулы t: X и t :Y являются правильно построенными, то формулы X uY совпадают. Доказательство. Допустим противное. Пусть "t : X - п.п.ф." и "t: У - п.п.ф." выводятся без использования правила 11, X Y и суммарная длина I этих выводов минимальна. Заметим, что последние правила в обоих выводах должны быть одинаковы, причем это не может быть ни правило 1, ни правило 2. Если это одно из правил З, 4, 5, 6, 8 или 10, то результаты применения этих правил также должны совпадать, что противоречит условию "X ф У". Остаются два случая: Лемма 2.2.5 i?a/m t является подтермом правильно построенной формулы F, то t является типизуемым. Доказательство. Индукция по выводу формулы "F - п.п.ф.", в котором правила 5 и 6 упрощены согласно следствию 2.2.3 и правило 11 не используется.
Правила 1 и 2 не добавляют новых подтермов, поэтому утверждение следует из предположения индукции. В случае применения одного из правил 3-9 типизуемость единственного нового подтерма доказывается самим применяемым правилом. Рассмотрим случай правила 10. В заключении правила 10 появляются два новых подтерма — \t и d-\ Типизуемость первого из них следует из тех же посылок по правилу 9, а типизуемость второго подтерма устанавливается самим правилом 10. Лемма 2.2.6 Если формула % : X" правильно построена, то формула X также является правильно построенной. Доказательство. Индукция по выводу формулы " : X - п.п.ф.", в котором правило 11 не используется. Последним правилом в выводе не могут быть правила 1 и 2. В случае правил 3, 5, 6, 7 и 9 правильная построенность формулы X утверждается в посылках применяемого правила. Правило 4. Правильная построенность формулы X = (t : F — F) следует из посылок применяемого правила по правилу 2. Правило 8. Правильная построенность формулы X = (и : (F — (?) —» (v: F — (uv): G)) следует из посылок применяемого правила по правилам 7 и 2. Правило 10. Правильная построенность формулы X — (t: F — \t:(t:F)) следует из посылок применяемого правила по правилам 9 и 2. Следствие 2.2.7 В правилах 4, 7, 8, 9 и 10 исчисления RCL-wf посылки "F - п.п.ф." и "G - п.п.ф." могут быть опущены без изменения множества выводимых суждений. Доказательство.
Следует из леммы 2.2.6. Теорема 2.2.8 1. Если терм t является ассоциированным подтермом правильно построенной формулы, то он типизуем. Более того, формула G, такая что формула t : G является правильно построенной, единственна и таксисе правильно построена. 2. Каждая ассоциированная подформула правильно построенной формулы также является правильно построенной. Доказательство. 1. Пусть t является ассоциированным подтермом правильно построенной формулы F. Докажем, что і типизуем, индукцией по высоте верхнего индекса, подтермом которого является
Устранение сечения в RCLTG
В исчислении RCLTG правило сечения (Cut) устранимо. Излагаемое ниже доказательство использует основные идеи из [2], где приведено синтаксическое доказательство устранимости правила сечения для интуиционистской логики доказательств ILPG. При адаптации последнего к более сложному синтаксису исчисления RCLTG приходится преодолевать дополнительные трудности, связанные с разметкой термов типами и использованием разметки правилами RCLTG. Однако наличие этой разметки позволяет существенно упростить индукци онное доказательство за счет удачного выбора параметра индукции (ранга сечения). Используемое в [2] понятие ранга отражает не только сложность высекаемой формулы, но и положение правила в дереве вывода. В случае RCLTG оказывается возможным ограничиться числовой характеристикой, зависящей только от высекаемой формулы, что значительно упрощает получение необходимых оценок этого параметра. в секвенциальный вывод Т определим его ранг как размер высекаемой формулы ИІгіш7- Ранг вывода гк{Т ) есть максимум рангов его сечений.
Глубиной depth(V) вывода V называется высота соответствующего дерева, т.е. количество ребер в максимальном пути от корня к листьям; глубина вывода, состоящего из одной аксиомы, равна 0. Уровень данного вхождения правила сечения в вывод определяется как сумма глубин выводов его посылок. Вспомогательные факты. Лемма 3.2.2 используется в доказательстве леммы 3.2.3. Лемма 3.2.3 - центральный прием при разборе правил с термами в группе III в основной лемме 3.2.4 про устранение одного сечения. Рассмотрим выводимую секвенцию вида Г =$ F —» G. Она является заключением правила {R —»), но может быть выведена также в результате применения другого правила. Мы показываем, что ее вывод всегда можно перестроить так, чтобы последним в нем оказалось именно правило (R —»), причем ранг вывода не возрастает. Лемма 3.2.2 (Обращение правила (R —+) ) Каждый вывод V секвенции Г =5 F — G можно перестроить в вывод той же секвенции, кончающийся правилом (R —). Доказательство. Индукция по глубине вывода V. В случае depth(V) = 0 утверждение выполняется ввиду ложности посылки: секвенция рассматриваемого вида не является аксиомой и ее выводов глубины 0 не существует. Пусть depth(V) 0. Если последним правилом в выводе уже является (R —»), то перестройка не нужна. Другие варианты для последнего правила - (Cut) и правила введения слева (L ) (для них F (?B сукцеденте не является главной формулой). Случай (Cut). Первое преобразование — применение индуктивного предположения к правой посылке, второе — перестановка правил. Оба преобразования не увеличивают ранга. Для правил (L —), (LC) и (L :) также применяем индуктивное предположение к посылке правила, а затем передвигаем (R — ) вниз. Здесь в антецедент секвенции F, Г А добавился "лишний" член F. Вывод такой секвенции получается из вывода Г =$» А дописыванием F в антецеденты всех секвенций, что не меняет ранга вывода. Случай {LC).
В последних двух случаях проведенные преобразования также не увеличивают ранг вывода. м Рассмотрим теперь вывод, заканчивающийся секвенцией вида Г =$ tF:F. С помощью сечения из нее можно вывести Г = F, однако это может увеличить ранг вывода до \tF :F \dag Покажем что увеличения ранга можно избежать.Лемма 3.2.3 По выводу V без сечения секвенции Г =j tF:F можно построить вывод Т \ секвенции Г = F с рангом Доказательство. Индукция по выводу V. Если Г = tF:F - аксиома, то Г — t :F, Д и искомый вывод следующий: Теперь рассмотрим случай вывода положительной глубины. Последнее правило в выводе не может быть одним из правил (R — ) и (Cut). В случае правил (Я!) и (В, г) утверждение тривиально. Если последнее правило - одно из (L —»), (L С), (L :), то достаточно применить предположение индукции к посылке (той, что имеет вид ... = tF: і 1), а потом применить то же правило. Основной случай - правило По индуктивному предположению, секвенции V=S F- GHV= F имеют выводы требуемого ранга. Применим лемму 3.2.2 к первому из них. Получим вывод требуемого ранга, который заканчивается правилом (R — ): Искомым оказывается следующий вывод: Ранги выводов посылок меньше \tF : F\dag и 5F G : (F —» (7)1 соответственно. Ранг добавленного сечения есть \F\dag І- ІАщ- Эти три величины меньше, чем \(sF G tF)G:G\dag Устранение единственного сечения. Лемма 3.2.4 Рассмотрим заканчивающийся сечением вывод V, в котором подвыводы Т \ и Т 2 не содержат сечений. Его можно преобразовать в другой вывод V той же секвенции, для которого rk{V ) rk{V). Доказательство. Выводы V рассматриваемого вида имеют две числовые характеристики - ранг г = rk{V) = \A\dag и уровень единственного сечения I — depth(T \) + depth(T 2). Докажем утверждение леммы индукцией по следующему полному порядку на множестве всех пар натуральных чисел:
Имеются три группы преобразований выводов, которые обеспечивают шаги индукции: I. (Преобразования, удаляющие сечение.) Если хотя бы один из выводов V\ и Х 2 состоит из единственной аксиомы Р, Д =» Р, то сечение можно устранить. Если аксиомой оказывается Г = А, то поступаем так: Д, Р,Г = В (члены Д добавляются в антецеденты всех секвенций результата, что не нарушает свойства быть выводом). Если аксиомой оказывается А, Г" =- -В, то либо заключение Г, Г = В тоже аксиома, либо А = В = Р и вывод преобразуется так: Аналогично можно устранить сечение, если хотя бы один из выводов Т і и Т 2 состоит только из правил (LC), т.к. они преобразуют аксиомы в аксиомы. Их можно убрать, а затем поступить, как указано выше. Сюда же относится случай, когда последнее правило в Z 2 есть (Ri). Тогда заключение правила сечения в V может быть получено "за один шаг" также по правилу (Ri), т.е. без сечения: II. (Преобразования, понижающие уровень сечения.) Пусть теперь оба вывода T i, 2 имеют ненулевую глубину, но хотя бы в одном из них А не является главной формулой последнего правила. Исключим также рассмотренный выше случай последнего правила (Ri) в выводе Х 2. Тогда в выводе V можно передвинуть сечение вверх по выводу, что понижает его уровень и не меняет ранг, а утверждение леммы следует из предположения индукции. Понижение глубины T i. Возможные правила — все левые правила. Правило (L — ).
