5 - Генценовские формальные системы. Исчисление GV. Исчисление GP (Конспект лекций)

ÔÍ-12ÔÍ-12ÌÃÒÓМосковский государственный технический университетимени Н.Э. БауманаÌÃÒÓФакультет «Фундаментальные науки»Кафедра «Математическое моделирование»ÌÃÒÓÀ.Í. ÊàíàòíèêîâÈ ÒÅÎÐÈß ÀËÃÎÐÈÒÌÎÂÊîíñïåêò ëåêöèéÔÍ-12Москва2009ÌÃÒÓÔÍ-12ÌÃÒÓÌÃÒÓÔÍ-12ÔÍ-12Äëÿ ñòóäåíòîâ êàôåäðû ÈÓ9ÌÃÒÓÌÃÒÓÌÀÒÅÌÀÒÈ×ÅÑÊÀß ËÎÃÈÊÀÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÌÃÒÓÔÍ-121. УтончениеУ >:Γ >∆X, Γ > ∆>У:Γ >∆Γ > ∆, X2. СокращениеС >:Γ, X, X, Λ > ∆Γ, X, Λ > ∆>С:Γ > ∆, X, X, ΛΓ > ∆, X, Λ3.

ПерестановкаП >:Γ, X, Y, Λ > ∆Γ, Y, X, Λ > ∆>П:Γ > ∆, X, Y, ΛΓ > ∆, Y, X, ΛÔÍ-12ÔÍ-12и большое количество правил вывода (всего 15). Их разделим на структурные и логические.Итак структурные правила:∆ > Λ, X; X, Γ > Θ∆, Γ > Λ, Θ→ >:> →:X, Γ > ∆, YΓ > ∆, X → YX, Γ > ∆Y, Γ > ∆,X ∧ Y, Γ > ∆ X ∧ Y, Γ > ∆> ∧:Γ > ∆, X; Γ > ∆, YΓ > ∆, X ∧ Y3. Дизъюнкция∨ >:X, Γ > ∆; Y, Γ > ∆X ∨ Y, Γ > ∆> ∨:Γ > ∆, XΓ > ∆, Y,Γ > ∆, X ∨ Y Γ > ∆, X ∨ Y4. Отрицание¬ >:Γ > ∆, X¬X, Γ > ∆> ¬:X, Γ > ∆Γ > ∆, ¬XÔÍ-1254ÔÍ-122.

Конъюнкция ∧ >:∆ > Λ, X; Y, Γ > ΘX → Y, ∆, Γ > Λ, ΘÌÃÒÓЛогических правил восемь — по две на каждую логическую связку. Похоже на логическиеправила в теории N , но нет правил удаления, а есть только введение, но либо в антецеденте,либо в сукцеденте:1. ИмпликацияÌÃÒÓX >XÃÒÓÌÃÒÓДля языка исчисления высказываний построим некоторое расширение, добавив символы “,”и “ >”:1) если X и Y — формулы, то X >, > Y и X > Y — секвенции (первые две назовемоткрытыми соответственно справа и слева);2) если S — закрытая слева секвенция, X — формула, то X, S — секвенция; если S —закрытая справа секвенция, X — формула, то S, X — секвенция.Как следует из этого формального определения, секвенция — это два списка формул, соединенных специальным знаком.

При этом один из списков (но не оба вместе) может бытьпустым. Левый список называется антецедентом, а правый — сукцедентом секвенции.Далее через X, Y , . . . будем обозначать отдельные формулы, через Γ, ∆ и т.д. — спискиформул.Исчисление GV имеет только одну схему аксиомÔÍ-12ÔÍ-125.1. Исчисление GVÌÃÒÓÌÃÒÓÔÍ-12ÌÃÒÓÌÃÒÓ5.

ГЕНЦЕНОВСКИЕФОРМАЛЬНЫЕ СИСТЕМЫ3. СечениеÔÍ-12ÔÍ-12ÔÍ-12ÌÃÒÓÌÃÒÓÔÍ-12ÌÃÒÓÌÃÒÓÔÍ-12ÌÃÒÓ55Единственная схема аксиом и правила вывода позволяют получать выводимые секвенциитак же, как и в теории N или P . Как и ранее, выводом в исчислении GV называем последовательность секвенций, в которой каждая секвенция либо аксиома, либо получена на основанииодного из правил вывода. Конечная секвенция всякого вывода называется выводимой в исчислении GV . Можно также ввести понятие частного вывода. Частный вывод строится исходяиз одной или нескольких исходных секвенций, называемых гипотезами, и завершается однойрезультирующей секвенцией. Результат частного вывода можно записать в том же виде, чтои правила вывода, и в дальнейшем использовать в качестве дополнительного правила вывода.

Условие выводимости секвенции S будем записывать в виде ` S, а вывод S из гипотез S1 ,S2 , . . . , Sn — в виде S1 , S2 , . . . , Sn ` S.Пример 5.1. Построим вывод секвенции > ¬¬X → X. Имеем:> ¬¬X → X ⇐ ¬¬X > X ⇐> X, ¬X ⇐ X > X.Пример 5.2.

Построим вывод секвенции > X ∨ ¬X. Имеем:> X ∨ ¬X ⇐> X ∨ ¬X, X ∨ ¬X ⇐> X ∨ ¬X, ¬X ⇐ X > X ∨ ¬X ⇐ X > X.Пример 5.3. Построим вывод секвенции > ¬X → (X → Y ):> ¬X → (X → Y ) ⇐ ¬X > X → Y ⇐ X, ¬X > Y ⇐⇐ ¬X, X > Y ⇐ X > Y, X ⇐ X > X, Y ⇐ X > X.Γ > ∆, X,Γ > ∆, ¬¬XΓ > ∆, X, Y.Γ > ∆, X ∨ YДействительно,¬¬X, Γ > ∆ ⇐ Γ > ∆, ¬X ⇐ X, Γ > ∆ÔÍ-12X, Γ > ∆,¬¬X, Γ > ∆ÌÃÒÓСтруктурные правила сокращения и перестановки означают, что в списках формул антецедента и сукцедента порядок не важен и формулы могут повторяться, т.е. эти списки есть простоконечные множества формул, которые могут записываться в любом порядке. Мы будем этимпользоваться для сокращения деревьев вывода: соответствующие формальности всегда можновосстановить.Из рассмотренных примеров можно выделить некоторые простые правила, которые такжеможно использовать для сокращения вывода:ÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-125.

Генценовские формальныесистемы(этот прием использован в примере 5.1) иΓ > ∆, X ∨ Y ⇐ Γ > ∆, X ∨ Y, X ∨ Y ⇐ Γ > ∆, X ∨ Y, Y ⇐ Γ > ∆, X, YX > ¬¬X¬¬X, Γ > ∆Γ > ∆, X, YΓ > ∆, X ∨ YX ∨ Y > X, Y¬X, X >X > X, YY > X, YX >XX >XY >YÌÃÒÓX, Γ > ∆ÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-12ÔÍ-12(этот прием использован в примере 5.2).

Эти правила обратимы, что можно установить, используя правило сечения:ÌÃÒÓÌÃÒÓΓ > ∆, ¬¬X ⇐ ¬X, Γ > ∆ ⇐ Γ > ∆, XÌÃÒÓÌÃÒÓÌÃÒÓÔÍ-12ИУ-9, МЛТА, 2009-10уч.г.Установленные дополнительные правила показывают, что формулы можно свободно переносить из одной части секвенции в другую, навешивая знак отрицания или, наоборот, убираяего. Кроме того, из них следует, что выводимость секвенции Γ > Y1 , Y2 , . . .

, Ym эквивалентнавыводимости секвенции Γ > Y1 ∨ Y2 ∨ . . . ∨ Ym , а выводимость секвенции X1 , X2 , . . . , Xk > ∆эквивалентна выводимости X1 ∧ X2 ∧ . . . ∧ Xk > ∆. Последнее свойство аналогично следующему свойству теории N : существование частного вывода X1 , X2 , . . . , Xn ` Y равносильновыводимости формулы X1 ∧ X2 ∧ . . . ∧ Xn → Y . Это вытекает из двух правил теории N :X1 , X2 , Γ ` YX1 ∧ X2 , Γ ` YиX1 ∧ X2 , Γ ` Y.X1 , X2 , Γ ` YПервое из этих правил — правило удаления конъюнкции, а второе может быть получено изправила введения конъюнкции с помощью сечения:ÌÃÒÓÌÃÒÓÔÍ-12ÔÍ-12ÔÍ-12ÌÃÒÓ56Теорема 5.1. Если в теории N существует вывод Γ ` Y , то в теории GV существуетвывод ` (Γ > Y ).Γ >YΓ >X →YX → Y, Γ > YY >YΓ > Y, XΓ >XПравило удаления конъюнкции сводится к введению конъюнкции в антецеденте:Γ, X1 ∧ X2 > Y ⇐ Γ, X1 ∧ X2 , X1 ∧ X2 > Y ⇐ Γ, X1 , X1 ∧ X2 > Y ⇐ Γ, X1 , X2 > Y.ÔÍ-12Y, Γ > YÌÃÒÓJ Доказательство строится на том, что каждое правило естественного вывода в теории Nможно интерпретировать в рамках правил вывода теории GV , а также на том, что любой выводв теории N можно получить в рамках техники естественного вывода.

Последнее вытекает издоказательства полноты исчисления высказываний: теоремы 2.5 и 2.6 доказаны с помощьютехники естественного вывода. Остановимся на вопросе интерпретации.Закон тождества вытекает из аксиомы теории GV с учетом правила утончения. Правиладобавления, сокращения и перестановки гипотез сводятся к правилам утончения сокращенияи перестановки для антецедента в исчислении GV . Наконец, правило сечения теории N естьчастный случай правила сечения теории GV . Таким образом, все структурные правила естественного вывода теории N интерпретируются в теории GV .Правила введения импликации (теорема о дедукции), введения конъюнкции и введения дизъюнкции есть частные случаи введения соответствующего символа в сукцеденте (при ∆ = ∅).Правило удаления дизъюнкции также непосредственно сводится к введению дизъюнкции в антецеденте.

Рассмотрим остальные правила естественного вывода.Правило удаления импликации сводится к введению импликации в антеценденте:ÔÍ-12ÌÃÒÓÔÍ-12ÌÃÒÓМы видим, что вывод в технике естественного вывода в N и вывод в исчислении GV оченьпохожи. Это приводит к вопросу: как соотносятся утверждения Γ ` Y из теории N и ` (Γ > Y )из теории GV ?ÃÒÓÔÍ-12X1 , X2 ` X2ÔÍ-12ÌÃÒÓX1 , X2 ` X1Γ, X1 ∧ X2 ` YÌÃÒÓÔÍ-12X1 , X2 ` X1 ∧ X2ÔÍ-12ÔÍ-12Γ, X1 , X2 ` YÌÃÒÓÌÃÒÓΓ > ¬XX, Γ >ÌÃÒÓY, ¬Y >Γ, X > YΓ, X > ¬YY >YПравило удаления отрицания это одно из правил удаления двойного отрицания, установленныхранее.Поскольку все правила естественного вывода интерпретируемы в исчислении GV , любойвывод Γ ` Y в технике естественного вывода можно трансформировать в вывод секвенцииΓ > Y в исчислении GV . IТеорема 5.2.

Если в теории GV существует вывод ` (Γ > Y ), то в теории N существуетвывод Γ ` Y .ÌÃÒÓJ Можно предложить два подхода к доказательству теоремы. Первый основан на интерпретации правил вывода теории GV в рамках правил естественного вывода теории N , как впредшествующей теореме. Более короткий второй подход, основанный на следующих соображениях. Можно показать непосредственной проверкой, что если ` (Γ > ∆), где Γ = X1 , X2 , . .

. , Xn ,∆ = Y1 , Y2 , . . . , Ym , то формула X1 ∧ X2 ∧ . . . ∧ Xn → Y1 ∨ Y2 ∨ . . . ∨ Ym является тавтологией. Наосновании этого сразу делаем вывод, что если ` (Γ > Y ), то формула X1 ∧ X2 ∧ . . . ∧ Xn → Yвыводима в теории N , т.е. существует частный вывод Γ ` Y . Последний переход базируетсяна применении правил удаления конъюнкции и удаления импликации.

IÔÍ-12ÔÍ-12X, Γ > Y ∧ ¬YÌÃÒÓÌÃÒÓÌÃÒÓ57Рассмотрим правило введения отрицания:Y ∧ ¬Y >Еще в исчислении N было отмечено, что правило сечение является излишним и может бытьзаменено комбинацией правил введения и удаления импликации:ÔÍ-12ÔÍ-12ÔÍ-12ÔÍ-12ÔÍ-12ÌÃÒÓÔÍ-125. Генценовские формальныесистемыΓ, ∆ ` XΓ, ∆ ` YΓ, ∆ ` Y → X∆`YΓ, ∆, Y ` XÌÃÒÓÔÍ-12ÔÍ-12Γ > ∆, X, Y.Γ > ∆, X ∨ YÔÍ-12иÌÃÒÓX, Y, Γ > ∆X ∧ Y, Γ > ∆ÔÍ-12В исчислении GV нет правила modus ponens и таким способом избавиться от правиласечения не удастся. Однако генценовскому исчислению можно придать важное свойство, из которого следует, что любой вывод в этом исчислении можно строить без использования правиласечения.Генценовские правила (структурные не в счет) устроены таким образом, что при построениидерева вывода мы из невыводимой (иными словами, ложной) секвенции получаем невыводимуюсеквенцию в одной из ветвей.

Однако обратное утверждение, во всяком случае для исходныхправил, неверно: наличие невыводимой секвенции внизу дерева еще не означает, что и кореньдерева есть невыводимая секвенция. Причиной тому правила введения конъюнкции в антецеденте и дизъюнкции в сукцеденте. Но их можно усилить, заменив правиламиÌÃÒÓÌÃÒÓΓ, Y ` XÌÃÒÓ5.2. Исчисление GPГенценовское исчисление предикатов строится как расширение генценовского исчислениявысказываний.

Мы выбираем любой логико-математический язык и с помощью пары списковформул Γ и ∆ строим формулы вида Γ > ∆ называя их секвенциями. Для этих секвенцийоставляем в силе единственную схему аксиом X > X и все пятнадцать правил вывода. Крометого, добавляются еще четыре правила вывода, связанные с кванторами:∀ >:Γ > ∆, XΓ > ∆, ∀yXyx> ∀:Xtx , Γ > ∆∀xX, Γ > ∆6. Введение ∃Γ > ∆, Xtx∃ >:Γ > ∆, ∃xX> ∃:X, Γ > ∆∃yXyx , Γ > ∆Пример 5.4. Построим в GP вывод секвенции > ¬∃xY (x) → ∀x¬Y (x).

Вывод строим ввиде дерева> ¬∃xY (x) → ∀x¬Y (x)¬∃xY (x) > ∀x¬Y (x)> ∃xY (x), ¬Y (x)Y (x) > ∃xY (x)Y (x) > Y (x)ÔÍ-12ÌÃÒÓÌÃÒÓÔÍ-12ÔÍ-12> ∃xY (x), ∀x¬Y (x)ÌÃÒÓЗдесь те же ограничения, что и в исчислении P : подстановка x → t свободна для X; В формулахвведения ∀ слева и ∃ справа переменная x не имеет свободных вхождений в формулы списков Γи ∆ и если y 6= x, то y не входит свободно в X.ÔÍ-125. Введение ∀ÃÒÓÔÍ-12Теорема 5.3 (теорема Генцена об устранении сечения).