2.2.2 Проверка доказательных рассуждений

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

Пример 2.4. [K78] Рассмотрим рассуждение: “Если бы он не сказал ей, она бы и не узнала. А не спроси она его, он и не сказал бы ей. Но она узнала. Следовательно, она спросила.” Это сложное рассуждение представляет собой конъюнкцию трех утверждений, за которыми следует некоторый вывод. Представим рассуждение структурно в табл. 2.3:

Таблица 2.3

F1:	Если бы он не сказал ей, она бы и не узнала.
F2:	А не спроси она его, он и не сказал бы ей.
F3:	Но она узнала.
R:	Следовательно, она спросила.

В предложениях можно выделить атомы (элементарные высказывания): “он сказал ей” (Ск), “она узнала” (У), “она спросила” (Сп), и, кроме того, отдельные утверждения F1, F2, F3 и вывод R. Схема, модель этого рассуждения приведена в табл.2.4. Кроме логических связок отрицания и импликации в схему входит символ “”, заменяющий “Следовательно”. Он показывает, что в рассуждении утверждается, что формула, стоящая за ним, является следствием приведенных ранее утверждений. 

Таблица 2.4

F1:	СкУ
F2:	СпСк
F3:	У
R:	 Сп

Одной из главных проблем логики, сформулированной еще великим Аристотелем, является разработка методов определения того, является ли заключительное утверждение (R) действительно следствием высказанных утверждений единственно в силу формальной структуры рассуждения при условии истинности приведенных фактов, а не исходя из смысла утверждения R или фактов F1, F2, F3. Формальная логика как раз позволяет определить это, т.е. логика позволяет определить, является ли утверждение R логическим следствием фактов F1, F2, F3.

Пример 2.5. Рассмотрим другое рассуждение: “В хоккей играют настоящие мужчины. Трус не играет в хоккей. Я в хоккей не играю. Значит, я трус(?!)” Элементарными высказываниями здесь будут: “я играю в хоккей (Х)”, “я -настоящий мужчина, не трус (М)”. Схема этого рассуждения:

Таблица 2.5

F1:	ХМ
F2:	МХ
F3:	Х
R:	 М

Если согласиться с посылками рассуждения, то следует ли из посылок его вывод? 

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

Силлогизмы. Силлогизмы - это правильные схемы рассуждений. Исторически впервые силлогизмы исследовались еще Аристотелем и имели вполне определенную фиксированную форму, описываемую предикатами. В этой главе мы под силлогизмами будем понимать исторически сложившийся стандартный, фиксированный набор схем рассуждений, в которых заключение всегда верно в силу именно формы рассуждения, а не его содержания. Рассмотрим следующие силлогизмы:

РQ	модус поненс (способ спуска)
P
 Q

РQ	модус толленс
Q	(доказательство от противного)
 Р

РQ	дизъюнктивный силлогизм
Р
 Q

РQ	гипотетический силлогизм
QR	(транзитивность импликации)
 РR

РQ	разделительный силлогизм
Р
 Q

РQ	простая дилемма
RQ
PR
 Q

РQ	конструктивная дилемма
RS
PR
 QS

РQ	деструктивная дилемма
RS
QS
 PR

Рассуждения, построенные на основе силлогизмов, правильны именно в силу своей структуры. Применение в рассуждениях таких стандартных схем гарантирует правильность полученных выводов. Если рассуждение построено не в соответствии со схемой силлогизма, можно попытаться последовательным применением нескольких силлогизмов доказать справедливость заключения. Для рассуждения “Узнала - спросила” из F2 и F1 в соответствии с правилом вывода «гипотетический силлогизм» можем заключить, что утверждение “F4: СпУ” истинно. Далее, пара утверждений F4 и F3 в соответствии с модус толленс гарантирует истинность заключения R этого рассуждения.

Однако, подбор правильных образцов рассуждений - силлогизмов не является систематическим методом, позволяющим всегда ответить на вопрос, является ли схема данного рассуждения правильной, если она не совпадает ни с одним из указанных силлогизмов. Например, в рассуждении “о хоккее” справедливо ли утверждать, что не играющий в хоккей - трус? Хотя схема этого рассуждения не совпадает ни с одним силлогизмом, уже в предыдущем примере мы видели, что не все правильные схемы рассуждений задаются силлогизмами. В действительности, правильных схем рассуждений бесконечное количество. Далее мы рассмотрим систематические методы проверки правильности рассуждений, применимые к любым схемам рассуждений.

Логическое следствие.

Определение 2.3.. Формула R называется логическим следствием формулы Ф (или: R логически следует из Ф), тогда и только тогда, когда для всякой интерпретации, на которой формула Ф истинна, R тоже истинна. 

Очевидно, что сама формула является логическим следствием самой себя, причем наиболее сильным следствием. Наиболее слабым следствием любой формулы является тавтология - тождественно истинная функция. Например, человек, выводящий из фактов только тривиальную истину, всегда прав. С другой стороны, из ложных фактов можно вывести любое утверждение. Например, знаменитый пример Гильберта “Если 2*2=5, то Луна сделана из зеленого сыра” с точки зрения логики является совершенно правильным умозаключением.

Теорема 2.1. Логическим следствием формулы Ф является False тогда и только тогда, когда Ф невыполнима.

Доказательство этой теоремы легко провести на основании определения 2.3. 

Очевидно, что если формула Ф невыполнима, то кроме False из нее можно получить любые следствия.

Определение 2.4. Формула R называется логическим следствием формул F₁, F₂, ..., F_k (или: R логически следует из F₁, F₂, ..., F_k), тогда и только тогда, когда для всякой интерпретации, на которой формула F₁&F₂&...&F_k истинна, R тоже истинна. 

Из определения 2.4 очевидно, что наиболее сильным логическим следствием нескольких фактов является просто конъюнкция этих фактов.

Пример 2.6 [C85]. Инспектора Крейга из Скотланд-Ярда направили для проверки лечебницы для умалишенных. Каждый из обитателей лечебницы - врач либо пациент - мог быть либо здоров, либо лишен рассудка. Если он был здоров, то говорил правду, если лишен рассудка, то только лгал.

В лечебнице Крейг побеседовал с двумя обитателями, Джонсом и Смитом. Джонс сказал, что Смит - один из врачей больницы, а Смит сказал, что Джонс - пациент. Поразмыслив, Крейг догадался, что либо в клинике или есть доктора, лишенные рассудка, или пациенты, которые нормальны (очевидно, и то, и другое следует пресекать). Как он догадался об этом? В [C85] приведено долгое рассуждение, обосновывающее вывод инспектора. Однако, вывод этот можно получить чисто механически. Действительно, обозначим:

Дд - Джонс доктор (следовательно, Дд - Джонс пациент);

Нд - Джонс нормален (следовательно, Нд - Джонс болен);

Дс -Смит доктор (следовательно, Дс - Смит пациент);

Нс -Смит нормален (следовательно, Нс - Смит болен).

Информация, полученная Крейгом, сводится к четырем фактам:

1) Нд  Дс;

2) Нд Дс;

3. Нс Дд;

4. Нс  Дд.

Какой вывод можно сделать из этих фактов? Для построения наиболее сильного следствия возьмем их конъюнкцию:

(НдДс)(НдДс)(НсДд)(НсДд) =

(НдДс)(НдДс)(НсДд)(НсДд) =

(НдДс ДсНд)(НсДд ДдНс) =

НдДсНсДдНдДсДдНс ДсНдНсДд  ДсНдДдНс.

Первый терм говорит о том, что Джонс доктор, но ненормальный, последний - что он пациент, но нормален. Второй и третий термы говорят подобное же о Смите. Их дизъюнкция говорит о том, что по крайней мере одна из этих возможностей реализуется. Каждая из них аномальна. Поэтому у инспектора Крейга есть все основания для расследования. 

Пусть теперь мы имеем произвольную схему рассуждений. Определение 2.4 дает нам возможность систематической проверки правильности любой схемы рассуждений с высказываниями, например, по таблице истинности. Построим таблицы истинности формул F₁&F₂&...&F_k и R для рассуждения “Узнала - спросила” примера 2.1 (табл.2.6).

Таблица 2.6

Формула F1&F2&F3 истинна в табл.2.6 только на последней интерпретации аргументов, и на этой же интерпретации R тоже истинна. Следовательно, схема для рассуждения “Узнала - спросила” правильна, вывод с необходимостью следует из истинности фактов. Заключительное утверждение здесь является новым знанием, оно не проверялось в реальной жизни специально: проверялись другие, а это является логическим следствием указанных фактов. Для того, чтобы сделать вывод о его истинности, достаточно только убедиться в истинности других высказываний (фактов): F1, F2, F3. Конечно, формальная логика не может гарантировать, что эти высказывания истинны - определение этого выходит за рамки логики, но уж если их истинность установлена, то истинность результата R можно не устанавливать: она будет следовать формально.

Проанализируем рассуждение “о хоккее” примера 2.2. Построим таблицу истинности:

Таблица 2.7

Табл. 2.7 показывает, что в этом рассуждении вывод не является логическим следствием утверждений F1, F2, F3. Интерпретация (f,t) является контрпримером: на ней все факты истинны, а утверждение R - ложно. Это означает, что установить, является ли говорящий трусом или мужчиной, считая истинными только высказывания F1, F2 и F3 этого утверждения, нельзя, решение этой проблемы требует привлечения каких-то других фактов. Интересно, что хотя две строки этой популярной песни: “В хоккей играют настоящие мужчины,” и “Трус не играет в хоккей” звучат по-разному, с логической точки зрения они не отличаются: соответствующие логические функции ХМ и МХ эквивалентны, одна является контрапозицией другой.

Используя таблицы истинности, легко проверить, что каждый приведенный выше силлогизм является “правильной” схемой рассуждений. Читатель может на основании этого подхода с построением таблиц истинности легко придумать свои правильные схемы рассуждений.

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

Основная теорема логического вывода

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

Теорема 2.2. Формула R является логическим следствием формул F₁, F₂, ..., F_k тогда и только тогда, когда формула F₁F₂...F_kR общезначима.

Доказательство. (Необходимость). Предположим, что R является логическим следствием формулы F₁F₂...F_k., и докажем при этом предположении, что F₁F₂...F_kR общезначима. Пусть I есть произвольная интерпретация атомов. Если все F₁,F₂,...,F_k истинны на I, то F₁F₂...F_k истинна на I и по определению логического следствия R истинна на I, и, следовательно, на этой интерпретации F₁F₂...F_kR истинна. Если же хотя бы одна F_i ложна на I, то на этой интерпретации F₁F₂...F_k ложна, но F₁F₂...F_k R также истинна независимо от R в силу определения импликации. Следовательно, на I формула F₁F₂...F_kR истинна. В силу произвольности интерпретации I этот вывод справедлив для всякой интерпретации, поэтому формула F₁F₂...F_kR общезначима.

(Достаточность). Предположим, что формула F₁F₂...F_kR общезначима. Тогда для всякой интерпретации, на которой все F_i истинны, формула F₁F₂...F_k тоже истинна, и тогда поскольку F₁F₂...F_kR общезначима, на этой интерпретации R тоже истинна в силу определения импликации. 

Теорема 2.3. Формула R является логическим следствием формул F₁, F₂, ..., F_k тогда и только тогда, когда формула F₁F₂...F_kR невыполнима.

Доказательство. По теореме 2.2 формула R является логическим следствием формул F₁, F₂, ..., F_k тогда и только тогда, когда формула F₁F₂...F_kR общезначима или, что то же, отрицание формулы F₁F₂...F_kR невыполнимо. Но по закону де Моргана (F₁F₂...F_kR) эквивалентно F₁F₂...F_kR. Теорема доказана. 

На основании теорем 2.2 и 2.3 вопрос о правильности схемы рассуждения сводится к проверке общезначимости либо невыполнимости некоторой формулы. Эта проверка может быть выполнена множеством различных способов.

Приведение к нормальным формам

Как, анализируя формулу в нормальной форме, можно сделать вывод о ее общезначимости или невыполнимости? Возьмем ДНФ, т.е. представление формулы в виде дизъюнкции конъюнкций К₁К₂...K_n. Для того, чтобы сделать вывод о ее общезначимости, нужно анализировать всю формулу целиком: каждая конъюнкция общезначимой формулы может быть истинной только на нескольких интерпретациях. В то же время, вывод о невыполнимости дизъюнкции конъюнкций можно сделать легко: каждая конъюнкция ДНФ невыполнимой функции должна быть невыполнима, а это очень легко проверить: конъюнкция литер невыполнима тогда и только тогда, когда она содержит хотя бы одну пару противоположных литер. Полностью аналогично можно использовать представление в виде КНФ, но для определения общезначимости функции. Очевидными следствиями предыдущих теорем являются:

Теорема 2.3 Для того, чтобы формула R была логическим следствием формул F₁, F₂, ..., F_k, необходимо и достаточно, чтобы каждый конъюнкт дизъюнктивной нормальной формы представления формулы F₁F₂...F_kR содержал пару противоположных литер. 

Теорема 2.4 Для того, чтобы формула R была логическим следствием формул F₁, F₂, ..., F_k, необходимо и достаточно, чтобы каждый дизъюнкт конъюнктивной нормальной формы представления формулы F₁F₂...F_kR содержал пару противоположных литер. 

Пример 2.7 Докажем правильность схемы рассуждения “Узнала - спросила” примера 2.4 приведением к ДНФ: (СкУ) (СпСк)УСп = (СкУ)(СпСк)УСп =

(СкСпУСп)  (СкСкУСп)  (УСпУСп)  (УСкУСп).

Поскольку каждый конъюнкт содержит пару противоположных литер, эта формула невыполнима, и, следовательно, схема рассуждения “Узнала - спросила” правильна. Заметим, что это доказательство много проще построения и анализа таблиц истинности (таб.2.6). 

Метод резолюции

Этот метод использует тот факт, что если некоторая формула является невыполнимой, то наиболее сильное следствие этой формулы - константа False. Предложенный в 1965г. Дж. Робинсоном [R65] метод резолюции позволяет получить максимально сильное следствие множества формул с помощью систематической процедуры последовательного построения логических следствий формулы, называемых резольвентами. Иными словами, метод резолюции обладает свойством полноты: для формулы Ф следствие False обязательно будет получено, если Ф - невыполнима.

Теорема 2.4. Пусть В - логическое следствие формулы А. Тогда А&В  А.

Доказательство теоремы легко проводится на основании определения понятия логического следствия. Действительно, пусть условие теоремы выполнено. Тогда в соответствии с теоремой 2.1, АВ  True. Отсюда АА&TrueА&(АВ) А(АВ) А&АА&ВFalseА&ВА&В. 

Определение 2.5. Резольвентой двух дизъюнктов D1L и D2L называется дизъюнкт D1D2. 

Теорема 2.5. Резольвента является логическим следствием порождающих ее дизъюнктов.

Доказательство. Пусть D1L и D2L - два дизъюнкта. Тогда D1D2 - их резольвента. Легко показать, что формула (D1L)&(D2L)(D1D2) общезначима. По теореме 2.1 отсюда следует заключение теоремы. 

Метод резолюции доказательства невыполнимости формулы Ф=F₁F₂...F_kR состоит в том, что формула Ф представляется в КНФ, и к ней конъюнктивно присоединяются все возможные резольвенты ее дизъюнктов и получаемых в процессе доказательства резольвент. Полнота метода резолюции состоит в том, что он гарантирует получение для формулы Ф следствия False, если Ф - невыполнима. Если же, перебрав все возможные резольвенты формулы Ф, мы не нашли пустую резольвенту, то Ф не является невыполнимой.

Пример 2.8. Доказательство правильности рассуждения “Узнала - спросила” сводится к проверке невыполнимости формулы Ф=F1&F2&F3&R, где F1=СкУ, F2=СпСк, F3=У и R= Сп.

Перечислим все дизъюнкты конъюнктивной нормальной формы Ф и построим возможные резольвенты:

Доказательство методом резолюции сделаем более наглядным, представив его графически:

Рис.2.2. Графическое представление доказательства методом резолюции

Доказательство методом резолюции очень близко обычному словесному доказательству от противного. Это демонстрирует интерпретация последовательных формул вышеприведенной таблицы. Проинтерпретируем еще раз это доказательство в естественном языке по графу рис.2.2.

Рассуждение: “Если бы он не сказал ей, она бы и не узнала. А не спроси она его, он и не сказал бы ей. Но она узнала. Следовательно, она спросила.”

Доказательство (см. рис.2.2): “Предположим противное, т.е. что она не спросила. Тогда из второго утверждения следует, что он ей не сказал. Отсюда, и из первого утверждения следует, что она не узнала. Но в третьем утверждении говорится, что она узнала. Таким образом, предположив, что следствие неверно, мы пришли к противоречию. Поэтому следствие верно.”

Для рассуждения примера 2.2: “В хоккей играют настоящие мужчины. Трус не играет в хоккей. Я в хоккей не играю. Значит, я трус(?!)” метод резолюции дает (см таб.2.5):

(1) ХМ - первое утверждение: “В хоккей играют настоящие мужчины”;

2. МХ - второе утверждение: “Трус не играет в хоккей”;

3. Х - третье утверждение: “Я в хоккей не играю”;

4. М - отрицание следствия: “Предположим, что неверно, что "Я трус" ”;

Резольвент нет

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

Определение 2.6. Пусть S - множество дизъюнктов. Резолютивный вывод С из S есть такая конечная последовательность С₁,...,С_k дизъюнктов, что С_k = C и каждый дизъюнкт С_i или принадлежит S или является резольвентой дизъюнктов, предшествующих С_i. Вывод пустого дизъюнкта из S называется опровержением S. 

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

Теорема 2.6 (о полноте метода резолюции). Множество дизъюнктов S невыполнимо тогда и только тогда, когда существует резолютивный вывод пустого дизъюнкта из S.

Необходимость. Доказательство того, что при невыполнимости S всегда найдется резолютивный вывод пустого дизъюнкта из S за конечное число шагов, здесь опускается.

Достаточность. Пусть из S существует резолютивный вывод пустого дизъюнкта. Докажем, что S невыполнимо. Поскольку резольвента  есть логическое следствие порождающих ее дизъюнктов D_i и D_k, то конъюнктивное присоединение резольвенты  к формуле S не меняет ее значения, поскольку S=AD_iD_k, а D_iD_kD_iD_k согласно теоремам 2.4 и 2.5. Если среди резольвент Ф существует пустая резольвента, соответствующая ее логическому следствию False, то Ф невыполнима, поскольку эквивалентна формуле с конъюнктивным членом False. 

Перебор всех возможных резольвент можно организовать по-разному, и разные стратегии построения резольвент будут (в среднем) иметь различную эффективность (число шагов вывода до получения положительного или отрицательного ответа). Одной из наиболее эффективных стратегий является стратегия движения “от цели” - получение на каждом шаге резольвент из двух дизъюнктов, один из которых - это цель доказательства (инверсия предполагаемого следствия) или резольвента-потомок этой цели. Эта стратегия особенно эффективна в языках логического программирования, где только небольшое число фактов общей базы данных действительно имеют отношение к заданному вопросу. Мы рассмотрим использование метода резолюции в языках логического программирования ниже.

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

Адекватность логики высказываний. Вопрос об адекватности математической модели при решении конкретных проблем в реальной жизни, как уже говорилось выше, лежит вне самого математического аппарата, это проблема, которую должен решать человек, использующий этот аппарат для решения задач практики. В области формализации рассуждений естественного языка всегда надо быть осторожным, применяя выводы логики высказываний к реальной жизни. Хорошую иллюстрацию этому дает так называемая “задача Кислера”, приведенная в монографии С. Клини “Математическая логика”. Рассмотрим ее в несколько измененной постановке.

Браун, Джонс и Смит обвиняются в преступлении. На допросе они под присягой дали показания:

Браун: Джонс виновен, а Смит невиновен (Д&С).

Джонс: Браун без помощи Смита это не смог бы сделать (БC).

Смит: Я невиновен, но кто-то из них виновен (C&(БД)).

Из этих утверждений следует, что виноват Джонс, а двое других подозреваемых невиновны (докажите!). Но задумаемся, действительно ли мы можем считать эти посылки истинными? Что, если виновный лжет, а невиновный говорит правду? В этом случае нахождение максимально сильного следствия шести посылок:

F1:Б(Д&С); F3:Д(БC); F5:СC&(БД);

F2: Б(Д&С); F4: Д(БC); F6: С(C&(БД));

приводит к полностью противоположному выводу. Если же мы будем полагаться на информацию только тех, кто невиновен (т.е учитывать только утверждения F1, F3, F5), то мы получим третий результат: установить в точности, кто виновен, без дополнительной информации нельзя. Таким образом, результаты анализа одной и той же ситуации с привлечением одного и того же аппарата - логики высказываний - существенно меняются в зависимости от того, как мы формализуем задачу проверки правильности рассуждений, какие факты мы будем считать установленными.

Другим примером, иллюстрирующим это положение, является доказательство древнегреческого философа Зенона того, что движения нет: “Если тело движется, то движение может происходить либо там, где тело есть, либо там, где тела нет. Но движение не может происходить там, где тело есть, потому что тогда бы оно стояло на месте. Движение не может также происходить там, где тела нет: если там тела нет, то как оно может там двигаться?. Следовательно, тело двигаться не может”. Логическая структура этого доказательства совершенно правильна, но формальная логика не может отвечать за то, что содержание умозаключения неверно. Движение все же есть!