Колмогоров, Драгалин - Введение в математическую логику (947386), страница 19
Текст из файла (страница 19)
При этом, конечно, н которые формулы Г могут и не быть гипотезами Р. Мы г ворим,~что вывод Р формулы А не зависит от таких чл ' нов Г. Список Г может быть и пуст. Тогда Г ~-А означает, ч существует вывод А без гипотез; мы пишем в этом случа ь-А и говорим, что формула А выводима в исчислении пре-' дикатов. Саму фигуру Г)- А мы будем называть иногда выводи мастью (или, в другой терминологии, секвенцией). Таки образом, чтобы обосновать секвенцмю Г~- А, следует построить вывод в исчислении предикатов с нижней формулой А' все гипотезы которого находятся среди членов списка Г. 3. Следующая лемма описывает семантические свойств выводимости. Лемма.
Пусть Г~-А, где Г есть список формул В„...,' В . Пусть М вЂ” интерпретация языка ьг и 8 — оценка для' Вь ..., В А. Тогда если М~ В18, ... М)==В 8, то М(=А8. (> Доказательство проведем индукцией по высоте вывода для Гь- А. Если -этот вывод состоит из единственной форму лы А, то А — либо гипотеза (и, следовательно, член Г), либо аксиома исчисления предикатов.
Если А — гипотеза, т. е. одна из формул Вь то М)==А8 ввиду М~В,О. Если А: аксиома, то М~ А8, так как А — логический закон. Если А в. выводе получена по модус поненс, то М)==А8-' следует из индуктивного предположения и того, что это пра-, вило сохраняет истинность формул при фиксированной оценке. Пусть А имеет вид у'хС и получена в выводе нз форму-' лы С по правилу обобщения.
Таким образом С выведена с помощью вывода меньшей высоты, чем вывод у' хС,' поэтому к выводу С можно применить индуктивное предпо-' ложение. По структурному требованию х не есть параметр гипотез вывода формулы С. Чтобы показать М)=(у' хС)8, достаточно установить, что для произвольного объекта а имеем М)= (С, )8. Так как всякая гипотеза В; вывода дл : С не содержит свободно х„то из М~ ВВ следует М)=' (В;, )8.
По индуктивному предположению отсюда Мг-.и' (С «)8.С) С лед с та и е. Если Г~- А и'все члены Г суть логические:. законы, то А — также логический закон. В частности, если 1- А, то А — логический закон. 98 Таким образом, на внводнмость в исчислении преднкатов можно смотреть, как на некоторый инструмент для получения логических законов, 4. Рассмотрим примеры выводов в исчислении предикатов. Для удобства выводы записываем в вндестолбцов формул, а не деревьев.
1) ~ А'=»А. В самом деле, можно построить следующий вывод: 1. А=э.(А=»А)~А, ' это пример схемы аксиом 1) п. 1; 2. (А~. (А=»А) =»А) ~ ((А=э'.А=»А) =».А~А), это пример схемы аксиом 2); 3. (А=»,А~А)'-з(А~А), получается по «модус поненс» нз 1 н 2;. 4. А=».А=»А, это пример схемы аксиом 1); 5. А=»А получается нз 3 н 4 по модус поненс. 2) Пусть А — формула, х н у — ' различные переменные, причем у не .входят свободно в А, Тогда )- 11'хА:э ~~1 у(А (х|~у)). В более традиционной (но менее точной) записи это высказывание имеет внд ' 'у'хА (х) ~ ~ууА (у). Действительно, строим вывод 1. ~ хА (х):»А (у), это пример схемы аксиом 11) п. 1; 2. ~1у( ~1хА(х) ~А(у) ) по правилу обобщения нз 1, структурное требование выпол- няется, так как 1 — не гцпотеза (а аксиома исчисления пре- днкатов); 3.
11у( у'хА(х) =»А(у).)~. '11хА(х):э'(1уА(у), ' это пример схемы аксиом 12) (существенно, что )1 хА(х) не содержит свободно у); 4. у'хА (х) =э 'руА (у) вытекает нз 2 н 3 по модус поненс. Упражне'нне. Установите в тех же условиях, что н во втором примере, что ~-. 3 у (А (х1~ у) ) =з ~хА. $2. ТЕОРЕМА О ДЕДУКЦИИ. ТЕХНИКА ЕСТЕСТВЕННОГО ВЫВОДА 1. Непосредственно 'испольэовать выводы в исчислении предикатов для установления логических законов крайне неудобно. Выводы даже простых формул получаются очень громоздкими, а главное, весьма непохожими на обычные способы рассуждения, употребляемые математиками: Поэтому понятие вывода в исчислении предикатов, как мы его сформулировали в п.
1, испоЛьзуется главным образом в теоретических исследованиях, где существенно, чтобы выводы имели простую структуру. Практически же выводимость формул и секвенций устанавливается с помощью серии специально подобранных допустимых вспомогательных правил вывода, относящихся непосредственно к секвенциям. С их помощью мы можем установить, что секвенция выводима, не строя для нее вывод в исчислении предикатов. Указанные. правила уже близко соответствуют обычной практике математического рассуждения, что сильно облегчает доказательство выводимости. Набор этих правил и называется техникой естественного вы; вода. 2. Ключевым фактом здесь является так называемая теорема о дедукции. Теорема. Если Г, А 1-В, то Г 1-А:эВ.
Этот факт записывается в виде вспомогательного правила вывода: Г,АРВ Гь А~В (> Воспользуемся индукцией по высоте вывода для Г, А 1- В. Если этот вывод состоит из единственной гипотезы В, то возможны два случая: В равно А или В есть член Г. В первом случае Г 1- А~В следует из 1-А~А. Если В есть член Г, то Г1- В. Кроме того, очевидно 1- В~.А:эВ (зто пример схемы аксиом исчисления преднкатов). С помощью модус поненс отсюда получается, что Г 1- А=эВ. Если В есть аксиома исчисления предикатов, то иэ 1- В:з.
А':зВ вновь получим 1- А:эВ и, значит, Г1- А~В. Теперь рассмотрим случай, когда В получена иэ Г, А 1-С н Г, А 1- С:>В по правилу модус поненс. По индуктивному предположению тогда .Г 1- А~С и Г 1- А=э.С~Я Далее, имеем 1- (А:э. С':зВ) ~.
(А:зС) ~(А~В) (это пример схемы аксиом 2 исчисления предикатов). Дваж'- ды применяя модус поненс, получим Г 1-А~В. Пусть теперь формула В имеет вид у'хС и получена из формулы С по правилу обобщения. Таким образом, Г,А 1-С. 100 Если вывод для Г, А) — С не зависит от А, то Г!- С. По правилу обобщения в этом случае Г !-17' хС. Кроме того, очевидно, Г ! !!асс схС». А» ~/ хС (это пример схемы 1). По модус по-. =- ненс отсюда Г 1- А» 'рхС, Если же А есть гипотеза вывода для Г, А 1- С, то по структупному требованию А не содержит свободно л.
Пусть Г| есть часть списка Г, состоящая нз всех гипотез вывода для Г, А!- С, отличных от А. Нн один член Г1 не содержит х свободно (по структурному требованию) и Гь А1- С. По индуктивному предположению Г~ 1-А»С. Далее, по правилу обобщения Г1 !-'у'х(А»С). Далее, Г1 ! — 'дх(А»С)». А» 'у'хС (ато пример схемы аксиом 12)). По модус поненс отсюда Г~ 1-. А»р'хС, н, следовательно, добавляя формулы, от которых вывод не зависит (а онн могут н содержать х.свободно!), получим Г1- А»'р'хС. П Теорема о дедукции показйвает, что для установления имплнкации Г1- А»В достаточно показать Г, А!- В, что часто бывает гораздо проще. В математической практике этому соответствует следующий пример рассуждения.
Если нужно в некоторой ситуации установить, что А»В, то долу- стим (введем гипотезу), что А верно, н докажем В, исходя нз этой гипотезы. 3. Следующие правила называются структурными правилами техники естественного вывода; 1) закон тождества А! — А; 2) правило добавления г,в г.в в' 3 правило перестановки Г, В, С, Ь ь А Г, С, В, Ь А 4) правило сокращения Г, В,В, Ь>-А Г,В, Ь-А Б) правило сечения Г!-.А; Ь, А>В Г, Ь;--С Правила 2) — 5) следует понимать как допустимые правила вывода.
Это означает, что если дан вывод для секвенций, !О! 1) Импликация: введение удаление Г,АьВ, Г~ — Л;ГьЛ~В ГьА~В ,ГьВ 2) Конъюнкция: удаление Г, А, В ~-',С ' введение Г Я;Г 8 Г~- ЛЛВ Г, АДВ1 — С 3) Дизъюнкция: введение , удаление Гьл. 1Г~ — В „Г,АьС; Г,ВмС Г~-А~)(В ' Г~-А)(В Г, А)~ В~-С 4) Отрицание: введение удаление Г,А~-В; Г,А~- ЧВ. ' Г~ — 1 1А Гь 1А ГьА 1ОЗ расположенных выше черты, то можно построить вывод н для секвенции, расположенной ниже черты. [> 1) Из гипотезы А и ввиду 1- А=зА (п.
4 $1) по 'модус поненс А )-А. 2) — 4). Тривиально допустимы. Вывод, обоснорывающий секвенцию выше черты, обосновывает и секвенцию ниже черты. 5) Из а, А 1- В по теореме о дедукции й1- А~В. Отсюда и .из Г1- А но правилу добавления Г, А~-А=зВ,: Г, Ь1- А..
Применяя модус поненс, получим Г,а 1- В. П В технике естественного вывода доказанные правила широко употребляются без явного упоминания. 4. Следующую группу образуют логические правила техники естественного вывода. Правила эти разбиваются на группы: для каждой логической связки и квантора — своя группа правил, Кроме того, внутри группы правила делится на два вида: правила введения, указывающие, как доказывать формулу с данным логическим символом, и правила удаления, указывающие, как использовать формулу с дан- ' ным логическим символом для доказательства других формул.
5) Общность: введение Г ь А(у) Г ь )(кА(к) (здерь у не входит свободно в Г, и если х отлично от у, го х не входит свободно в А (ф); удаление Г~ — укА Г ь А(к)1) б) Существование: удаление Г, А(у)ьС Г, ДкА(к) ь С (здесь у не входит свободно в Г и С, и если х отлично от у, то х не входит свободно в А (у), А (х) есть А (у( х)).
внеденне Г 1- А (к ) 1) Г ь зкА 7) Эквивалентность: введение удаление Г, А ь В; Г, В ~ — А Г ь А; Г 1- А кк В . ГьАккВ Г| — В Г, В; Г ~ — А =и В Г~ — А ~ Рассмотрим некоторые из правил. Доказательство допустимости остальных правил предоставляется читателю. ~-введение. Это есть в точности теорема о дедукции. ~-удаление.
Из данных выводов Г)-А, Г,)- А~В вывод для Г 1- В получим с помощью модус поненс. ~/-введение. Имеем: Г)-А. Кроме того, 1- А=зА~/В (это аксиома). По модус поненс Г)- АЧВ. ~/-удаление. Из данных Г, А)-С; Г, В 1- С по теореме о 'дедукции Г 1- А=эС и Г 1- В=зС. Кроме того, 1- (А=зС)=з. (В~С)~(А~/В=эС) (это аксиома). Дважды применяя модус поненс, получаем; Г(- А~/В~С. По,закону тождества (н правилу добавления) Г, А~/В 1- А~/В.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
