Диссертация (1149226), страница 17
Текст из файла (страница 17)
Таммета[139].ОднакостратегияУСНФпредставляется существенно более сильной. В терминах настоящей работыстратегия Т. Таммета позволяет удалять секвенции, содержащие формулы,соответствующие таким вхождениям подформулистрого положительным вхождением подформулы вив , что63является. Заметим, что вслучае односукцедентного исчисления из вышеприведенных условий следует, чтоявляется отрицательным вхождением подформулы в, поэтому.Таким образом, при рассмотрении сингулярных секвенций стратегия Т. Таммета64покрывает условие 1 из определения множестваслучай условия 3, когда63.В формулировке «nesting strategy» из статьи [139], судя по всему, есть опечатка: меткесоответствовать подформула64совпадает с, а также частный, а не.Следует уточнить, что в условии 1 из определения множестваболее сильное ограничение «должнаили», чем ограничение «все же используется несколькоили», соответствующеестратегии Т.
Таммета. Это связано с различиями между исчислением GJm из [139] и исчислениямичастности, исчисление GJm отличается одним из правил введения импликации в сукцедент.и.В993.6. Стратегия тривиального сокращенияТривиальным сокращением –секвенциитакая правильная –секвенция, чтоив исчисленииназываетсявыводима изправила сокращения с последующим применением правилприменениемиСтратегия тривиального сокращения для исчисленияпроцессе поиска вывода получена такая секвенциятривиальное сокращение, то секвенцию.: если в, для которой существуетможно заменить секвенцией.Приведенную стратегию можно считать аналогом тактики перехода ктривиальным спецификациям [20, с. 24], учитывая, что понятия поглощения итривиального сокращения по смыслу схожи с понятиями поднаборности итривиальной склейки (частный случай тривиальной спецификации) из статьиС.
Ю. Маслова65.Теорема 3.6. Полнота стратегии тривиального сокращения. Стратегиятривиального сокращения является полной для исчисления.Следует из определения тривиального сокращения и полноты стратегиипоглощения (теорема 3.1).3.7. Сингулярная стратегияИз любого вывода в исчисленииможно получить вывод в исчислении, заменив в исходном выводе каждое применение правиласледующим выводом в исчислении65:В указанной статье С. Ю.
Маслова тактика перехода к тривиальным спецификациям предложена вприменении к классической логике.100где,.При этом за счет использования только сингулярных секвенций размерпространства поиска вывода в исчисленииисчисленииможет быть меньше, чем в. Поэтому в качестве самостоятельной стратегии для исчисленияможно рассматривать поиск вывода формулыв исчисленииспоследующим преобразованием полученного вывода к выводу в исчислении. Такую стратегию назовем сингулярной стратегией.Теорема 3.7.
Полнота сингулярной стратегии. Сингулярная стратегияявляется полной для исчисления.Следует из равнообъемности исчисленийиисчислению предикатов Гейтинга. Для исчисленияинтуиционистскомуэто следует из теоремы2.4 и результата, полученного А. Г. Драгалиным [10]. Для исчисленияэтоследует из результатов, полученных А. Дегтяревым и А.
Воронковым [68],С. К. Клини [13] и Г. Генценом [5]66.3.8. Совместимость стратегийЗамечание 3.3. Все стратегии, рассмотренные в параграфах 3.3 — 3.6,также применимы к исчислениюА. Дегтярева и А. Воронкова [68]. При этомвсе определения, формулировки лемм и теорем непосредственно переносятся наслучай исчисления, а доказательства полноты стратегий отличаютсянесущественным образом (см. также замечания 3.1 и 3.2 о стратегии упрощения и66В работе [68] доказана равнообъемность исчисленияи исчисления G3 С. К. Клини.
В книге [13]доказана эквивалентность исчислений G3 и G1, последнее из которых по существу эквивалентно исчислению LJ[13, с. 496]. В работе [5] доказана равнообъемность исчисления LJ исчислению LHJ, которое эквивалентноисчислению Гейтинга [5, с. 62].101стратегииУСНФ).Такжеследуетотметить,чтостратегии,схожиесрассмотренными в этой главе стратегиями поглощения и упрощения, былиобоснованы Т. Тамметом [139] для исчисления GJm, близкого к исчислению.Замечание 3.4. При использовании стратегии поглощения совместно состратегией упрощения следует рассмотреть новое отношениевыполняется для –секвенцийсовпадает ситогда и только тогда, когда, которое, гдеили является ее упрощением. При этом следует скорректироватьпонятие допустимости процедуры поиска вывода, лемму 3.3 и теорему 3.1 изпараграфа 3.3: заменить отношениеотношением, а вместо простойвыводимости доказывать выводимость в соответствии со стратегией упрощения.В результате доказательство нового утверждения, полученного из леммы 3.3,будет отличаться несущественно, если учесть следующие наблюдения.
Вопервых, еслиупрощением,–секвенцией иявляется правильной, то либо, либо из секвенцииупрощений вывести такую секвенцию, чтоявляетсяможно только с помощью. Во-вторых, в определенииотношения поглощения для исчисленияв пункт 1.б можно добавитьусловие, что если правило, товходит в списокявляется применениемтого же правила. При этом лемма 3.2 по-прежнему будет выполняться (вчастности, случаи 4 и 5 из доказательства леммы это подтверждают).Учитываявышеприведенныезамечания,можносформулироватьследующую теорему о совместимости стратегий поиска вывода в предположении,что используемая процедура поиска вывода допустима.Теорема 3.8. Совместимость стратегий. Любая комбинация стратегийпоглощения, упрощения, УСНП, УСНФ и тривиального сокращения являетсяполной для исчисленийи.Из теорем 3.1, 3.3, 3.4, 3.5 и 3.6 следует, что каждая из перечисленныхстратегий является полной для исчислениядоказательствосоответствующихутверждений.
Для исчисленияотличаетсянесущественно.102Стратегии УСНП и УСНФ совместимы с другими стратегиями, так как при ихиспользовании удаляются только такие секвенции, которые не могут участвоватьв выводе формулыили. Кроме того, если секвенцияпринадлежит множеству, то любая поглощаемая ею секвенция также принадлежитодному из этих множеств. Аналогично для множестви,. Тривиальное сокращение представляет собой частный случайприменения стратегии поглощения. Из теоремы 3.3 и рассуждений, приведенныхв замечании 3.4, следует, что стратегии поглощения и упрощения такжесовместимы.Следствие.
Сингулярная стратегия совместно с любой комбинациейстратегий для исчисленияисчисления.Пусть формулачто, перечисленных в теореме 3.8, является полной длявыводима в исчислениитакже выводима в исчислениивыводима в исчислении. Из теоремы 3.7 следует,. Отсюда по теореме 3.8 формулас любой комбинацией стратегий.Пусть имеется доказательство формулыв исчислениис применениемнекоторой комбинации стратегий. Из этого доказательства можно получитьдоказательство в исчисленииследующим образом.
Сначала восстановим всепромежуточные применения правил, которые были вычеркнуты в соответствии состратегиями упрощения и тривиального сокращения. Затем преобразуемполученную фигуру к выводу в, как было показано в параграфе 3.7.3.9. Применение стратегий к модификациям исчисленийСтратегии, рассмотренные в параграфах 3.3 — 3.7, непосредственноприменимы к исчислениями(см. параграф 2.8), если во всехформулировках, названиях исчислений и терминах заменить формулуформулой103, а также убрать из формулировок упоминания связкии соответствующихправил введения .Например, списоквывода:,для исчисления,,случае, если формула,состоит из следующих правил,и,, а такжевне содержит отрицательных вхождений символа .Определение критической принадлежности вхождений подформул (пункт3.5.2) переформулируется для исчисленийкритическим образом принадлежити), если(такое положительное вхождение подформулыили, при этомВсеисчисленийирассмотренные,,в , чтои существуетимеет вид.стратегиииследующим образом.такжеприменимыкмодификациямдля вывода формул логики высказываний.
Приэтом стратегия УСНП никогда не срабатывает, а стратегия тривиальногосокращения срабатывает всегда, так как в случае логики высказываний всеподстановки в –секвенциях (–секвенциях) являются пустыми.3.10. ПримерыПоясним принцип действия рассмотренных в этой главе стратегий нанаглядных примерах. Выводы могут приводиться в линейном виде (в виде спискасеквенций) или в виде дерева. В линейной записи справа от каждой секвенции вквадратных скобках указано имя аксиомы или правила, которое применяется длявывода секвенции.
После имени правила вывода указаны номера секвенцийпосылок.Правилапереименованияинормализацииприменяютсяпринеобходимости, их применения явно не приводятся.Пример 3.1. Рассмотрим формулуЧерта над одним из предикатоввыводах..указана для удобства, чтобы отличать их в104Формулавыводима в исчислении. Рассмотрим ее вывод (построениетаблицы вхождений подформул и их полярностей здесь опускаем, подробнее этотэтап был рассмотрен в примере 2.1), совпадающий с выводом в исчислениисточностью до имен правил вывода. Фигурирующая в выводе переменнаяявляется новой переменной.1..2..3..4..5..Тот же вывод в форме дерева выглядит следующим образом:Кроме приведенных пяти секвенций, мы могли бы также вывести и другиесеквенции.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
