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