4. Аксиомы и правила вывода исчисления секвенций

Определение 4.1. (1) Секвенцией называется выражение вида , где Р и Q – два множества формул.

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

Соответственно, задача поиска контрпримеров к формуле q – секвенция .

(2) Правилами вывода исчисления секвенций называются следующие восемь правил:

(С+) ,

(С–) ,

(D+) ,

(D–) ,

(I+) ,

(I–) ,

(N+) ,

(N–) .

Замечание. Предположим, что мы ищем контрпример к секвенции вида . Один из вариантов – поискать наборы, на которых ложна формула . Это в точности те наборы, на которых истинна r и ложна s, то есть – контрпримеры к секвенциям и (одновременно!). Отсюда правило . Остальные правила получаются аналогично.

(3) Объяснение. Аксиомой исчисления секвенций естественно счесть любую секвенцию, которой не соответствует никаких контрпримеров. Таковыми, например, являются секвенции, для которых .

Итак, аксиомой исчисления секвенций называется любая секвенция , такая, что .

(4) В результате обработки формулы исчисление секвенций формулы получается своеобразное «дерево вывода».

Примеры. (1) . Обе секвенции и – аксиомы, поэтому формула есть тавтология (ибо к ней не существует контрпримеров). В этом случае говорят, что рассмотренная формула есть теорема исчисления секвенций.

(2) . Секвенция имеет контрпример: р и q – ложны. Следовательно, он будет и контрпримером к формуле . Это так и есть .

Следующая теорема очевидна.

Теорема 4.1. (Корректность и полнота исчисления секвенций)

Секвенция выводима тогда и только тогда, когда она не имеет контрпримера.

Замечание. Из этой теоремы можно получить ещё одно доказательство теоремы о полноте исчисления высказываний. Это немного хлопотно, поскольку секвенции – это всё-таки не формулы и доказательство в исчислении секвенций формально не имеет ничего общего с доказательством в исчислении высказываний. Тем не менее, родство двух исчислений несомненно существует, и доказательства в них, в содержательном смысле, всё-таки примерно одно и то же .

§5. Интуиционистская пропозициональная логика

1. Обсуждение

Одна из аксиом пропозициональной логики (да, собственно, и всей классической математики), конкретно – аксиома (А11), стала однажды в истории предметом нешуточного обсуждения, чтобы не сказать – конфликта. Один из крупнейших математиков XX века Л.Э.Я. Брауэр увидел в её использовании причину появления странных математических результатов, подобных теореме Банаха-Тарского (эти два математика однажды объяснили миру, что шар можно разрезать на конечное множество частей, из которых можно сложить два таких же шара). Брауэр на основании кажущейся абсурдности подобных результатов (в действительности теорема Банаха-Тарского отнюдь не абсурдна: части, на которые делится шар, не имеют никакого объёма, поэтому объём и не обязан сохраняться при их перекладывании в другом порядке) счёл, что математические рассуждения утратили некий исходный «интуитивный смысл» и предложил к нему некоторым образом вернуться. Например, ощущение того, что всякое утверждение может быль либо истинным, либо ложным, подтверждается, в действительности, только сравнительно простыми примерами (правда, можно заметить, что в мире почти всё просто ). С другой стороны, существует по меньшей мере один результат (недоказуемость и неопровержимость континуум-гипотезы: «существует несчётное подмножество R, неравномощное R»), который можно (при желании) счесть подтверждением противоположной точки зрения. Поэтому – вполне допустима такой взгляд на вещи: существуют утверждения, не являющиеся ни истинными, ни ложными. «Неизвестно» . Может быть, континуум-гипотеза – не истинная и не ложная, «никакая»!

Итак, возможно, что аксиома (А11) «в действительности места не имеет», и от её использования следует воздерживаться. С другой стороны, Брауэр проницательно заметил, что доказательства всех «странных» теорем используют эту аксиому. «Все люди, умершие в двадцатом веке, ели сахар. Естественно предположить, что от этого они и умерли. Сахар – белая смерть двадцатого века!»

То, что остаётся от классической математической логики в результате такого «воздержания от употребления сахара», называется интуиционистской (или конструктивистской) логикой. Почему вообще что-то остаётся? Потому что даже в рассмотренных примерах упомянутая аксиома использовалась далеко не всегда.

Противоположный вопрос тоже уместен: а почему, собственно, исключение аксиомы (А11), хоть что-то меняет? Может быть эта аксиома выводится из остальных?

Теорема 5.1. Формула невыводима в интуиционистской пропозициональной логике.

Доказательство. Изменим смысл всех символов (научно говоря, построим другую модель аксиоматики). Предположим, что истинность высказывания бывает не двух, а трёх типов: «истинно» (1), «ложно» (0) и «неизвестно» (? или ). Далее, истинность сложных высказываний можно задать таблицей (любой, лишь бы остальные аксиомы выдержали предлагаемые изменения).

0	1
?	0
1	0

0	0	0	0	1
0	?	0	?	1
0	1	0	1	1
?	0	0	?	0
?	?	?	?	1
?	1	?	1	1
1	0	0	1	0
1	?	?	1	?
1	1	1	1	1

Почему именно так? Некоторые правила хорошо понятны: , , , (считая, что 0<?<1), , . По поводу остальных правил можно сказать: делать можно как угодно, лишь бы результат получился нужный . Отметим, однако, что ожидаемое неприемлемо: аксиома (А9) при и становится ложной.

Формулу назовём 3-тавтологией, если на любом наборе аргументов она принимает значение 1. Теперь нужно проверить две вещи. Во-первых – то, что все аксиомы, кроме (А11) являются 3-тавтологиями. Это длинная рутинная процедура, и она оставляется читателю в качестве самостоятельного, обязательного для исполнения упражнения. Во-вторых – состоятельность правила МР. Она очевидна: если и , то обязательно , так как .

Следовательно, любая выводимая формула является 3-тавтологией. Осталось заметить, что аксиома (А11) 3-тавтологией не является: .

QED

Замечание. Формула , которая тоже невыводима в интуиционистской логике (почему?), тем не менее, является 3-тавтологией (проверьте). Можно сказать, что нам просто повезло с законом исключённого третьего: его невыводимость доказалась так легко . В общем же случае потребуется какой-то более мощный инструмент.