1.3.3. Логические исчисления и их интерпретация
В математической логике наиболее распространены три системы логического вывода: 1) исчисления гильбертовского типа, которые были предложены в работах Д. Гильберта и В. Аккермана [Гильберт, 1947]; 2) натуральное исчисление (или естественный вывод), разработанное логиком Г. Генценом [Генцен, 1967], и 3) логический вывод на основе принципа резолюции, ставший широко известным после публикации статьи М. Девиса и Х. Патнема [Davis, 1960]. Рассмотрим особенности логического вывода для систем перечисленных типов. Каждый из типов проиллюстрируем сначала на примере исчисления высказываний, а затем – исчисления предикатов.
Исчисления высказываний гильбертовского типа в современном варианте основаны на следующих аксиомах и правилах вывода:
Аксиомы:
(A1) A (B A);
(A2) (A (B C)) ((A B) (A C)); (A3) ( B A) (( B A) B).
Правила вывода:
правило подстановки: в любую аксиому или выведенную формулу можно вместо любого атома вставлять любое правильно построенное предложение;
модус поненс (MP): если A и A B – выводимые формулы, то B – выводимая формула.
Работу такой системы можно понять на следующем примере. Пусть необходимо вывести из приведенных выше аксиом теорему ├ A A. Вывод осуществляется по шагам:
1) (A ((A A) A)) ((A (A A)) (A A)) – подстановка в (A2)
A A вместо B и A вместо C;
2)A ((A A) A) – подстановка в (A1) A A вместо B;
3)(A (A A)) (A A) – применение MP к 2) и 1);
4)A (A A) – подстановка в (A1) A вместо B;
5)A A – применение MP к 4) и 3).
Важное место в исчислениях занимает теорема дедукции, впервые сформулированная и доказанная Ж. Эрбраном в 1930 г. Для исчисления
45
высказываний ее формулировка такова (приводится по книге [Клини, 1973]): Теорема 1.3. (теорема дедукции).
(a)Если A ├ B, то ├ A B;
(b)Если A1, ..., Am-1, Am ├ B, то A1, ..., Am-1├ Am B.
В исчислении предикатов в формулировку теоремы дедукции необходимо ввести некоторые дополнительные условия. Их мы рассмотрим позже.
Натуральное исчисление высказываний предназначено для того, чтобы приблизить формальное исчисление к естественному выводу. В этом исчислении состав правил вывода расширен, они имеют ясную интерпретацию на естественном языке, которая приведена в [Гладкий, 2001], и лежат в основе современной формальной теории доказательств [Такеути, 1978]. К тому же эти правила можно вывести как теоремы, используя исчисление гильбертовского типа. Для исчисления высказываний обычно применяются следующие правила вывода натурального исчисления.
Для произвольных формул A, B, C и некоторого множества формул применимы следующие правила вывода:
1) |
|
|
A,B |
|
|
|
2) |
|
A B |
; |
|
A B |
||
|
|
|
|
|
|
|
|
|
|
|
|
|||
|
A B |
|
|
|
|
A |
|
B |
||||||
введение конъюнкции (ВК); |
удаление конъюнкции (УК); |
|||||||||||||
3) |
|
|
A |
; |
B |
|
4) |
Если , A ├ C и , B ├ C, |
||||||
|
|
A B |
A B |
|||||||||||
|
|
|
|
|
|
|
|
|
|
|
||||
введение дизъюнкции (ВД) то , A B ├ C удаление дизъюнкции (УД), |
||||||||||||||
5) |
Если , A ├ B, то ├ A B |
6) |
|
A,A B |
|
|
|
|||||||
|
B |
|
|
|
|
|||||||||
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
введение импликации (ВИ); |
удаление импликации (УИ); |
|||||||||||||
7) |
Если , A ├ false, то ├ A |
8) |
A, A ├ false |
|||||||||||
введение отрицания (ВО); |
удаление отрицания (УО); |
|||||||||||||
9)false ├ A – правило Дунса Скотта (ДС);
10)├ A A – закон исключенного третьего (ИТ);
11)Если A – одна из формул в составе , то ├ A – правило тривиальной выводимости (ТВ).
Приведенные в скобках обозначения (ВК, УК, ВД и т.д.) – общеприняты в русскоязычной литературе по логическому выводу. Нетрудно видеть, например, что правило ВИ – один из вариантов теоремы дедукции, правило УИ
46
– правило модус поненс, правило ДС – формальный вариант известного логического принципа "из лжи можно вывести все, что угодно".
Обоснование аксиом исчисления высказываний легко выполнить на основе интерпретации этой системы – алгебры логики (см. п. 1.2.). Множество формул исчисления высказываний можно отобразить во множество формул алгебры логики, где переменным уже приписываются значения 1 (истина) или 0 (ложь), а формулам – некоторые таблицы истинности. При этом взаимосвязь между формулами исчисления высказываний и алгебры логики устанавливается с помощью теоремы 1.4 [Игошин, 2008].
Теорема 1.4. Всякая доказуемая в формализованном исчислении высказываний формула является тождественно истинной формулой (или тавтологией) алгебры логики.
Таким образом, можно сказать, что исчисление высказываний описывает способы получения всех возможных общезначимых формул.
Если определить логические связки " " и " ", то из аксиом (A1) – (A3) можно вывести как теоремы все основные законы алгебры логики (см. [Мендельсон, 1984]).
Для доказательства корректности того или иного вывода A1, A2, ..., An ├ An+1 можно использовать уже упомянутую теорему дедукции, которая позволяет во многих сложных случаях перейти от доказательства с помощью построения дерева вывода, не удобного для практических применений, к доказательствам с помощью алгебраических методов, в частности, к подтверждению или опровержению общезначимости логической формулы, полученной с помощью теоремы дедукции. Поясним сказанное на примере. Пусть имеется вывод: A, B ├ C. Тогда, согласно теореме дедукции, имеем A ├ B C. Применив еще раз эту теорему, получим ├ A (B C). С учетом теоремы 1.4, для обоснования корректности вывода ├ A (B C) необходимо установить общезначимость формулы алгебры логики A (B C).
В исчислении высказываний корректность тех или иных правил вывода также можно проверять алгебраически с помощью теоремы дедукции, подобно тому, как на основе законов алгебры множеств производится обоснование правил силлогистики (см., например, [Поспелов, 1989]).
Часто для доказательств с использованием алгебраических методов применяется не сама теорема дедукции, а ее следствия: теоремы 1.5 и 1.6. Эти
47
теоремы приведены в [Чень, 1983]. |
|
|
|
|
|
|
|
Теорема 1.5. Пусть даны формулы F1, ..., Fn |
и формула G. G есть |
||||||
логическое |
следствие F1, ..., Fn |
тогда |
и |
только |
тогда, |
когда |
формула |
((F1 ... Fn) G) общезначима. |
|
|
|
|
|
|
|
Теорема 1.6. Пусть даны формулы F1, ..., Fn |
и формула G. G есть |
||||||
логическое |
следствие F1, ..., Fn |
тогда |
и |
только |
тогда, |
когда |
формула |
(F1 ... Fn G) противоречива.
Формально исчисление предикатов можно представить как некоторое усложнение исчисления высказываний. Переход к исчислению предикатов означает ввод двух новых обязательных условий: 1) переход к фиксированным отношениям (предикатам) и 2) введение кванторов. Это отличие принципиально даже в тех случаях, когда в моделируемой системе область определения каждой переменной содержит ровно два элемента. Правила логического вывода для исчисления предикатов не во всех случаях применимы для систем с бинарными областями значений переменных.
В исчислении предикатов аксиомы и правила логического вывода исчисления высказываний остаются без изменений, к ним только добавляются новые аксиомы и правила вывода. Их формулировка для исчислений предикатов гильбертовского типа не во всех источниках одинакова,
приведем их по [Мендельсон, 1984].
Аксиомы:
(A4) xiA(xi) A(t), где A(xi) есть формула, содержащая свободную переменную xi, а t — терм, свободный для xi в A(xi); в частности, если t = xi, то данная аксиома выражается как xiA(xi) A(xi).
(A5) xi( A B) (A xiB), если в формуле A не содержится свободных вхождений переменной x.
Правило вывода (обобщения): из A следует xiA. Другое название этого правила – правило связывания квантором всеобщности.
Правило обобщения само по себе трудно объяснимо. Если формула A содержит свободную переменную xi (в формулировке правила это допускается), то в случае, когда формула A такова, что xiA противоречива, получается явная нелогичность. Например, из утверждения "Грибы мухоморы ядовиты" выводится утверждение "Все грибы ядовиты", но поскольку последний тезис ложен, то из этого следует, что из любой логической формулы, в которой
48
переменная xi не пробегает всех своих значений, выводится ложь.
Эту несообразность в исчислении гильбертовского типа в какой-то степени исправляет теорема дедукции для исчисления предикатов [Мендельсон, 1984]:
Теорема 1.7. Если , A ├ B и существует вывод, построенный без применения правила обобщения к свободным переменным формулы A, то
├ A B.
Из формулировки теоремы ясно, что правило обобщения к посылкам применяется не во всех случаях. Получается, что необъяснимая ситуация, связанная с правилом обобщения в исчислениях гильбертовского типа, корректируется с помощью теоремы дедукции.
В натуральном исчислении предикатов такого несоответствия нет.
Кванторные правила вывода в нем |
уже не вызывают подобных вопросов |
(приводятся по [Гладкий, 2001]): |
|
12) Если ├ A(x) и переменная x |
13) Если подстановка переменной y |
не входит свободно ни в одну |
вместо переменной x корректна, |
из формул , то ├ xA(x); |
то xA(x) ├ A(y); |
введение общности (В ) |
удаление общности (У ) |
14) Если подстановка переменной |
15) Если , A(x) ├ B и переменная x |
x вместо переменной y корректна, |
не входит свободно ни в одну |
то A(y) ├ xA(x); |
формулу из , то xA(x) ├ B. |
введение существования (В ); |
удаление существования (У ) |
Здесь правило вывода В полностью соответствует теореме дедукции для исчисления предикатов. Подробное объяснение смысла этих правил вывода и примеры можно найти в [Гладкий, 2001].
Считается, что формулы исчисления предикатов имеют смысл (можно судить об их выполнимости), если задана какая-либо интерпретация входящих в них символов, т.е. термов, предикатов, функций, констант и т.д. В п. 1.3.1 уже приводилось общепринятое определение понятия "интерпретация" для исчисления предикатов, согласно которому алгебраическая система
B= <A, F, P> является интерпретацией, если:
1)каждой предметной константе соответствует некоторый элемент из A;
2)каждой переменной соответствует область определения, равная A;
3)каждой m-местной функции соответствует отображение Am в A
(операция);
49