Диссертация (1149226), страница 16
Текст из файла (страница 16)
К полученной секвенции применяются правилаполучить правильную–секвенцию. Секвенцию,иили, чтобыможно упрощать такимобразом до тех пор, пока не получим секвенцию, которую далее невозможноупростить (такую секвенцию будем называть упрощением секвенции ).Замечание 3.1. Для исчислениясписокдлясостоит из правил вывода исчисленияправилам, перечисленным в спискеисчисления59применима аналогичная стратегия:соответствует правилодля, соответствующих. Например, правилуисчисления.Указанное исключение введено для того, чтобы к упрощенной секвенции было применимо правило, если оно было применимо к исходной секвенции.92Стратегии такого же рода существуют и для других исчислений обратногометода. Например, Т.
Таммет в статье [139] предложил стратегию, которую онназвал«reductionstrategy»,дляодносукцедентногоинтуиционистскогоисчисления обратного метода. Предложенная в настоящей работе стратегияотличается от стратегии Т. Таммета списком «упрощающих» правил: в спискедополнительно присутствует правило введения импликации в сукцедент. Также встатье Т. Таммета не приведено доказательство полноты стратегии, а тольконамечена его идея. Таким образом, рассмотрение стратегии упрощения дляисчисленияпозволяетобобщитьеенаболееширокийклассинтуиционистских исчислений.Стратегия Т.
Таммета основывается на идеях аналогичной стратегии дляклассической логики, предложенной А. Воронковым в [157]. В той же статьеА. Воронков предложил общий подход к обоснованию подобных стратегий дляразличных исчислений обратного метода. В настоящей кандидатской работеиспользуется другой подход, основанный на доказательстве теоремы оперестановочности применений правил.Основные трудности при доказательстве полноты стратегии упрощениявозникают при рассмотрении правили, из-за ограничения насобственную переменную. Эти случаи обосновываются с помощью следующихдополнительных лемм.Лемма 3.6.
Рассмотрим вывод формулысодержащий либо применение правилаиз спискадля исчисления,, либо такое применение правила, боковая формула которого не имеет вид(обозначим указанное применение каквывод входит секвенцияв исчислении). Пусть выше примененияв, к которой применимо то же правило с той жебоковой формулой (которая является предком60 боковой формулы применения ).60Формальное определение предка вхождения формулы в вывод см. в статье С. К. Клини [16].Неформально в данном выводе одно вхождение формулы называется предком другого вхождения формулы, еслипо применениям правил вывода можно «проследить» переход первого из них во второе.93Тогда вывод можно перестроить (с сохранением свойства чистотыпеременных, если оно имелось), поднимая наверх применениеего посылкой не окажется .
При этом в случае, когдаправиладо тех пор, покаявляется применением, может потребоваться удвоение применения этого правила, еслионо поднимается над применениями двухпосылочных правил.Доказательство леммы вынесено в приложение Б.Следствие. Аналогичная лемма верна для исчисления.Используем ту же идею, что и в доказательстве теоремы 3.2: переходим кисчислению, применяем лемму 3.6 и возвращаемся к исчислению.Теорема 3.3. Полнота стратегии упрощения. Стратегия упрощенияявляется полной для исчисления.Следует из теоремы 3.2 и следствия из леммы 3.6: любой вывод формулыможно перестроить так, чтобы он удовлетворял стратегии упрощения.3.5.
Стратегии удаления недопустимых секвенций3.5.1. Стратегия удаления секвенций с недопустимыми подстановкамиРассмотримстратегиюудаленияподстановками (УСНП) для исчислениясеквенцийснедопустимыми, которую можно рассматриватькак адаптированный вариант тактики удаления наборов с недопустимымисистемами зависимостей61. Эта тактика в общем виде была сформулированаС. Ю. Масловым [22]. В. П. Оревков предложил конкретизацию этой тактики вприменении к одной модификации обратного метода для классической логики[38]. Следует отметить, что полученная стратегия УСНП существенно слабееуниверсальной тактики С.
Ю. Маслова (см. [22, с. 35]), но при этом включает всебя условия допустимости (списков формул) из работы [38]. Адаптация тактикик исчислению61заключается (кроме использования другой терминологии) вВ настоящей диссертации роль систем зависимостей играют подстановки в –секвенциях.94выделении частных случаев недопустимых подстановок, для которых можнодостаточно быстро выполнить проверку на недопустимость.СтратегияУСНПдляисчислениязаключаетсявудалении–секвенций, принадлежащих одному из трех множеств секвенцийили,. Указанные множества соответствуют выделеннымчастным случаям недопустимых подстановок и определяются ниже.Будем называть переменнуюформулы , еслисвязана вположительной переменнойквантором типаили.состоит из –секвенций, содержащих такие вхожденияМножество–формули(необязательно различные) и такие различныепеременные, что,переменными формулыиМножествоитакуюявляются положительными.состоит–формулуииз–секвенций,переменнуюположительной переменной формулы , асодержащих,чтоявляетсяне является переменной, т.
е.является предметной константой или составным термом видаПустьПеременная— положительнаяпеременная.формулыназывается зависимой от переменной, еслии.не совпадает сквантор, связывающий , входит в зону действия квантора, связывающегоДля –секвенции, чтоии переменных–формулачто существуеттакуюзапись, входящая ви.означает,, и такие переменные— положительная переменная формулы ,зависима от,.состоит из –секвенций , для которых существует такая цепочкапеременных,, что.Теорема 3.4.
Полнота стратегии УСНП. Стратегия удаления секвенций снедопустимыми подстановками является полной для исчисления.95Полнота стратегии следует из двух наблюдений. Во-первых, множестваи,не содержат доказываемую секвенцию. Во-вторых, индукцией по построению вывода можно доказать, что если секвенцияпринадлежит одному из множествили,, то всякаявыводимая из нее секвенция также принадлежит одному из этих множеств.Поэтому такая секвенцияне может участвовать в выводе формулы .Например, рассмотрим подробнее случайвхождения–формулии,переменными формулыкв. Найдем такиеи такие различные переменныекоторыеявляютсяположительнымии для которых выполняется равенство.
Еслиприменяется правило сокращения, то вхождениям –формул–секвенциюисоответствуют (возможно, совпадающие) вхожденияив заключение. При этом для переменныхвыполняется равенствомножествуив–формулпо-прежнему, поэтому заключение также принадлежит. Это верно и для остальных правил вывода, кроме случаевприменения правила введения квантора всеобщности в сукцедент или правилавведения квантора существования в антецедент, когда собственная переменнаясовпадает сили.
Однако указанные случаи невозможны из-за того, что невыполняется ограничение на собственную переменную.3.5.2. Стратегия удаления секвенций с недопустимыми формуламиВхождение подформулыв формулубудем называть строгоположительным62, если оно является положительным вхождением ви непринадлежит никакому отрицательному вхождению подформулы в .Пустьи— вхождения подформул вкритическим образом принадлежит62. Будем говорить, что, и писать, еслиДанный термин соответствует понятию «существенно положительное вхождение» из статьи [39].и96существует такое положительное вхождение подформулывидили,Пустьи, при этомиимеет.— вхождения подформул в . Общей надформулойбудем называть такое вхождение подформулыБлижайшей общей надформулойнадформулув , чтоии.ибудем называть такую общую, обозначаемую как, которая принадлежитлюбой другой общей надформулеРассмотримв , чтоиистратегию.удаленияформулами (УСНФ) для исчислениясеквенцийснедопустимыми, которая заключается в удалении–секвенций, принадлежащих любому из множеств.
Сами,эти множества определяются ниже.— –секвенция.Пустьииз , что, если найдется такая пара –формул(в частности, вхождениеявляется строго положительным вхождением вне совпадает с),и выполняется хотябы одно из условий:1.имеет види совпадает симеет вид,, при этомили.2.,иявляется строгоположительным вхождением в .не имеет вид3., при этом либо, либо.За формулировкой множестваформулыивыводимая изобеих –формулскрывается следующая идея: еслиудовлетворяют одному из трех условий, то любая секвенция,, обязательно содержит несовпадающие вхождения потомкови, причем для этих потомков также выполняетсяодно из условий 1–3.
Поэтому секвенции, принадлежащие множествуне могут участвовать в выводе формулы .,97Пустьи— вхождения подформул в . Будем говорить, чтокритическим образом принадлежит, и писатьположительное вхождение подформулы, если существует такоев , чтои при этом,не существует такого отрицательного вхождения подформулыисильнов , что.Множествоопределяется следующим образом. Пусть–секвенция., если найдется такая пара –формулвходящих в сукцедент , что для всехвыполняетсяодного.выполняетсяМножествои,и хотя бы дляосновывается на тех же идеях, что иэтом для множества. Присущественно, чтобыбыло строгоположительным вхождением подформулы в , а для множестваограничения нет. Множестваитакогочастично пересекаются.Для наглядности рассмотрим пример.
Пусть–секвенция.обозначения:,и.,. А так какПустьиВведем. ТогдаЗначит,—, то такжетеперь.и.Заметим, что этот пример отличается от предыдущего только наличием двойногоотрицания в формуле . В этом случаевхождение подформулы, новуже, так какне являетсястрогоположительным.Лемма 3.7. Если секвенция принадлежит множеству(),то всякая выводимая из нее секвенция также принадлежит множеству(соответственно).Доказательство леммы вынесено в приложение Б.Теорема 3.5. Полнота стратегии УСНФ.
Стратегия удаления секвенций снедопустимыми формулами является полной для исчисления.98Множестваине содержат доказываемую секвенцию. Поэтому из леммы 3.7 следует, что если секвенция S принадлежитмножеству, то никакая выводимая из нее секвенция неможет совпадать с доказываемой секвенцией.Замечание 3.2. Стратегия УСНФ также применима к исчислениюработы [68]. При этом множестводля исчисленияизявляется пустым,поскольку выводимые в этом исчислении секвенции содержат не более однойформулы в сукцеденте. Доказательство полноты этой стратегии длянесущественно отличается от доказательства теоремы 3.5.Идея стратегии УСНФ схожа с идеей стратегии «nesting strategy» дляодносукцедентного интуиционистского исчисления GJm, приведенной (бездоказательства)вработеТ.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
