ИСЧИСЛЕНИЕ ВЫСКАЗЫВАНИЙ

Время: 25-02-2013, 11:38 Просмотров: 1419 Автор: antonin
    
ИСЧИСЛЕНИЕ ВЫСКАЗЫВАНИЙ
Построение и анализ логических исчислений (высказыва-
ний и предикатов) составляют содержание одного из наибо-
лее важных разделов современной логики как науки. Это —
существенная часть теории дедукции. Теория дедук-
ции включает: 1) описание формализованного языка; 2) логи-
ку языка; 3) исчисление.
из
Исчисление — это формализация соответствующей логи-
ки. Исчисления составляют основное содержание современ-
ной логики. Теория дедукции, включающая логические ис-
числения, — это формальная логика в строгом смысле этого
слова. Однако в данном случае речь идет о современном эта-
пе логики. Как в традиционной, так и в современной логике
предметом изучения формальной логики (теории дедукции)
являются формы правильных рассуждений (выводов, доказа-
тельств), или, как их было принято называть прежде, формы
дедуктивных умозаключений.
Умозаключением вообще называют один из приемов по-
знания — выведение из имеющихся высказываний нового вы-
сказывания, то есть некоторый логический прием получения
нового знания на основе имеющегося.
Наряду с дедуктивными выводами (умозаключениями) су-
ществуют также индуктивные (а некоторые авторы выделя-
ют еще и традуктивные выводы).
Специфика дедуктивных выводов состоит в том, что они
обеспечивают истинность выводимого высказывания — за-
ключения — при истинности исходных суждений — посы-
лок вывода (умозаключения). Это свойство дедуктивных вы-
водов обусловлено, в свою очередь, наличием определенной
связи между их посылками и заключением. Их связь воспро-
изводит отношения логического следования между соответ-
ствующими высказываниями.
Имеется принципиальное различие между теорией дедук-
ции в традиционной логике и современной. В традиционной
логике теория сводилась, в основном, лишь к эмпирическому
выделению и описанию некоторых форм правильных рас-
суждений — правил дедуктивного вывода — без какого-либо
полного их обоснования. Дело в том, что в прежней логике
не было необходимых для этой цели понятий логического за-
кона и отношения логического следования.
Основой метода построения теории дедукции с примене-
нием метода логических исчислений является, как мы уви-
дим позднее, наличие взаимосвязей между самими законами
и правилами вывода, в силу которых одни законы и правила
можно обосновывать с помощью других. Исчисление (логи-
ческое) — это теория, которая строится, как уже ясно из
предыдущего, на базе некоторого формализованного языка,
например, исчисление высказываний на базе описанного язы-
114
ка логики высказываний. При построении исчисления, во-
первых, в качестве исходных выделяется минимальное мно-
жество формул — законов логики — и правил вывода (в ак-
сиоматических системах) или только правил (в натуральных
системах). Во-вторых, определяются понятия вывода и
доказательства. Понятие вывода — какой-либо фор-
мулы из множества формул — и понятие доказательства
формулы являются основными в логическом исчислении.
Эти понятия определяются таким образом, чтобы а) всякая
доказуемая формула представляла собой закон логики, фор-
мулируемый в данном языке, и чтобы б) была возможность
осуществить доказательство любой формулы, представляю-
щей собой закон логики. При этом в случае доказательства
формул вида (Aj z> (A2z>... (АЛ z> В)...)) осуществим также вы-
вод формулы В из множества формул Av A2, ..., Ап, соответ-
ствующий имеющемуся в таком случае отношению логиче-
ского следования: А1Г А2, ..., Ап (=5. Показательно, что выво-
ды и доказательства осуществляются при этом по фор-
мальным правилам, то есть по таким правилам, для
применения которых не требуется учитывать смысл употреб-
ляемых высказываний, надо учитывать лишь характер знако-
вых форм этих высказываний (состав и порядок расположе-
ния знаков языка, из которого они построены). Более того,
правильность или неправильность осуществляемых выводов
и доказательств оценивается без учета смысла имеющихся
высказываний. Последний может приниматься во внимание
лишь в эвристических целях — при поиске и составлении
плана доказательства или вывода, при определений необхо-
димых средств его построения и т. д.
Все сказанное означает, что в исчислении осуществляет-
ся формализация основных понятий логики, а именно: зако-
на логики и отношения логического следования. Для каждо-
го из этих семантических понятий формулируется его син-
таксический (формальный) аналог: для закона логики — до-
казуемая формула, для отношения логического следова-
ния — формальный вывод, в результате осуществления кото-
рого устанавливается формальная выводимость. Употребляя
для доказанности формулы А обозначение - А, а для выво-
димости формулы В из некоторого множества формул Г
обозначение Г - В, получаем — при правильном построении
115
исчисления — следующие соотношения между указанными
семантическими понятиями и их синтаксическими аналога-
ми:
. н Л е. т. е. 1= А и Г t- В е. т. е. Г t= В.
Если выполняются эти соотношения, то говорят, что в ис-
числении осуществлена адекватная формализация основных
понятий: закона логики и отношения логического следования.
Важно заметить, что, в силу сказанного, построение логиче-
ского исчисления означает также формализацию
рассуждений. Естественные рассуждения заменяются
здесь формальными преобразованиями знаковых форм вы-
сказываний. Это обеспечивает точность и проверяемость вы-
водов и доказательств и открывает возможность передачи
осуществления соответствующих видов интеллектуальной
деятельности человека машине. Однако в тех или иных случа-
ях оказывается, что формализация неполна, а для некоторых
языков она и в принципе не может быть полной. При непол-
ной формализации имеем: если I- А, то N А, но обратное име-
ет место не для любых формул. Аналогично, при наличии вы-
водимости Г у- В имеется отношение Г 1= В, но не для всякого
отношения логического следования может быть построен
формальный вывод, то есть получена соответствующая фор-
мальная выводимость. В последнем случае говорят, что логи-
ческое исчисление непротиворечиво относительно заданной
семантики языка, но не является полным. При адекватной же
формализации основных семантических понятий оно семан-
тически непротиворечиво и полно относительно заданной се-
мантики. Утверждения о наличии у исчисления этих и других
подобных свойств называются метатеоремами ис-
числения. Их доказательство осуществляется иными сред-
ствами, чем доказательство теорем самого исчисления1.
Существуют различные способы формализации логики и
соответственно различные формы (или типы) логических ис-
числений. В качестве основных выделяются аксиомати-
ческие системы, натуральные системы и
системы секвенциального типа. Внутри каж-
дого типа возможны также различные, но эквивалентные
между собой (представляющие формализацию одной и той
1
Важную роль здесь играет метод математической индукции.
116
же содержательной логической теории) системы, различаю-
щиеся составом постулатов (аксиом и исходных правил вы-
вода — в аксиоматических системах; исходных правил выво-
да — в натуральных системах; исходных секвенций и правил
вывода для секвенций — в исчислениях секвенций).
Построение систем логических исчислений имеет двоя-
кое значение. Во-первых, теоретическое для самой логики,
поскольку в процессе и в результате этого построения выяв-
ляются связи между логическими законами, правилами вы-
вода. Из бесконечного множества тех и других выделяется
множество исходных, достаточных для доказательства всех
формул, представляющих логические законы, для воспроиз-
ведения всех возможных отношений следования, для обос-
нования любого из допустимых правил рассуждения и т. п.
Во-вторых, построенное логическое исчисление может быть
использовано как логический аппарат для осуществления
выводов и доказательств в тех или иных нелогических тео-
риях, построенных на базе соответствующего прикладного
формализованного языка. Построение теории при этом осу-
ществляется просто добавлением специальных ее аксиом к
постулатам логического исчисления.
Построение всякого логического исчисления, как и лю-
бой формальной системы, начинается с формулировки пос-
тулатов. В аксиоматических логических
системах таковыми являются: некоторое непустое мно-
жество аксиом — формул, являющихся законами логики, и
так же непустое множество правил вывода (правил преобра-
зования формул). При этом обычно прибегают к сокраще-
нию количества связок языка с учетом того, что одни из них
могут быть выражены (определены) через другие. Например,
& и v посредством з и -i. Так, согласно имеющимся в задан-
ном языке отношениям, формула А & В истинна е. т. е. истин-
на формула -. (A =э -i В); Av В истинна е. т. е. истинна A z> В. В
силу этого при построении исчисления можно принимать в
качестве основных его связок только z> и -,, а формулы вида
А & В и A v В рассматривать как сокращения, соответствен-
но, для формул: -I (A => -i В) ИпАэВ.
При построении аксиоматических исчислений качествен-
но различаются системы с конечным и бесконечным мно-
жеством аксиом, или — системы с аксиомами и
системы со схемами аксиом. Бесконечное
117
множество аксиом задается перечислением некоторого ко-
нечного множества схем аксиом.
Аксиома — это формула языка. Например, в языке логи-
ки высказывании в качестве аксиом можно взять формулы
(р=>(д=>р)) или (p^{rz>p)).
Схема аксиом — это выражение метаязыка, представля-
ющее бесконечное множество формул определенной струк-
туры. Например, (Az> (Bz>A)). Различные формулы получа-
ются заменой А, В какими-либо формулами языка (подста-
новкой вместо А и В каких-либо формул языка). Ясно, на-
пример, что формулы
и
и т. д. будут принадлежать к одной и той же схеме:
Принимая во внимание все вышесказанное, аксиомати-
ческую систему исчисления высказываний можно задать
следующим образом:
I. В качестве схем аксиом выступают:
а) AD(BDA) — схема консеквента;
б) (AD(BDQ)D((ADB)D(ADQ) — схема самодистрибу-
тивности импликации;
в) (-.AD-IB)D(BDA) — схема обратной (сильной) кон-
трапозиции.
II. Правило вывода (в данной формулировке одно): из
АэВ И А непосредственно выводимо В. В иной записи:
(Аз В),А
- — правило modus ponens — m. р. (правило «модус
поненс».)
III. Доказательством некоторой формулы В в данной сис-
теме называется непустая конечная последовательность фор-
мул В1( В2, .... Вт, в которой каждая формула есть или аксио-
ма (частный случай какой-либо из схем аксиом) или получа-
ется из предыдущих формул последовательности по правилу
вывода и последняя формула Вт которой есть В.
118
Формула, для который имеется доказательство, называ-
ется теоремой системы.
Нетрудно проверить, что последовательность, состоящая
из одной аксиомы, есть доказательство этой аксиомы. Зна-
чит, все аксиомы системы являются и ее теоремами.
В практике познания в определенных случаях возникает
необходимость проводит рассуждения с использованием не-
которых допущений, то есть высказываний, которые не яв-
ляются доказанными, например, в той или иной теории1.
Формальным аналогом таких рассуждений у нас будет поня-
тие вывода из допущений.
Выводом формулы В из множества допущений Г называ-
ется непустая конечная последовательность формул Bv Bv
..., Вт, в которой каждая формула есть или некоторое допу-
щение из Г, или аксиома системы, или получается из пред-
ыдущих формул по правилу вывода, и последняя формула Вт
этой последовательности есть В.
Очевидно, что понятие вывода из допущений является
обобщением понятия доказательства. Доказательство есть вы-
вод из пустого множества допущений. Утверждение о нали-
чии вывода (выводимости) формулы В из множества допуще-
ний Г записывается (в метаязыке, конечно) в виде Г ь В; в слу-
чае пустого Г (то есть при наличии доказательства В) имеем
н В (читается: «В доказано» или «В есть теорема системы»).
Рассмотрим в качестве примера доказательство формулы
(рзр). Для удобства нумеруем члены последовательности и
указываем для каждой формулы, является ли она аксиомой
или получена из других формул; указания такого рода назы-
ваются анализом доказательства (вывода).
1. рз ((рзр) зр) — аксиома (частный случай схемы кон-
секвента).
2. (рэ ((рз p) з р)) з ((рэ (рз р)) з (рз р)) — аксиома
(частный случай схемы самодистрибутивности з).
3. (р з (р з р)) з (р з р) — из пунктов 2 и 1 поправилу т. р.
4. (р з (р з р) — аксиома (частный случай схемы консек-
вента).
5. (р з р) из пунктов 3 и 4 по т. р.
1
НИЧТО не мешает нам, конечно, рассматривать в качестве допущения
и некоторую формулу, фактически являющуюся теоремой, отвлекаясь от
того, что существует ее доказательство.
119
Итак, имеем н (рзр), то есть «формула рзр есть теоре-
ма нашей системы».
Если вместо формул (выражений языка) использовать
схемы формул (выражения метаязыка), а вместо аксиом —
схемы аксиом и их варианты, то получим схему дока-
зательства формул определенной структуры. Соответ-
ственно вместо выводов можем строить схемы выво-
дов. Каждый вариант той или иной из схем аксиом мы
обозначаем тем же названием.
Схема доказательства формул вида АэЛ1.
1. А з ((АзА) зЛ) — схема консеквента (один из вариантов).
2. (Аз((АзА)зА))з ((Аз(АзА))з(АзА)) — схема само-
дистрибутивности з.
3. (А з (А з А)) з (А з А) — из пунктов 2 и 1 по т. р.
4. А з (А з А) — схема консеквента.
5. А з А из пунктов 3 и 4 по т. р.
В символической логике имеется доказательство того, что
приведенная формулировка исчисления высказываний пред-
ставляет собой адекватную формализацию понятий закона
логики и отношения логического следования.
Мы не останавливаемся здесь подробно на рассмотрении
этой системы, как и вообще аксиоматических построений,
поскольку имеются значительные сложности в применении
их как аппарата дедукции. Уже из рассмотренного примера
доказательства казалось бы самого простейшего закона логи-
ки видно, насколько трудно осуществимы в этой системе до-
казательства и выводы. Трудно определить в каждом конкрет-
ном случае доказательства, какие именно из аксиом нужно
выбрать в качестве посылок для его осуществления. К тому
же выводы здесь значительно отличаются от тех, которые мы
имеем в естественном языке. И отличаются именно тем, что в
последних не употребляются в качестве частей — посылок
выводов и доказательств — законы логики, а ведь аксиомы,
как мы помним, и являются таковыми. В математических до-
казательствах, например, в геометрии, посылками доказа-
тельств являются аксиомы геометрии или уже доказанные на
их основе утверждения. В ряде других случаев, и особенно
вне аксиоматических теорий, это могут быть просто какие-то
1
Ясно, конечно, что к формулам данного вида будут принадлежать та-
кие, например, как: (А & В) =э (А & В), (В з Q •=> (В => Q, (AVB)D(AVB) и др.
120
допущения (гипотезы). Указанные трудности в построении
выводов и доказательств и несоответствие естественным рас-
суждениям преодолеваются в определенной мере в системах
натурального типа, к рассмотрению которых мы и переходим;
там мы увидим, в частности, что доказательство того же зако-
на тождества (AIDА) мы получим всего в два шага! Однако в
натуральных системах возникают свои трудности. Они связа-
ны с определением вывода. Обычно его определения получа-
ются здесь весьма усложненными. Дело в том, что, устраняя
из множеств возможных посылок выводов и доказательств
законы логики, мы должны использовать так называемые не-
прямые правила рассуждения (см. дальше). В силу этого
опять-таки происходит отдаление способов построения выво-
дов в этих исчислениях от естественных рассуждений. Мы
же даем здесь систему, которая максимально приближена к
естественным рассуждениям.

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

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

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