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

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

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

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

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

(С+) ,

(С–) ,

(D+) ,

(D–) ,

(I+) ,

(I–) ,

(N+) ,

(N–) .

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

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

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

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

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

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

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

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

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

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

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

Обсуждение

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

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

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

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

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

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

?

	?		?
?			?
?	?	?	?
?		?
	?	?		?

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

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

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

QED

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

Модели Крипке

Определение 5.1.(1)Пусть – частично-упорядоченное множество, называемое множеством миров. Каждый мир есть разбиение множества V всех пропозициональных переменных на два подмножества: истинных и ложных (в этом мире) переменных. Истинность переменной x (и формулы тоже) в мире w символически записывается формулой . Этот объект называется шкалой Крипке, если выполнено условие:

– , , – истинность наследуется вверх по шкале.

(2) Пусть – шкала Крипке, p – пропозициональная формула. Истинность формулы р в мире w этой шкалы определяется индуктивно:

а) формула О ложна, а I – истинна во всех мирах;

б) формула x, где , истинна в мире w тогда и только тогда, когда ;

в) и ;

г) или ;

д) если , то ;

е) ни в одном мире формула р не является истинной.

(3) Множество всех миров шкалы, на которых истинна формула р, называется областью истинности этой формулы.

Лемма 5.2. Область истинности любой формулы – двойственный идеал частично-упорядоченного множества , то есть если , , то .

Доказательство.Индукция по построению формул. База содержится в определении. Переход для импликации и отрицания – тоже. Дизъюнкции и конъюнкции соответствуют объединение и пересечение идеалов, которые тоже, очевидно, являются идеалами.

QED

Шкалы Крипке имеют простой наглядный «философский» смысл. Множество W можно понимать как множество всевозможных логически непротиворечивых ступеней развития некой цивилизации. Неравенство означает, что ступень v может получиться из ступени u в процессе развития этой цивилизации. При этом уж если формула доказана, то она так и останется истинной (то есть – цивилизация не совершает ошибок). Но, наверное, есть какие-то обстоятельства, которые так и останутся от неё сокрыты…

Теорема 5.3. (О корректности интуиционистского исчисления высказываний относительно шкал Крипке)

Формула, выводимая в интуиционистском исчислении высказываний, истинна во всех мирах всех шкал Крипке.

Доказательство.Достаточно проверить, что все аксиомы истинны во всех мирах, а правило МР это свойство сохраняет. Второе очевидно следует из определения импликации, и миры и шкалы тут вообще ни при чём.

Проверим аксиому (А1). Если формула р истина в некотором мире, то во всех бòльших мирах истинна и формула , а, следовательно – и формула . Если же р ложна, то импликация истинна в любом случае.

Проверим аксиому (А2). Аналогично предыдущему, достаточно рассмотреть только те миры, в которых истинна формула . Итак, пусть . Покажем, что в этом случае . Это означает, что . В силу произвольности v это то же самое, что . При этом снова достаточно рассмотреть только те миры, в которых . Итак, достаточно рассмотреть только те миры, в которых , среди них – только те, в которых , и только те из них, в которых . Из первого условия следует, что во всех таких мирах , из третьего – что в них , следовательно, в них . Итак, из всегда следует , значит во всех рассматриваемых мирах , что и требовалось доказать.

Остальные аксиомы разбираются аналогично.

QED

Примеры.(1) Шкала Крипке, в одном из миров которой ложна формула строится легко. Возьмём два мира, первый меньше второго. Пусть формула p истинна только во втором мире. Тогда формула не истинна нигде, а истинна только во втором мире. В действительности – это уже приведённое рассуждение: 0 – значение формулы, ложной в обоих мирах, 1 – истинной в обоих мирах, ? – истинной только во втором мире.

(2) Аналогичная шкала Крипке для формулы устроена немного сложнее. Рассмотрим три мира: u, v, w, такие что , , а миры v и w несравнимы. Далее, пусть формула р (и, следовательно, , так как импликация выводима в интуиционистской логике) истинна только в мире v, а формула – только в мире w. В итоге получается, что в мире u обе формулы и ложны, следовательно – ложна и исходная формула.

Не нашли, что искали? Воспользуйтесь поиском по сайту: