НАТУРАЛЬНАЯ СИСТЕМА ИСЧИСЛЕНИЯ ВЫСКАЗЫВАНИЙ

Время: 25-02-2013, 11:38 Просмотров: 1058 Автор: antonin
    
НАТУРАЛЬНАЯ СИСТЕМА ИСЧИСЛЕНИЯ ВЫСКАЗЫВАНИЙ
Постулатами натуральной системы являются только пра-
вила вывода. В выводах и доказательствах в качестве посы-
лок используются только допущения. К их числу можно от-
носить, конечно, и специальные аксиомы теорий, отличая их
при этом от таких допущений, которые играют в доказатель-
ствах промежуточную роль и, в конечном счете, исключают-
ся из доказательств. Более того, всякий вывод (и в частности,
доказательство) начинается с некоторых допущений.
Мы будем строить выводы, учитывая зависимость получа-
емых в них на каждом шаге результатов — формул вывода —
от введенных допущений. Указания на эту зависимость будут
называться характеристиками зависимости
формул вывода от допущений. Каждый шаг вы-
вода, представляющий собой некоторую формулу этого выво-
да с характеристикой зависимости, будет иметь вид: А [Г], где
А — сама формула вывода, а Г — множество формул, от кото-
рых зависит Л в этом выводе. Г — может быть, конечно, и
пустым множеством. Этот случай будет указывать, что фор-
мула является законом логики и вместе с этим — теоремой
логического исчисления.
121
Понятие зависимости формул определяется индуктивно:
1. Каждое допущение вывода зависит от самого себя. Это
означает, что характеристикой зависимости допущения А яв-
ляется одноэлементное множество {Л}, однако фигурные
скобки мы далее будем опускать и будем употреблять обо-
значение А [А].
2. Для остальных формул вывода, получаемых по прави-
лам вывода из других, зависимости определяются в самих
формулировках правил.
Правила вывода. Мы будем рассматривать систему,
включающую в качестве постулатов правила вывода (исход-
ные правила) относительно всех ранее выделенных в языке
логики высказываний логических констант (связок): конъ-
юнкции — &, дизъюнкции — v, импликации — z> и отрица-
ния ,. Как обычно в натуральных системах, для каждой
логической константы имеется правило введения этой кон-
станты и правило удаления ее (этим объясняются специаль-
ные обозначения правил, например, «&в» — правило введе-
ния конъюнкции; «&и », «&и » — первое и второе правило
исключения конъюнкции; А, В, С — далее любые формулы;
Г, Д — любые, возможно пустые, множества допущений. В
правилах мы различаем также посылки применения данного
правила с характеристиками зависимости (записываются над
чертой) и заключения применения данного правила, — фор-
мула с характеристикой зависимости (указывают под чер-
той). Посылки — уже имеющиеся в выводе формулы, а за-
ключение — формула, которую согласно правилу мы имеем
право добавлять (и добавляем при применении правила) к
имеющемуся выводу. Итак, мы принимаем следующую сис-
тему правил:
, А[Г],В[А]
*• Л&5ГГ Д1' ГАе Г' Л есть °бъеАинение множеств Г и А,
то есть Г, А = ГиД;
3
-
122
Для завершения описания исчисления необходимо сфор-
мулировать понятие вывода и доказательства.
Выводом некоторой формулы В из множества допущений
А называется непустая конечная последовательность формул
с характертистиками зависимости Bjrj, ... , -ВЛ[ГП], в кото-
рой каждая формула есть либо допущение, либо поручена из
предыдущих по какому-либо правилу вывода, причем Вп есть
В (заключение вывода), а ГЛ — некоторое множество допу-
щений Г, являющееся подмножеством А (Г с А). Ясно, что
данную последовательность можно охарактеризовать также
1
По данной формулировке это правило выглядит как введение дизъ-
юнкции. В каком смысле оно является исключением дизъюнкции, будет
разъяснено позже.
(АУВ)[Г], ^А[А)
Вместо правила vH может быть взято прямое правило gtr Ai •
Это известная форма вывода, называемая modus tollendo ponens раздели-
AvB,-,A
тельного силлогизма к •
D
123
как вывод В из Г. Характеризуя же его как вывод из А, мы
подчеркиваем то обстоятельство, что каждый вывод форму-
лы В с характеристикой Г, представляет бесконечное множе-
ство выводимостей, поскольку А может быть любым расши-
рением Г. Выводимость Г \- В является для данного вывода
наиболее сильной, так как в выводе использованы все допу-
щения из данного множества Г (хотя возможен и другой вы-
вод с меньшим числом использованных допущений).
Данная система исчисления эквивалентна рассмотренной
выше аксиоматической формулировке исчисления высказы-
ваний. Это значит, что формализация следования здесь аде-
кватна, то есть каждому случаю отношения следования Г 1= А
в системе соответствует отношение формальной выводимос-
ти Г ь А и наоборот. Поскольку согласно определению следо-
вания «Если В следует из Г, то оно следует из любого расши-
рения Г», постольку аналогичное свойство имеет и отноше-
ние формальной выводимости (если Г I- В, то и А Ь- В, где А —
любое расширение Г, то есть ГсА).
Итак, вывод с заключением В, зависящим от множества
допущений Г — при непустом Г — мы будем обычно харак-
теризовать как Г I- В. В случае если Г пусто, вывод называет-
ся доказательством формулы В и характеризуется как н В
(вывод В из пустого множества допущений). Но и в этом слу-
чае любое доказательство В представляет собой также вывод
А I- В, при любом А. Очевидно, что в силу указанного понятия
В [Г]
выводимости правомерно правило: ^гд п' допускающее
возможность расширения характеристик зависимости. Это
правило, называемое часто правилом утончения и являющее-
ся производным, мы будем применять наряду с указанными
выше основными правилами (как будет показано дальше, его
применение может быть исключено за счет более сильной
формулировки правил ZDB И -.В. Формально — как производ-
ное правило — оно может быть получено из основных пра-
вил системы.) В самом деле, положим, что в каком-то выводе
получено заключение В с характеристикой зависимости Г, то
есть имеем В [Г]. Тогда мы можем продолжить этот вывод,
добавив допущение А, то есть Л [А] и получить (по правилу
&в) А&.В [А, Г], а отсюда (по правилу &и ) — В [А, Г]. Итак,
124
имея в выводе В [Г], мы по основным правилам системы по-
лучили В [А, Г].
Рассмотрим теперь несколько примеров выводов и дока-
зательств. Допущения будем выделять знаком « + ». Как и
обещали, приведем доказательство закона тождества.
Пример 1. Схема доказательства формул вида A z> A — за-
кон тождества:
+ \.А[А] ;
2. А эА[-] ИЗ 1, зв.
В дальнейшем, как и в приведенном примере, будем ну-
меровать все формулы вывода и для упрощения записей
вместо формул в характеристиках зависимости будем указы-
вать их номера в выводе.
Пример 2. Схема доказательства формул вида
((A&B)DQD(AD(5DQ) — закон экспортации:
+ 1. (А&В)=эС[1];
+ 2. А [2];
+ 3. В [3];
4. А & В [2, 3] — из 2 и 3, &в;
5. С[1, 2, 3] — из 1 и 4, зи;
6. BDC[1, 2] —из 5, зв;
7. Аз {Вз С) [11 — из 6, =эв;
8. ((А&5)^д^(А=)(ВзС)) [-] — из 7, z>B.
Последовательность формул 1—8 представляет собой
здесь доказательство нужной формулы. Любая часть этой
последовательности 1—п (1 С), А ь- В ZD С и т. п.
Пример 3. Схема доказательства формул вида AD(BDA) —
закон консеквента:
+ 1. A [1J;
+ 2. В [2];
3. А [ 1, 2] — из 1, правило утончения;
4. ВзА [1] —из Ззв;
5.A^{Bz>A) [-] —из 4, z>B.
Решение вопроса о том, какие вспомогательные допуще-
ния использовать для построения того или иного вывода, от-
носится к числу творческих моментов. При данном построе-
нии системы (с характеристиками зависимости) в вывод мо-
гут вводиться, вообще говоря, любые допущения, они просто
не найдут отражения в характеристиках зависимости. Любое
125
допущение может использоваться независимо от того, при-
менялись ли правила, исключающие его. Однако при введе-
нии вспомогательных допущений существенно иметь в виду
возможность устранить в конечном счете зависимость от
них подлежащей выведению или доказательству формулы.
Это может быть осуществлено только применением правил
V
M' -"В' "'В'
С учетом этого могут быть указаны некоторые эвристи-
ческие принципы введения допущений.
1. Если в качестве заключения вывода должна быть полу-
чена формула вида Ах z> (Л2 з... (Ат z> J5)...), то можно исполь-
зовать в качестве вспомогательных допущений Av A2, ..., Ат,
стремясь вывести В. Формула, выведение которой является
конечной целью, может быть получена тогда, очевидно, по =>в.
Правило -iB обеспечивает возможность строить выводы
по принципу или, способу, «опровержение сведением к аб-
сурду», а в сочетании с -.и также по принципу «доказатель-
ство от противного».
2. Первый способ состоит в том, что, желая вывести от-
рицание некоторого высказывания В, то есть -Д берут в ка-
честве допущения В (возможно, конечно, в дополнение к
другие посылкам, например, допущениям, введенным соглас-
но пункту 1). Цель теперь должна состоять в том, чтобы по-
лучить противоречие («абсурд»), то есть вывести некоторое
Си -.С. Тогда по -iB получаем -i В, и притом не зависящее
от допущения В.
3. Способ доказательства «от противного» состоит в том,
что, желая вывести В, вводим допущение -i В. Если теперь
удастся вывести некоторое С и его отрицание -. С, то по -i B
получаем -. -. В (не зависящее от допущения -.В), и по -i и
выводим нужное В.
4. Конечно, для того, чтобы полнить упомянутые в пунк-
тах 2 и 3 С и -л С, могут понадобиться дополнительные допу-
щения. Так, если В есть высказывание вида Вх v B2, то наряду
с -, (Blv B2) можно использовать В{ или В2 (или и то, и дру-
гое). Это целесообразно, в частности, когда желательно
иметь в выводе Вх или ВТ Совершенно очевидно, что уже в
указанных допущениях содержится противоречие, которое
обнаруживается: как только по vB (или по vB ) мы получаем
В{ v В2 из Вх (или В2). Аналогично, если учесть, что AziB эк-
126
Бивалентно -. A v В — желая получить А или -. В при наличии
в выводе -. (А => В) — следует брать допущения -и А или В.
5. Если В, которое желательно вывести, имеет вид Вх & В2,
то вывод его, очевидно, обеспечен (по &в), если выведены В{
и Вт Для осуществления выводов этих составляющих, есте-
ственно опираться на сформулированные уже принципы.
Рассуждая, например, по принципу «доказательство от про-
тивного», можем ввести допущения -• Вх и -. Вт
6. Если в некотором выводе получена формула вида AvB,
а цель состоит в получении некоторой (отличной от указан-
ной) формулы С, которую не удается вывести из имеющихся
посылок, естественно прибегнуть к способу «рассуждения
по случаям», вводя сначала допущение А, затем В и стремясь
в каждом случае получить С. Если С выводимо при допуще-
нии А невыводимо также из допущения В (независимо от А),
то по vH получаем С независимо от допущений А и В (если
A v В является в выводе допущением, то С будет зависеть те-
перь от него). (Введенная выше оговорка относительно того,
что при допущении В формула С должна быть выведена не-
зависимо от допущения А, не означает каких-либо ограниче-
ний на применение правила vH. В случае невыполнения ого-
воренного условия мы просто не получим желаемого резуль-
тата.)
Мы уже упоминали выше, что наличие правила утонче-
ния необязательно в данной системе. Можно заметить (см.
примеры 3 и 4), что оно применяется только в двух суще-
ственных случаях, связанных с правилами зв и ->в. Первое
указывает на то, что если выведена некоторая форму-
ла В, зависящая от множества допущений Г, и при этом мы
хотим получить высказывание A z> В, тогда нужно, — соглас-
но формулировке правила z>B — чтобы в числе элементов Г
была и А. Однако согласно понятию логического следования
в применении к системе рассматриваемых логических свя-
зок (классической логике) это необязательно, то есть мы мо-
жем получить A ID В даже в том случае, когда В не зависит
от А. Это позволяет сформулировать правило зв в виде:
В [Г]
A z> В [Г — {А}]' гл-е А- — любое имеющееся в выводе допуще-
ние (при этом если его нет в выводе, то его всегда можно
приписать) и где Г — {А} есть множество допущений, кото-
127
рое получается из Г исключением А (если, конечно, таковое
имеется в Г, в противном случае, Г — {А} есть само Г; ясно
также, что если Г = {А}, то Г — {Л) есть пустое множество,
как в примере доказанной выше формулы А => А).
Аналогично дело обстоит и с правилом введения отрица-
ния (-iB). Содержательно правомерно выводить -.Лиз сово-
купности формул В и -1В и в том случае, когда какая-нибудь
из этих формул и даже обе не зависят от А. Отсюда возника-
ет возможность более общей формулировки этого правила:
В[Ц, -Д[А]
-А [(Г А) —(А)]'1 гАе А — любое имеющееся в выводе допу-
щение.
• Упражнения
1. Осуществите доказательства, данные в примерах 3 и 4,
без применения правила утончения, пользуясь только что
введенными формулировками правил зв и ->Б.
2. Постройте доказательства формул:
а) (A Z) {В z> Q) з ((А & В) ZD С) — закон импортации;
б) (А =э В) z) (-1В з -I А) — закон контрапозиции;
в) (-.AD-IB)D(BDA) — закон сильной контрапозиции;
г) ((ADBJDA)DA — закон Пирса.
3. Осуществите выводы:
а) (AvB) к- ЬАэВ);
б) ((AvJ3)3Qb-A=>C;
в](А з С, В з С, A v В \- С.
4. Постройте доказательства формул (законов логики, со-
ответствующие выводимостям упражнения 3):
а) {AVB)Z>(^AZDB);
б) ((Av5)3Qz>(A:Dq;
в) (ADqD((B3qD((Av5)Dq).
Мы уже употребляли такие понятия, как основные прави-
ла и производные. Основные — это исходные правила
системы (постулаты системы). Производным является
правило, заключение которого может быть выведено из его
посылок по основным правилам. Мы могли видеть это уже на
примере правила утончения. По существу, таким образом,
128
производные правила — это некоторые выводы по основным
правилам системы. Они используются в системах для сокра-
щения выводов; применение производного правила есть со-
кращение именно того вывода, которое оно представляет.
Если читатель выполнил предшествующее упражнение 3, то
тем самым он получил три производных правила:
Ясно, что применение производных правил не является
обязательным; каждое такое применение может быть заме-
нено соответствующей этому правилу последовательностью
формул. Читателю должно быть ясно и то, что каждой дока-
зуемой в системе формуле (теореме) вида AID В соответству-
А[Г]
ет производное правило "^грг •
• Упражнение
1. Доказать теоремы:
а) ((A3Q&(5z)q)=)((AvB)z5q;
б) ((A ID В) & (A ID Q) z> (А з {В & Q, и указать соответствую-
щие им производные правила.
Существенное значение при анализе рассуждений имеет
различение прямых и непрямых правил. Прямые пра-
вила указывают на выводимость какого-то высказывания
из каких-либо высказываний (в исчислении — выводимость
формулы из формул). В предлагаемой системе все правила
сформулированы как прямые. Однако существенной особен-
ностью обладают правила введения импликации (=>в), введе-
ния отрицания (-,в) и правило исключения дизъюнкции (vM).
В отличие от других они позволяют, исключать некоторые
5-2061 129
допущения из характеристик зависимости формул (возмож-
но с заменой их — как при vM — другими допущениями),
что характерно для непрямых правил рассуждения. При при-
менении «vH» исключаются допущения А и В с заменой их
на A v В; при « ->в» и « зв» исключается допущение А.
В других системах (без характеристик зависимости) они
формулируются явным образом как непрямые, соответствен-
но:
В этой формулировке очевидна их особенность, состоя-
щая в том, что они указывают на возможность заключения о
наличии некоторой выводимости на основе других выводи-
мостей. Специфика их в рассуждениях состоит в том, что
они дают возможность использовать в рассуждениях наряду
с данными посылками вспомогательные допущения с после-
дующим исключением их из рассуждения. Так, желая полу-
чить вывод Г, A v В \- С, мы совершаем «обходной» маневр,
используя правило vM : учитывая указанные в дизъюнкции
A v B возможности — истинность А или истинность В — рас-
суждаем «по случаям»1 — осуществляем вывод Г, А\- С, со-
ответствующий случаю истинности А, и вывод Г, В ь С, соот-
ветствующий случаю истинности В. Пользуясь указанным
правилом vH, заключаем после этого о наличии нужной нам
выводимости Г, A v В \- С (здесь содержится обещанное ра-
нее разъяснение, почему именно данное правило называется
правилом исключения, а не введения дизъюнкции: дизъюнк-
ция A v В исключается из рассуждения). Например, надо
вывести, что «данное число делится на 5» — [С] из дизъюнк-
ции «это число оканчивается на 0 или на 5» — (A vB). С уче-
1
В силу того, что само это правило часто называют правилом рассуж-
дения «по случаям».
130
том множества аксиом арифметики и выводимых из них
утверждений — Г и рассуждая «по случаям», осуществляем
сначала вспомогательные выводы Г, А \- С и Г, В \- С, затем
заключаем о наличии нужной нам выводимости: Г, A v В I- С.
По правилу ZDB вместо того, чтобы непосредственно выво-
дить условное высказывание ЛзВиз посылок Г (что обычно
представляет определенную сложность), мы заключаем о на-
личии этой выводимости на основе вспомогательного вывода
Г, А\- В. Из аксиом геометрии Г, например, можно вывести
«если углы, полученные при пересечении двух параллельных
линий третьей, являются соответственными (Л), то они рав-
ны {В)» на основании вспомогательного вывода Г, Л ь В.
Правило -.д в истории логики, как и в конкретных на-
уках, например, в математике, известно как правило
опровержения путем «сведения к абсур-
ду».
Часто этот прием опровержения составляет часть другого
рассуждения, которое называется «доказательством от про-
тивного». Этой форме рассуждения соответствует также не-
Г, -iAf-fl-Г, -,Al-^B
прямое правило: р ( (^ д • Оно может быть полу-
чено из предыдущего с использованием правила снятия двой-
ного отрицания —-—. обозначенного в нашей системе как
Г, -,АнД;Г, -.Ан-ifl
-1И. По правилу опровержения имеем rv-n-nA и
теперь по правилу -.и получаем: Г к А. Желая доказать, на-
пример, что согласно аксиомам геометрии (Г) «из данной точ-
ки плоскости, лежащей вне этой плоскости, можно опустить
только один перпендикуляр на прямую, принадлежащую этой
плоскости», предположим, что это А неверно, то есть имеет
место -iA (можно опустить не один, по крайней мере, два
перпендикуляра). Теперь оказывается, что если из точки опу-
щено два перпендикуляра, то сумма углов полученного тре-
угольника больше 180°, поскольку каждый перпендикуляр об-
разует с соответствующей прямой угол, равный 90° (обозна-
чим это утверждение ,В, оно представляет собой отрица-
ние утверждения В о том, что сумма углов всякого треуголь-
131
ника равна 180°, которое является следствием аксиом геомет-
рии, а значит, и расширения множества Г за счет добавления
нашего утверждения -iA). Таким образом, мы имеем две вы-
водимости: Г, -1А \- В и Г, -. А I—i В, по указанному правилу
доказательства «от противного» получаем отсюда: Г У- А.
В дополнение к уже рассмотренным примерам законов
логики приведем список некоторых других наиболее важных
схем законов логики (которые читатель может использовать
в качестве упражнений для доказательств):
1. HAD(ADB).
2. (AVB}D(-.ADB).
3. (ADB)D(-,AVB).
4. (А&В)з-.(А=э-,В).
5. (АэВ)эп(А&пВ).
6. -,(A&B)z>(-,Av-,B).
7. -,(AVB)=D(-.A&-,B).
8. {Az>В) z> {{A& С) z> {В& Q).
9. [Az>В) z> {{Av С) и (В v Q).
10. (A&(BVQ)D ((A & B) v (A & Q).
11. (A v (B & Q) z> ((A v B) & (A v Q).
Эти законы, как нетрудно заметить, выражают связь
между логическими константами языка логики высказыва-
ний.

| распечатать

Другие новости по теме:

Другие новости по теме: