<<
>>

Глава 8. Теория доказательства:пропозициональные правила

1. После проделанной подготовительной работы мы можем теперь перейти к изучению строения рассуждений, что и является главной задачей нашего курса. В этой и следующих трех главах мы будем заниматься так называемыми дедуктивными рассуждениями, состоящими в том, что из некоторых явно и четко сформулированных утверждений (называемых обычно посылками) выводятся другие так же четко сформулированные утверждения (следствия), причем вывод абсолютно достоверен в том смысле, что если мы уверены в истинности посылок, то мы в такой же степени можем быть уверены в истинности следствий.

Наиболее чистым примером дедуктивных рассуждений могут служить математические доказательства.

Но сфера их использования далеко не исчерпывается математикой, хотя она и является единственной наукой, в которой только за такими рассуждениями признается доказательная сила. Дедуктивные рассуждения составляют неотъемлемую часть любых рассуждений, используемых в науках (как естественных, так и гуманитарных) и в практической деятельности. О том, каким образом дедуктивные рассуждения «вписываются» в рассуждения более общего вида, пойдет речь в главах 13 и 14; а сейчас нам надлежит изучить их строение.

Первая теория, имеющая целью описание строения дедуктивных рассуждений, была построена еще Аристотелем. (Мы познакомимся с ней в главе 11.) В течение многих веков считалось, что эта теория исчерпывающим образом описывает вообще любые рассуждения; недостаточность

дедуктивных рассуждений была замечена лишь в Новое время, приблизительно в конце XVI—начале XVII в. (см. ниже главу 12). Вскоре ученые начали осознавать и недостаточность аристотелевской теории для описания самих дедуктивных рассуждений. Великий философ и математик Г.В.Лейбниц (Gottfried Wilhelm Leibniz, 1646—1716) выдвинул идею построения «универсальной характеристики» (Characteristica universalis) — математизированной логической системы, которая могла бы служить не только для теоретического описания рассуждений, но и для их практического выполнения.

Эта система должна была состоять из знаков, соответствующих мыслям, и правил оперирования с этими знаками, построенных таким образом, что всякий раз, когда некоторая мысль является следствием другой, знак первой получается из знака второй по этим правилам. Лейбниц мечтал о времени, когда философы вместо того, чтобы спорить, будут говорить: «Посчитаем!»

Сам Лейбниц не построил развернутой формально-логической системы, но под его влиянием мысль ученых начала работать в этом направлении. Первым серьезным успехом на этом пути было создание «алгебры логики», т.е. пропозициональной части символического языка, рассмотренного нами в главе 5. Основные идеи, которые легли в основу алгебры логики, впервые появились в опубликованных в 1847 г. работах А. де Моргана и Дж. Буля и были развиты рядом других исследователей в течение второй половины XIX в. А в 1879 г. вышла книга Г. Фреге (Gottlob Frege, 1848—1925) «Begriffsschrift» («Понятийная письменность») с подзаголовком «Формульный язык чистого мышления, построенный по образцу арифметического», где впервые была построена формальная логическая система, в которой не только предложения представляются в виде формул, подобно математическим выражениям, но и правила вывода следствий из посылок представляются в виде формальных операций, подобных математическим. Впоследствии такие системы стали называть логическими исчислениями. Однако формализованный процесс вывода в исчислении Фреге и во всех других логических исчислениях, предлагавшихся разными авторами на протяжении нескольких последующих десятилетий, был мало похож на то, как на самом деле рассуждает человек даже в тех случаях, когда он проводит совершенно строгое доказательство — например, математическое. И только в 30-х гг. XX столетия Г. Генцен (Gerhard Gentzen, 1909—1945) построил исчисление естественного

вывода, дающее строгое описание реального процесса дедуктивного рассуждения—иначе говоря, процесса доказательства. В математической логике исчисления «до-генценовского» типа широко используются и в настоящее время, т.к.

в чисто техническом аспекте они обладают некоторыми преимуществами. Но теорию доказательства как таковую принято излагать либо на основе исчисления естественного вывода, либо на основе другого построенного Генценом исчисления — секвенциального, так же хорошо (хотя и «менее непосредственно») описывающего реальный процесс рассуждения. Мы будем вести изложение на основе исчисления естественного вывода.

В заключение этого краткого исторического обзора необходимо заметить, что развитие математической логики, создатели которой в значительной мере вдохновлялись идеями Лейбница, не оправдало его надежд на замену рассуждений вычислениями. Прежде всего, не все рассуждения сводятся к дедуктивным (см. ниже, часть IV), а формализации и «математизации» поддаются только эти последние. Кроме того, дедуктивные рассуждения тоже не могут быть формализованы полностью: доказано, что даже в арифметике натуральных чисел можно сформулировать утверждения, являющиеся истинными, причем истинность их можно установить с помощью рассуждений, которые всякий математик должен признать настоящими доказательствами, но при этом такие, что ни в каком сколько-нибудь «разумном» логическом исчислении невозможен их формальный вывод из аксиом арифметики. И, наконец, формальные выводы чрезвычайно громоздки, и поэтому даже в тех пределах, в которых формализация рассуждений возможна, она до сих пор остается —и, будем надеяться, останется дальше — только средством (хотя и важнейшим!) их теоретического изучения, а практически рассуждать каждый должен по-прежнему исключительно с помощью собственной головы.

2. В исчислении естественного вывода — как и во всяком логическом исчислении — основную роль играет отношение выводимости. Область отправления этого отношения состоит из конечных множеств формул

(т.е. предложений), а область прибытия — просто из формул. Выражение «Формула у выводима из множества формул М» означает, что если все формулы, входящие в М (посылки), истинны, то формула у также истинна, причем —и это здесь самое главное! —ее истинность можно вывести из истинности посылок по правилам исчисления (которые будут рассмотрены ниже).

Вместо «Формула у выводима из множества формул М» мы часто будем писать символически М h у.

М

а, |3, мы будем говорить просто «Формула у выводима из формулы а», соответственно «из формул а, |3» и писать a h у, соответственно а, р h у.

М

М

0 h у будем писать просто h у. Содержательно выводимость формулы из пустого множества означает, что она истинна и при этом ее истинность может быть доказана по правилам исчисления (без каких бы то ни было посылок). Формулы, выводимые из пустого множества, мы будем называть доказуемыми.

В этой и следующей главах мы будем рассматривать только «пропозициональную часть» исчисления естественного вывода, не затрагивая те его правила, которые связаны с кванторами. (Рассмотрение этих правил мы отложим до главы 10.) Поэтому слово «формула» будет здесь означать формулу логики предложений. Но теперь мы будем рассматривать формулы, которые наряду с пропозициональными переменными могут содержать также логическую константу Л, означающую «ложь» — подобно тому, как формулы элементарной алгебры наряду с переменными могут содержать символы постоянных чисел—1, 2, %/2

и т.п. (Можно было бы допустить также константу И, но технически

В дальнейшем мы будем обозначать формулы строчными греческими буквами, причем такая буква всегда будет означать произвольную формулу.

Главную часть системы правил исчисления естественного вывода со-ставляют правила введения и удаления логических символов. Каждой из шести рассмотренных нами в главе 5 логических операций отвечают два правила — правило введения и правило удаления символа этой операции. В настоящей главе мы будем иметь дело только с правилами, отвечающими пропозициональным связкам.

Правила введения и удаления нам будет удобно расположить в два столбца:

а, Р ha&р 2) а&р h а

(введение конъюнкции); а&р hp

(удаление конъюнкции);

h V И, h И, h

h V И, V h

(введение дизъюнкции); (удаление дизъюнкции);

И, h И h — , — h

(введение импликации); (удаление импликации);

7) Если И, а h Л, то И h —а 8) а, —ah Л

(введение отрицания); (удаление отрицания).

Сокращенно эти правила будут обозначаться ВК, УК, ВД, УД, ВИ, УИ, ВО, УО.

Кроме правил введения и удаления, исчисление содержит три особых правила:

h

10) h aV—a (закон исключенного третьего, сокращенно ИТ);

Если р є И, но И hp (правило тривиальной выводимости, сокращенно ТВ).

,,

формулы, все правила останутся справедливыми, если заменить эти буквы любыми другими буквами и вообще любыми формулами.

Например, каждая из следующих выводимое! ей получается по правилу ВД: yhSVy; сг&р ha & р V у; a h a V a. To же верно и для всех выводи- мостей, доказываемых ниже.

Поясним теперь содержательный смысл сформулированных правил. Как уже было сказано, по этим правилам производятся мельчайшие «элементарные шаги» дедуктивного рассуждения.

Первые три правила, а также пятое и шестое, настолько просты, что, пользуясь ими, мы этого практически никогда не замечаем: доказав два утверждения А и Б, мы делаем из этого вывод, что истинно также утверждение «А и Б» (введение конъюнкции); обратно, если доказано A Б A

Б

но из утверждений А, Б, отсюда выводится истинность утверждения A Б A Б

считается доказанным условное утверждение «Если А, то Б» (введение импликации); обратно, из истинности условного утверждения и его посылки выводится истинность заключения (удаление импликации).*'

Удаление дизъюнкции — это прием, известный под названием «доказательство разбором случаев»: если в какой-то ситуации (описываемой множеством предложений М) возможны два случая А ж Б (не обязательно взаимоисключающие), и в каждом из этих случаев удается доказать утверждение C, то это утверждение можно считать вообще доказанным для данной ситуации. Например, если мы доказали, что все целые числа, большие или равные нулю, обладают некоторым свойством, а затем доказали также, что этим свойством обладают все целые числа, меньшие или равные нулю, то мы можем считать доказанным, что данным свойством обладают вообще все целые числа.

Введение отрицания — это тот прием доказательства, который в старых учебниках математики назывался приведением к нелепости (поМ

утверждение А истинно, мы приходим к заведомо ложному выводу,

М

А

используется не только в математике, но и в других науках (подробнее об этом см. ниже, в главе 13), а также и в обыденной жизни. Если, на-пример, мне говорят: «Сегодня ночью был дождь», а я отвечаю: «Тогда земля была бы мокрая, но посмотри —она сухая, значит, дождя не было», я пользуюсь приведением к нелепости.

Предостережение.

Приведение к нелепости не следует смешивать с доказательством от противного, представляющим собой более

сложный способ рассуждения. (О нем мы мы будем говорить в следующей главе.)

Удаление отрицания — это не что иное, как закон противоречия, о котором мы говорили уже в главах 1 и 6.

Правило Дунса Скота на первый взгляд кажется менее очевидным, чем предыдущие правила, но в действительности даже люди, далекие от науки, интуитивно уверены в его справедливости. Когда кто- нибудь, желая показать, что убежден в ложности некоего утверждения, говорит: «Если это верно, то я китайский император», он пользуется правилом Дунса Скота. Именно в силу этого правила условное утверждение считается истинным, когда его посылка опровергнута (ср. те соображения, которыми мы обосновали в главе 5 определение имплика-ции; см. также ниже в настоящей главе пример 11). В математических рассуждениях правило Дунса Скота часто используется при доказатель-

И

справедиво утверждение C, мы рассматриваем различные случаи, и

И

(т. е. из него в этом случае выводится заведомая ложь), то мы считаем, что и в этом случае C истинно при условии И. Например, утверждение «Все диагонали выпуклого многоугольника лежат целиком внутри него» (точнее: «Всякая внутренняя точка диагонали выпуклого многоугольника является внутренней точкой этого многоугольника») истинно, хотя некоторые выпуклые многоугольники (а именно, треугольники)

И

емая точка является внутренней точкой некоторой диагонали данного многоугольника.) Еще один пример использования ДС в сочетании с разбором случаев см. ниже в этой главе (пример 12).

Закон исключенного третьего занимает в системе логических правил особое место; о его роли в рассуждениях мы будем говорить в следующей главе, а в этой будем рассматривать только такие выводы, в которых он не используется.

Что касается правила тривиальной выводимости, то это, собственно, не логическое, а структурное правило, играющее чисто техническую роль. В техническом аспекте очень удобно считать каждое утверждение выводимым из любого множества утверждений, в котором оно содержится (и, в частности, из самого себя).

4. Процесс вывода изображается в исчислении естественного вывода не в виде последовательности шагов, расположенных «в одну линию», а в виде дерева. Как выглядит такое изображение, лучше всего уяснить себе на примерах.

Пример 1. Покажем, что сг&р h J3&а. Для этого построим следующую фигуру (дерево вывода):

3_g а—вк

Р&а

В этой фигуре каждая горизонтальная черта отвечает одному шагу вывода. Слева от черты записан номер шага, справа — сокращенное название применяемого на этом шаге правила. Над чертой записаны фор-мулы, к которым это правило применяется, под чертой — формула, получаемая в результате его применения. Самая нижняя формула (единственная, под которой нет черты), называется корнем дерева; самые верхние формулы (те, над которыми нет черты), называются листьями. Корень — это формула, получающаяся в результате данного вывода, листья — его посылки. (Точнее, множество листьев дерева есть множество посылок вывода. Дело в том, что дерево может иметь несколько одинаковых листьев, но в таком случае все они «считаются только один раз»; так, в рассмотренном примере множество листьев состоит из одной формулы сг&р, входящей в дерево дважды.)

Номера шагов и названия правил мы записываем только ради большей ясности, в принципе без них можно обойтись: какое правило при-меняется на том или ином шаге, всегда можно узнать по виду формул, стоящих над и под чертой, а номера служат просто метками, позволяющими в случае надобности ссылаться на тот или иной шаг. Нумерация шагов никоим образом не означает, что вывод должен производиться в задаваемом ею порядке: единственное условие, которому должен удовлетворять порядок шагов, состоит в том, что «нижний» шаг можно выполнять только после того, как выполнены все «верхние», от которых он зависит —т. е. те, которые расположены на «ветвях», «растущих» из черты, отвечающей этому шагу.

В дальнейшем мы часто — в очевидных случаях — будем опускать названия правил, а иногда и номера шагов.

Во всех следующих примерах мы вслед за выводимостью, которую хотим доказать, будем сразу рисовать дерево вывода, являющееся ее доказательством.

Пример 2. а, а ^ |3, J3 ^ у h у.

^^уи

т

Пример 3. <х, —(а VJ3) h у.

-УО

I «Vp вд — («Vp)

з^дс т

Пример 4. а&р V у ^ 8, а, р h 8.

1 —2-вк

—ВД

3 gfepVy ot&Vy ^ Ь уд

8

Пример 5. (а&р)&у ha&(Р&у)-

3 (ц&Р)&г ук 1 Qx&fl&r yR 4а<^ук 5 (afep)feT VK

2«і^УК 6 2 Ї ВК

7 « RK

а&(р&у)

Следующий пример показывает, как «работает» правило тривиальной выводимости:

Пример 6. а, р h aVp.

! а 2-ТВ

2——ВД

V

Приведенные примеры показывают, что построение дерева вывода можно представлять себе как «сборку» его из меньших деревьев. Так,

дерево примера 5 составляется (на 7-м шаге) из двух деревьев с корнями а и J3 & Y; П0Д которыми проводится черта, а под чертой записывается конъюнкция их корней; второе из этих деревьев (правое) составляется точно таким же образом (на 6-м шаге), а первое (левое) получается (на 2-м шаге) из «элементарного дерева» (с единственным листом (а & р) & у> единственной чертой и корнем а&р), под которым проводится черта и под чертой записывается формула а. (Таким образом, мы произвели «полный разбор» левого дерева; подобным же образом можно «разобрать» и правое, хотя такой «разбор» будет более громоздким.)

5. Просмотрев приведенный выше перечень правил, можно заметить, что в некоторых из них речь идет просто о том, что из каких- то формул что-то выводимо, а в некоторых о том, что из каких-то формул что-то выводимо при условии, что имеет место какая-то другая выводимость. Правила первого типа мы будем называть безусловными, правила второго типа — условными. Условными являются правила УД, ВИ и ВО, остальные правила — безусловные.

В приведенных до сих пор примерах использовались только безусловные правила, а сейчас мы займемся условными. Для чего они служат? В дедуктивных рассуждениях часто приходится вводить промежуточ-ные допущения, которые потом становятся ненужными и устраняются. Примером может служить доказательство разбором случаев: рассматривая каждый отдельный случай, мы принимаем допущение, что этот случай имеет место, а когда все случаи разобраны, мы больше не нуждаемся в этих допущениях. То же происходит при доказательстве приведением к нелепости: чтобы доказать, что некоторое утверждение ложно, мы допускаем сначала, что оно истинно, а как только из этой гипотезы получено противоречие, она устраняется. Наконец, при доказательстве условного утверждения мы допускаем, что его посылка истинна, и из этого допущения выводим его заключение, а затем устраняем допущение. Эти три приема рассуждения как раз и описываются нашими условными правилами. При применении каждого из этих правил устраняется некоторое допущение или допущения. (Формулируя правила, мы обозначали устраняемые допущения через а. р в правиле УД и через а в правилах ВИ и ВО.) В дереве вывода допущения — это те формулы, которые являются его листьями. Поэтому устранение допущения можно

представлять себе как «обрыв» или «увядание» листа; из дальнейшего будет видно, что «увядание» — более точный образ.

При «сборке» большего дерева из меньших некоторые листья этих меньших деревьев могут «увядать»; те листья, которые не «увянут» до конца, образуют множество исходных посылок вывода, т. е. то множество И, которое стоит слева от знака h в выводимости И ha, доказываемой с помощью данного дерева; «увядшие» листья —это проме-жуточные допущения. Может случиться, в частности, что «увянут» все листья; тогда мы получим вывод из пустого множества — иначе говоря, корень дерева будет доказуемой формулой.

В дальнейшем мы будем писать слова увядать, увядание, увядший без кавычек, а листья, не увядающие до конца вывода, будем называть зелеными листьями соответствующего дерева.

Проиллюстрируем теперь применение условных правил на примерах. При этом мы будем заключать увядшие листья в квадратные скобки, а рядом будем писать в круглых скобках номер шага, на котором увял данный лист. (Впрочем, указание этого номера не обязательно, и иногда мы будем его опускать.)

VhV

-уд

3[3Va ^ [3Va ^ aV[3 J3Va

И

Пример 8. h а. ^ а.

л М(2)

ТВ ВИ

а • а

И

ных листьев; это значит, что формула а ^ а доказуема.) Пример 9. а. І—і—а.

, a —](2)

УО

——ВО

И

Замечание. Сравнение примера 9 с примером 3 иллюстрирует су-щественное различие между правилами ВО и ДС: то и другое применяются в случае, когда выведена константа Л, но при применении ВО один из зеленых листьев дерева увядает, тогда как при применении ДС все зеленые листья остаются зелеными.

—-

h

М(2)

-ТВ

-ви

а —>

Пример 11. —a h а. ^ J3.

УО

, _М(3)

2^-ДС

ви

а —>

Пример 12. а^р, —а h

, М(4)

ГР](4)

УО

-¦а

ТВ

gvp

¦уд

2^ДС 4^

Пример 13. (а vp) Vy h М(4)

pVy

. М(7)

(а Vp) VY

j«V (р VT) "gV (р VT) [я Vp](7) pVy 7 V( V )

М

Пример 14. а. ^ р, —р h —а.

а —>

М(3)

Л -¦а

Пример 15. а ^ р h —Р ^ —а.

Дерево вывода получается здесь из дерева предыдущего примера добавлением одного шага, на котором применяется ВИ.

И

ТВ имеем И, Л h Л, а отсюда то правилу ВО следует, что И і—'Л.

И

Замечание. Нетрудно убедиться, что формула р тогда и только тогда выводима из формулы а, когда доказуема импликация а ^ р. В самом деле, если a h р, то (по правилу ВИ) h а ^ Р; с другой стороны, если импликация а ^ р доказуема, то фигура

а

где Д — дерево вывода формулы а ^ р из пустого множества (не имеющее зеленых листьев), будет, очевидно, деревом вывода формулы р из формулы а.

6. Чтобы лучше понять строение деревьев вывода, нужно научиться хотя бы в несложных случаях строить их самостоятельно. При этом полезно принять во внимание следующие простые соображения:

Во-первых, если среди исходных посылок, из которых нам надлежит нечто вывести (т. е. тех формул, которые должны быть листьями дерева) есть формула, являющаяся конъюнкцией каких-либо двух формул, то нам, скорее всего, придется один или несколько раз применить к этой формуле правило удаления конъюнкции; аналогично для остальных пропозициональных связок. Так, в дереве примера 1 к (единственной) исходной формуле сг&р дважды применяется УК; в дереве примера 5 к исходной формуле (а & р)& у т0 же правило применяется трижды; в деревьях примеров 2 и 4 к исходным формулам применяется УИ, в деревьях примеров 3 и 9 —УО, в деревьях примеров 7 и 13 —УД, в деревьях примеров 14 и 15 — У И и УО, в дереве примера 12 — У О и УД.

То же самое будет, если формула, являющаяся, например, конъюнкцией, получится на одном из промежуточных шагов вывода, или такая формула появится в качестве промежуточного допущения: эту конъюнкцию, скорее всего, придется потом удалить. Так обстоит дело в

&

V

Во-вторых, если формула, которая должна быть корнем, представляет собой конъюнкцию, то получить ее мы, скорее всего, должны будем с помощью правила введения конъюнкции, и аналогично для остальных пропозициональных связок. Так, в деревьях примеров 1 и 5 на «самом нижнем» шаге применяется ВК, в деревьях примеров 6 и 13 — ВД, в деревьях примеров 8,10,11 и 15 — ВИ, в деревьях примеров 9 и 14 — ВО. То же верно для корней «частичных деревьев» (см. хотя бы пример 4, где на шаге 1 применяется ВК и на шаге 2 — ВД).

В-третьих, если мы хотим нечто вывести из дизъюнкции с помощью правила УД, мы должны сначала вывести это из каждого ее члена в отдельности (см. примеры 7, 12, 13).

В-четвертых, если формула, которую нужно вывести, содержит «куски», не входящие в состав исходных посылок, то весьма вероятно, что придется применить ДС (особенно в случае, когда эти «куски» не находятся внутри дизъюнкции, что могло бы дать надежду воспользоваться правилом ВД). Так обстоит дело в примерах 3 и 11. То же относится к корням «частичных деревьев» (см. пример 12). Иногда, впрочем, в подобных случаях работает правило ТВ (см. пример 10).

Пользуясь этими соображениями, можно пытаться рисовать деревья вывода сверху вниз, или снизу вверх, или попеременно в том и другом направлении.

Теперь читателю рекомендуется, прежде чем продолжать чтение, доказать (построением деревьев) следующие выводимости: &hV & , & h &

а, р, —(а&р)

а, р, —у, <*&Р ^У h Л;

а, р, —у, Р ^У h 8;

а&(р&у) h (а&р)&у;

а ^ р, р ^ у ha ^ у;

а ^ (р ^ у) hp ^ (а ^ у);

а ^ (р ^ у) h а&р ^ у;

а&р ^ у ha ^ (р ^ у);

ai ^ Pi, а2 ^ Р2 h ai &а2 ^ Pi &Р2;

V( V ) h ( V )V

а^ р, а р h —а;

(а ^ у) & (р ^ у) h aVp ^ у;

(аVp)&(р ^ у) h aVy.

Т. Обратимся теперь к содержательному смыслу рассмотренных примеров. Каждая из полученных нами выводимое! ей представляет собой, в сущности, некоторое «правило рассуждения». Но эти правила в нашем исчислении не постулируются, как основные правила, перечисленные выше (пункт 3), а выводятся из основных правил. Поэтому их называют производными правилами. Среди производных правил есть очень простые, представляющиеся очевидными даже без всякого обоснования — таковы правила примеров 1 и 7, разрешающие переставлять члены в конъюнкции и дизъюнкции, — другие более сложны, но все они дают формальное описание тех или иных правильных способов рассуждения. Некоторые из этих способов по тем или иным причинам представляют особый интерес, и об их смысле стоит сказать отдельно. Так, выводимости примеров 10 и 11 означают, что импликация истинна, если ложна ее посылка или истинно заключение, выводимость примера 12 —что если дизъюнкция истинна, то из ложности одного ее члена следует истинность другого. Выводимость примера 14 —это правило, известное в традиционной логике под названием modus tollens («отрицательный способ»): если истинно условное предложение, то из ложности его заключения следует ложность посылки. Некоторые выводимости, вошедшие в только что сформулированное задание, также являются важными, часто используемыми правилами: выводимость (7) выражает так называемое «правило транзитивности импликации», (8) — «правило перестановки посылок», (9) — «правило соединения посылок», (10) — «правило разъединения посылок».

8. В заключение главы займемся вопросом о связи между понятиями выводимости и доказуемой формулы, с одной стороны, и изучавшимися в главе 6 понятиями равносильности и тождественно истинной формулы — с другой.

Прежде всего, вспоминая данное в начале этой главы (пункт 2) пояснение к определению доказуемой формулы (доказуемость формулы означает, что она истинна и при этом ее истинность может быть доказана по правилам исчисления без каких бы то ни было посылок), мы можем ожидать, что по объему понятие доказуемости совпадает с понятием тождественной истинности. И это действительно так: формула логики предложений доказуема в исчислении естественного вывода тогда и только тогда, когда она тождественно истинна. Это утверждение называется теоремой о полноте исчисления предложений; его доказательство можно найти в курсах математической логики.

Из теоремы о полноте вытекает, в частности, что рассматриваемое нами исчисление непротиворечиво: не может существовать такой формулы, чтобы и и она, и ее отрицание были доказуемы в этом исчислении. В самом деле, в таком случае и сама формула, и ее отрицание были бы тождественно истинны, а это, очевидно, невозможно.

Чтобы выяснить, что отвечает в нашем исчислении понятию равносильности, введем следующее определение: две формулы называются дедуктивно эквивалентными, если каждая из них выводима из другой. Дедуктивно эквивалентными являются, например, формулы а&р и J3 & а (см. пример 1; ясно, что первую формулу можно вывести из второй точно так же, как вторую из первой, поскольку через а и J3 мы обозначаем произвольные формулы), а Vр и |3 V а (пример 7), (а&р)& у и а & (р & у) (пример 5 и выводимость (6) из задания в пункте 6), (а V р) V y и а V (р V y) (пример 13 и выводимость (12) из того же задания). Во всех этих парах входящие в них формулы равносильны. Так обстоит дело и в общем случае: две формулы логики предложений дедуктивно эквивалентны в исчислении естественного вывода тогда и только тогда, когда они равносильны.

В частности, для каждой из основных равносильностей, приведенных в главе 6, можно вывести ее левую часть из правой и обратно. Для двух равносильностей, выражающих коммутативность конъюнкции и дизъюнкции, мы это уже сделали, для равносильностей, выражающих ассоциативность тех же операций, сделали в одну сторону, в другую это делается аналогично. Приведем еще выводы, отвечающие дистрибутивности конъюнкции по отношению к дизъюнкции:

Пример 17. а&(рVy) 1-а&рVa&у.

»&(РУК Ш8) 4 «&(Р^ УК М(8)

* , R И(8) ВК 5 ^ №ВК , ,я ,

3 <*&р Вд g <*&Г Вд „а&фVY) ук

уд

а& Р Va &Y а&р Va&Y PVY

а&рVa& Y

Пример 18. а&рVa^ ^&(р^).

[а&р](9)

[а&р](9)

[«&г](9)

[«&у](9)

7 Т

У

У

д&ф У у)

&У&

а&ф У Y)

сг&(р У y)

Мы уже умеем, таким образом, выводить друг из друга левые и правые части первых пяти основных равносильностей группы I (см. пункт 3 главы 6). Для остальных трех равносильностей этой группы читатель может попробовать построить соответствующие выводы сам (для 17 и 18 это просто, а для 16 технически довольно сложно, но принципиальных трудностей здесь нет). Нетрудно построить такие выводы

и для равносильностей группы IV (см. пункт 5 главы 6; символы R и F

отвечающих равносильностям групп II и III, в ряде случаев нужны принципиально иные средства, к рассмотрению которых мы обратимся в следующей главе.

<< | >>
Источник: Гладкий А. В.. Введение в современную логику. — М.: МЦНМО,2001. — 200 с.. 2001

Еще по теме Глава 8. Теория доказательства:пропозициональные правила: