В этом разделе мы построим другой вариант исчисления высказываний — так называемое исчисление секвенций. Такого рода исчисления изучаются в теории доказательств. Они оказываются более удобными для анализа синтаксической структуры выводов. Их называют исчислениями генценовского типа (по имени Генцена, который начал их изучать). Ранее приведенный вариант исчисления высказываний называют исчислением гильбертовского типа (по имени Гильберта, который использовал подобные исчисления в своей программе формального построения математики).
Для начала мы вообще не будем говорить ничего об аксиомах и
правилах вывода, а рассмотрим задачу поиска контрпримера. Пусть
дана некоторая формула $$A$$, про которую мы подозреваем, что она
не является
Введем необходимую терминологию и обозначения. Будем называть секвенцией выражение $$\Gamma\vdash\Delta$$, где $$\Gamma$$ и $$\Delta$$ — некоторые конечные множества формул. (Пока что знак $$\vdash$$ не имеет ничего общего с выводимостью, а только разделяет два множества формул.) С каждой секвенцией $$\Gamma\vdash\Delta$$ будем связывать задачу поиска таких значений переменных, при которых все формулы из $$\Gamma$$ истинны, а все формулы из $$\Delta$$ ложны. Такой набор значений мы по некоторым причинам будем называть контрпримером к секвенции $$\Gamma\vdash\Delta$$. Легко проверить, что контрпримеры к секвенции $$\Gamma\vdash\Delta$$ — это контрпримеры к формуле$$\land \Gamma\to\lor\Delta,$$ ( $$\land\Gamma$$ обозначает конъюнкцию формул из $$\Gamma$$, а $$\lor\Delta$$ — дизъюнкцию формул из $$\Delta$$ ), то есть те наборы значений, при которых эта формула ложна. При этом конъюнкцию пустого множества формул мы считаем тождественно истинной, а дизъюнкцию — тождественно ложной.
Наша исходная задача поиска контрпримера к формуле $$A$$ может быть теперь сформулирована как задача поиска контрпримера к секвенции $$\vdash A$$. (Мы позволяем себе писать так для краткости; полностью следовало бы написать $$\varnothing\vdash\{A\}$$.)
Задачу поиска контрпримера к секвенции можно решать с помощью следующих правил. В каждом из приведенных правил нижний заказ на контрпример выполним, если и только если выполним один из верхних заказов, т. е. нижняя секвенция имеет контрпример тогда и только тогда, когда хотя бы одна из верхних секвенций имеет контрпример.$$\begin{align*} \frac{\Gamma\vdash A,\Delta\qquad \Gamma\vdash B,\Delta} {\Gamma\vdash A\wedge B,\Delta} \qquad\qquad \frac{A,B,\Gamma\vdash\Delta} {A\wedge B,\Gamma\vdash\Delta} \\[0.7ex] \frac{\Gamma\vdash A, B,\Delta} {\Gamma\vdash A\vee B,\Delta} \qquad\qquad \frac{A,\Gamma\vdash \Delta\qquad B,\Gamma\vdash \Delta} {A\vee B,\Gamma\vdash \Delta} \\[0.7ex] \frac{\Gamma,A\vdash B,\Delta} {\Gamma\vdash A\to B,\Delta} \qquad\qquad \frac{\Gamma\vdash A,\Delta\qquad \Gamma,B\vdash\Delta} {A\to B,\Gamma\vdash \Delta} \\[0.7ex] \frac{A,\Gamma\vdash \Delta} {\Gamma\vdash \neg A,\Delta} \qquad\qquad \frac{\Gamma\vdash A,\Delta} {\neg A,\Gamma\vdash \Delta} \end{align*}$$
Каждое из правил соответствует анализу одной из формул нижней секвенции. Правила разделены на группы в зависимости от главной связки анализируемой формулы, и согласованы с таблицами истинности для этой связки (что легко проверить). Запятая в правилах используется как сокращение: $$\Gamma,A$$ обозначает $$\Gamma\hm\cup\{A\}$$ и т. д.
Как пользоваться этими правилами? Возьмем секвенцию, к которой мы ищем контрпример. Выберем в ней одну из формул слева или справа, посмотрим на главную связку и применим соответствующее правило (написав одну или две секвенции над исходной). Затем к каждой из них снова применим одно из правил и т. д. Постепенно будет расти "дерево поиска контрпримера", причем исходная секвенция будет иметь контрпример тогда и только тогда, когда одна из верхних секвенций (стоящих в "листьях") этого дерева имеет контрпример.
Когда этот процесс обрывается? Это происходит в том случае, если все формулы в оставшихся секвенциях представляют собой переменные, тогда ни одно из наших правил поиска контрпримера не применимо. Но к этому моменту все становится ясным: если в левой и правой части секвенции есть общая переменная, то к ней нет контрпримера (одна и та же переменная не может быть одновременно истинной и ложной). Если же левая и правая часть такой секвенции не пересекаются, то контрпример есть.
Вот как это делается с секвенцией $${\vdash(p\to q)}\hm\to q$$:$$\frac{\mathstrut\vdash p,q\;\qquad q\vdash q} {\frac{\displaystyle \mathstrut(p\to q)\vdash q} {\displaystyle \mathstrut\vdash (p\to q)\to q}}$$ Контрпример найден: $$p$$ и $$q$$ ложны (он является контрпримером к секвенции $$\vdash p,q$$ ).
Напротив, попытка поиска контрпримера к секвенции $${\vdash((p\to q)\to p)}\hm\to p$$
не дает результата:$$\frac{\frac{
\frac{\displaystyle \mathstrut p\vdash p,q}
{\displaystyle \mathstrut\vdash p,p\to q}\qquad
\displaystyle
\mathstrut p\vdash p}
{\displaystyle \mathstrut (p\to q)\to p\vdash p}}
{\mathstrut\vdash((p\to q)\to p)\to p}$$
Здесь обе секвенции $$p\hm\vdash p,q$$ и $$p\hm\vdash p$$ не
имеют контрпримеров. Следовательно, формула $$((p\to q)\to p)\to p$$
является
Построенный алгоритм можно одновременно рассматривать как доказательство полноты некоторого "исчисления секвенций".
Аксиомами исчисления секвенций будем называть секвенции, в левых и правых частях которых встречаются только переменные, причем некоторая переменная встречается в обеих частях.
Правилами вывода в исчислении секвенций являются правила нашей таблицы. Каждое из этих правил объявляет выводимой нижнюю секвенцию, если выводимы все верхние. (Процесс вывода естественно представлять в виде дерева, как в наших примерах, но можно развернуть и в последовательность секвенций.)
Теорема 23 (корректность и полнота исчисления секвенций). Секвенция выводима тогда и только тогда, когда она не имеет контрпримера.
Аксиомы не имеют контрпримера. Если все верхние секвенции какого-то правила вывода не имеют контрпримера, то и нижняя секвенция не имеет контрпримера. (Именно так мы подбирали правила: контрпример к нижней секвенции будет контрпримером к одной из верхних.) Следовательно, все выводимые секвенции не имеют контрпримера.
Обратно, пусть секвенция не имеет контрпримера. Тогда описанный процесс поиска контрпримера обрывается на аксиомах и тем самым дает ее вывод.
В частности, если формула $$A$$ является
Это требует довольно хлопотной проверки, впрочем. Сначала надо
проверить, что конъюнкция и дизъюнкция доказуемо ассоциативны, и
потому все равно, как расставлять скобки в формуле,
представляющей секвенцию. Затем полезно убедиться, что правила,
связанные с отрицанием (два последних правила таблицы) можно
применять в обе стороны, не меняя выводимости соответствующей
формулы. Другими словами, надо проверить, что формулы$$\Gamma\to(\Delta\lor A) \quad \text{и} \quad
(\Gamma\land\lnot A)\to\Delta,$$
а также формулы$$\Gamma\to(\Delta\lor \lnot A) \quad \text{и} \quad
(\Gamma\land A)\to\Delta$$
выводимы одновременно (здесь $$\Gamma$$ и $$\Delta$$ можно
считать формулами, а не множествами формул, расставив скобки надлежащим
образом). После этого мы можем переносить формулы из одной части
в другую (меняя их на противоположные), и потому можем считать
одно из множеств $$\Gamma$$ и $$\Delta$$ пустым, если это нам
удобно. Теперь ссылка на лемму о
30. Провести это рассуждение подробно.
Естественно возникает вопрос — чем уж так интересно исчисление
секвенций? Какая, собственно говоря, разница — иметь дело с
секвенциями или с формулами, раз всякую секвенцию можно
представить формулой? Принципиальное различие тут в следующем.
Правила вывода в исчислении секвенций таковы, что в их верхнюю
часть входят только
Заметим, что добавление к исчислению секвенций уже упоминавшегося правила сечения$$\frac{\Gamma\vdash \Delta,A \qquad \Gamma, A\vdash \Delta} {\Gamma \vdash \Delta}$$ нарушает свойство "подформульности", так как формула $$A$$ может быть никак не связана с нижней секвенцией. Отметим, что добавление правила сечения не нарушает корректности, как легко проверить, и не может нарушить полноты.
Задачи о поиске вывода и анализе его структуры, хотя и были одно
время модными в связи с "искусственным интеллектом",
представляют большой интерес, и про них есть целая наука, в
которой исчисления генценовского типа играют центральную роль.
Мы рассмотрели один из вариантов исчисления секвенций для
классического исчисления высказываний; бывают исчисления для
интуиционистских и модальных логик, для
Исключим из числа аксиом
Конечно, сразу же возникают естественные вопросы. Почему именно
эта аксиома вызывает сомнения? Вообще-то аксиом много, и можно
было бы исключить любую и смотреть, что получится без нее — но
ясно, что скорее всего получится что-то странное. Как понять,
какие формулы останутся теоремами без закона исключенного
третьего? Раньше у исчисления высказываний была "сверхзадача" —
вывести все
Интуиционистская логика возникла как попытка (сделанная Гейтингом) формализовать (пусть частично) методы рассуждений, практикуемые в "интуиционистской математике". Голландский математик Брауэр широко известен как автор классической (во всех смыслах) теоремы Брауэра о неподвижной точке (она утверждает, что любое непрерывное отображение многомерного шара $$D^n$$ в себя имеет неподвижную точку). Но одновременно он создал целую школу в области оснований математики — математический интуиционизм. Отчего, спрашивал Брауэр, в теории множеств возникли парадоксы? Можно считать, что это оттого, что мы стали рассуждать о каких-то уж очень абстрактных объектах, которые существуют лишь в нашей (порой противоречивой) фантазии, так что следует проявлять осторожность и не подходить к опасной черте. Но Брауэр пошел дальше, говоря, что противоречия лишь симптом болезни, а надо устранить ее причину. Причину он видел в том, что математические рассуждения и понятия утратили интуитивный смысл, и нужно вернуться к основам и пересмотреть смысл самих логических связок.
Что мы имеем в виду (или должны иметь в виду), говоря о том, что мы установили, что " $$A$$ или $$B$$ "? Это значит, по Брауэру, что либо мы установили $$A$$, либо установили $$B$$. Когда мы устанавливаем, что " $$A$$ и $$B$$ ", это значит, что мы установили и $$A$$, и $$B$$. "Если $$A$$, то $$B$$ " означает, что мы располагаем каким-то общим рассуждением, которое позволит нам установить $$B$$, как только кто-то установит нам $$A$$. Отрицание $$A$$ означает, что мы располагаем рассуждением, которое приводит к противоречию предположение, что $$A$$ установлено. (Как с точки зрения интуиционизма, так и с классической точки зрения, $$\lnot A$$ во всех смыслах эквивалентно $$A\to\perp$$, где $$\perp$$ — заведомо ложное утверждение. Можно было бы вообще не использовать отрицания, а иметь константу $$\perp$$ — это не очень привычно, но технически удобно.)
Интуиционизм отвергает идею о том, что все высказывания делятся
на истинные и ложные (пусть неизвестным нам образом). С этой
точки зрения
Обычно, говоря об интуиционизме, приводят следующий пример
рассуждения, неприемлемого с точки зрения интуиционизма.
Докажем, что существуют
Вообще интуиция — дело тонкое: если долго рассуждать, скажем, о действительных числах, то начинает казаться, что они в каком-то смысле существуют независимо от наших рассуждений. Именно поэтому психологически оправдан вопрос о том, скажем, как обстоят дела с континуум-гипотезой "на самом деле": существует ли несчетное множество действительных чисел, не равномощное всем действительным числам, или не существует?
Мы не будем говорить о философских предпосылках интуиционизма
подробно. Вкратце упрощенная история вопроса такова. Брауэр
наметил планы переустройства математики на интуиционистских
принципах и отстаивал их настолько горячо, что однажды Гильберт
в раздражении заметил: отменить
В планы Брауэра не входила формализация интуиционистской логики
и математики, скорее наоборот. Тем не менее анализ принципов
интуиционизма пошел именно по этому пути, когда Гейтинг
стал изучать пропозициональную логику без закона исключенного
третьего. Различные спорные интуиционистские принципы стали
предметом изучения с точки зрения формальной логики; были
построены интуиционистские варианты формальной арифметики, теории
множеств,
Возвращаясь к интуиционистскому исчислению высказываний, приведем несколько выводимых формул.
31. Провести подробно доказательство выводимости в интуиционистском исчислении высказываний всех перечисленных формул.
С другой стороны, многие законы классической логики перестают
быть выводимыми без
Довольно ясно, что эти формулы не согласуются с интуиционистским подходом. Например, в предпоследней формуле говорится, что если мы опровергли предположение $$(p \land q)$$, то мы можем указать на одно из предположений $$p$$ и $$q$$ и предъявить его опровержение. Вряд ли такой переход можно считать обоснованным с интуиционистской точки зрения. Но, разумеется, формальный вопрос о выводимости требует формального ответа.
Начнем с
Теорема 24.Формула $$p\lor\lnot p$$ не выводима в интуиционистской логике.
В классической логике каждая пропозициональная переменная может
принимать два значения — истина ( И ) и ложь ( Л ). В зависимости
от значений переменных каждой формуле также приписывается
значение И или Л. Расширим множество
Мы докажем, что интуиционистски выводимые формулы всегда принимают значение И, а формула $$p\lor\lnot p$$ не такова, и потому не выводима.
Чтобы определить
Сложнее всего определение истинности для импликации. Мы полагаем, что$$(\text{И}\to x)=x \quad\text{и}\quad (\text{Л}\to x)=\text{И}$$ для любого истинностного значения $$x$$, а также что$$(\text{Н}\to\text{Л})=\text{Л}, \quad (\text{Н}\to\text{Н})=\text{И} \text{ и }(\text{Н}\to\text{И})=\text{И}.$$
Назовем формулу $$3$$ -
Следовательно, всякая интуиционистски выводимая формула является $$3$$ -
32. Покажите, что всякая $$3$$ -
Использованный нами прием годится не всегда. Например,
интуиционистски невыводимая формула $$\lnot p \lor\lnot\lnot p$$
является $$3$$ -
33. Какие из перечисленных нами интуиционистски невыводимых формул являются $$3$$ -тавтологиями?
Более общий способ установления недоказуемости (невыводимости) различных формул доставляют шкалы Крипке (или модели Крипке, как еще говорят).
Чтобы задать шкалу Крипке, нужно:
При этом требуется, чтобы было выполнено следующее: если $$u\le v$$ и $$u\Vdash x$$, то $$v\Vdash x$$ (область истинности любой переменной наследственна вверх).
Когда шкала задана, можно определить истинность любой формулы (в
данном мире) индукцией по построению формулы. Мы пишем $$w\Vdash
A$$, если в мире $$w$$
Формула, не являющаяся истинной (в данном мире), называется ложной (в нем).
Определение истинности для отрицания, как легко проверить, согласовано с пониманием $$\lnot A$$ как $$A\to{\perp}$$, где $$\perp$$ — тождественно ложная (во всех мирах) формула.
Именно определение импликации (и отрицания) использует порядок на множестве миров. Если формула содержит лишь конъюнкции и дизъюнкции, то ее истинность по существу определяется отдельно в каждом мире.
Индукцией по построению формулы $$A$$ легко проверить, что если она истинна в каком-то мире, то истинна и во всех больших мирах. В самом деле, пересечение и объединение двух наследственных вверх множеств также обладает этим свойством, так что для случая конъюнкции и дизъюнкции можно сослаться на предположение индукции. А для импликации даже и этого не нужно, достаточно посмотреть на определение.
Философский смысл шкал Крипке иногда объясняют так. Пусть $$W$$ есть множество возможных состояний цивилизации (миров); $$w\le u$$ означает, что мир $$u$$ может получиться из мира $$w$$ в результате развития цивилизации. Утверждение $$w\Vdash A$$ означает, что в мире $$w$$ установлено, что высказывание $$A$$ истинно. (При этом оно останется истинным и при дальнейшем развитии цивилизации.) Истинность $$\lnot A$$ в мире $$w$$ означает, что ни при каком развитии цивилизации из состояния $$w$$ высказывание $$A$$ не станет истинным.
Определение истинности отрицания в шкалах Крипке предвосхитил Пушкин, когда писал "нет правды на земле. Но правды нет и выше, $$\ldots$$ " (Моцарт и Сальери).
34.Во что превращается определение истинности в шкале Крипке, если в ней только один мир? если в ней никакие два мира не сравнимы?
Теорема 25 (корректность интуиционистского исчисления высказываний относительно шкал Крипке). Формула, выводимая в интуиционистском исчислении высказываний, истинна во всех мирах всех шкал Крипке.
Надо проверить, что все аксиомы истинны во всех мирах, а также что правило modus ponens сохраняет это свойство. Второе очевидно: если $$A\to B$$ истинна во всех мирах и $$A$$ истинна во всех мирах, то по определению истинности импликации $$B$$ будет истинна во всех мирах.
Осталось проверить истинность всех аксиом. Чтобы установить,
что импликация $$\varphi\to\psi$$ истинна во всех мирах,
надо проверить, что в тех мирах, где
Проверим вторую аксиому $$(A\hm\to(B\hm\to C))\hm\to((A\hm\to B)\hm\to (A\hm\to C))$$. Пусть $$u\Vdash A\to(B\to C)$$. Надо убедиться, что $$u\Vdash (A\to B)\to(A\to C)$$. Это означает, что если $$v\ge u$$ и $$v\Vdash A\to B$$, то $$v\Vdash A\to C$$. Последнее, в свою очередь, значит, что если $$w\ge v$$ и $$w\Vdash A$$, то $$w\Vdash C$$. Но в силу монотонности мы знаем, что $${w\Vdash A\to(B\to C)}$$ и $$w\Vdash A\hm\to B$$. Поэтому из $$w\Vdash A$$ следует $$w\Vdash B$$, $$w\Vdash (B\to C)$$, и, наконец, $$w\Vdash C$$, что и требовалось.
Остальные аксиомы проверяются еще проще.
Таким образом, чтобы доказать, что некоторая формула не выводима в интуиционистском исчислении высказываний, достаточно предъявить шкалу Крипке, в одном из миров которой она ложна.
35. Покажите, что в этом случае есть шкала, в которой среди миров есть наименьший и в нем формула ложна.
Для формулы $$p\lor \lnot p$$ такая шкала строится легко. Возьмем два мира, первый меньше второго. Пусть $$p$$ истинна только во втором мире. Тогда $$\lnot p$$ не будет истинна нигде, а $$p\lor \lnot p$$ будет истинна только во втором мире.
На самом деле это доказательство в сущности совпадает с
приведенным выше (с
Теперь мы можем установить, что все перечисленные выше формулы невыводимы в интуиционистском исчислении высказываний. Для формулы $$\lnot\lnot p \to p$$ годится та же самая шкала ( $$p$$ истинно только в большем мире). Она же годится для формулы $$(\lnot q\to\lnot p)\to (p\to q)$$, если $$p$$ истинно в обоих мирах, а $$q$$ — только в большем. Для трех оставшихся формул можно рассмотреть шкалы с тремя мирами: начальным миром $$u$$, из которого можно попасть в $$v\ge u$$ и в $$w\ge u$$ ; миры $$v$$ и $$w$$ не сравнимы. Если формула $$p$$ истинна только в мире $$v$$, то формула $$\lnot p$$ истинна только в мире $$w$$, a $$\lnot\lnot p$$ истинна только в мире $$v$$, так что в мире $$u$$ обе формулы $$\lnot p$$ и $$\lnot\lnot p$$ ложны и дизъюнкция $$\lnot p \lor \lnot\lnot p$$ ложна. Чтобы построить контрмодель для формулы $$\lnot(p\land q)\to \lnot p\lor \lnot q$$, будем считать, что $$p$$ истинна только в мире $$v$$, а $$q$$ истинна только в мире $$w$$. Та же шкала годится и для формулы $$((p\lor q)\to p)\lor((p\lor q)\to q)$$.
Оказывается, что этот прием универсален, как показывает следующая теорема.
Теорема 26 (полноты интуиционистского исчисления высказываний относительно шкал Крипке). Для любой невыводимой в интуиционистском исчислении формулы $$\varphi$$ можно подобрать шкалу Крипке, в которой $$\varphi$$ ложна в некотором мире.
Напомним схему доказательства полноты классического исчисления высказываний, приведенного в разделе "Второе доказательство теоремы о полноте". Пусть формула $$\varphi$$ невыводима. Мы хотим найти значения переменных, при которых формула $$\varphi$$ ложна, то есть формула $$\lnot\varphi$$ истинна. Само по себе требование истинности $$\lnot\varphi$$ не определяет значения переменных однозначно. Чтобы избавиться от произвола, мы расширяем непротиворечивое множество $$\{\lnot\varphi\}$$ до полного множества $$\Gamma$$ и объявляем истинными те переменные, которые входят в $$\Gamma$$.
Для интуиционистского случая в этой схеме требуются некоторые изменения. Раньше ложность формулы $$\varphi$$ была равносильна истинности формулы $$\lnot\varphi$$. В шкалах Крипке это уже не так, и мы будем отдельно говорить об истинных и ложных (не истинных) формулах.
Пусть $$A$$ и $$B$$ — конечные множества пропозициональных формул. Будем говорить, что пара $$(A,B)$$ совместна, если существует шкала Крипке и ее мир, в котором все формулы из $$A$$ истинны, а все формулы из $$B$$ ложны. Будем говорить, что пара $$(A,B)$$ противоречива, если в интуиционистском исчислении высказываний выводима формула$$(A_1 \land A_2 \land\ldots\land A_n) \to (B_1 \lor B_2 \lor\ldots\lor B_m),$$ где $$A_1,\dots,A_n$$ — формулы множества $$A$$, а $$B_1,\dots,B_m$$ — формулы множества $$B$$. (Без ограничения общности можно считать, что перечислены все формулы множеств $$A$$ и $$B$$, поскольку пропущенные формулы можно добавить, не нарушив выводимость.)
Пример: если одна и та же формула входит в обе части пары, то такая пара противоречива.
Легко проверить, что противоречивая пара не может быть совместна. В самом деле, если в некотором мире все формулы из $$A$$ истинны, а все формулы из $$B$$ ложны, то посылка импликации в этом мире истинна, а заключение ложно. Поэтому импликация ложна, что противоречит ее выводимости (теорема о корректности).
Мы докажем, что верно и обратное: всякая непротиворечивая пара
совместна. В частности, когда $$B$$ состоит из единственной
формулы, получается утверждение теоремы о полноте. (Мы
предполагаем, как это обычно делается, что конъюнкция пустого
множества формул есть
Итак, пусть имеется непротиворечивая пара $$(A,B)$$. Как доказать ее совместность? Как и в классическом случае, мы устраним произвол, расширив $$A$$ и $$B$$. Основным средством здесь является такая лемма.
Лемма 1. Пусть $$(A,B)$$ — непротиворечивая пара, а $$\tau$$ — произвольная формула. Тогда хотя бы одна из пар $$(A\cup\{\tau\},B)$$ и $$(A,B\cup\{\tau\})$$ непротиворечива.
Доказательство леммы 1. Пусть обе пары с добавленным $$\tau$$ противоречивы. Надо доказать, что противоречива исходная пара. Другими словами, надо показать, что если в интуиционистском исчислении высказываний выводимы формулы$$\begin{align*} (A \land \tau)\to B,\\ A \to(B \lor \tau), \end{align*}$$ то выводима и формула $$A\to B$$ (для простоты мы отождествляем множества $$A$$ и $$B$$ с конъюнкцией и дизъюнкцией их элементов и считаем $$A$$ и $$B$$ формулами).
В самом деле, по лемме о
Проведенное рассуждение, как говорят, устанавливает допустимость (в интуиционистской логике) правила сечения, позволяющего "иссечь" формулу $$\tau$$ из формул $$(A\land\tau)\to B$$ и $$A\to(B\lor\tau)$$ и получить формулу $$A\to B$$.
Возвращаясь к доказательству теоремы, рассмотрим произвольную непротиворечивую пару $$(A,B)$$. Рассматривая по очереди различные формулы $$\tau$$, мы будем добавлять их к левой или правой части. Чтобы этот процесс ("пополнение") был конечным, мы ограничимся формулами из некоторого множества.
Фиксируем некоторое конечное множество формул $$F$$, которое
содержит все формулы из $$A,B$$ и замкнуто относительно перехода к
Пару $$(X,Y)$$, у которой $$X,Y\hm\subset F$$, будем называть полной, если она непротиворечива и любая формула из $$F$$ входит либо в $$X$$, либо в $$Y$$ (то есть $$X\hm\cup Y\hm=F$$ ). Заметим, что из непротиворечивости следует, что $$X\hm\cap Y\hm=\varnothing$$, так что полная пара задает разбиение $$F$$ на две части. (Более точно полные пары следовало бы называть "полными относительно $$F$$ ", но у нас множество $$F$$ фиксировано.)
Лемма 2. Исходная пара $$(A,B)$$ может быть расширена до полной: существует полная пара $$(X,Y)$$, для которой $$A\hm\subset X$$, $$B\hm\subset Y$$.
Доказательство очевидно: применяем по очереди лемму 1 ко всем формулам из $$F$$.
Точно так же любую непротиворечивую пару, составленную из формул множества $$F$$, можно расширить до полной. (Это замечание нам впоследствии понадобится.)
Для завершения доказательства теоремы 26. нам осталось показать, что всякая полная пара $$(A,B)$$ совместна (существует шкала и мир, в котором формулы из $$A$$ истинны, а формулы из $$B$$ ложны). В отличие от классического случая построение будет использовать не только пару $$(A,B)$$, но и все полные пары.
Шкала Крипке строится так. Мирами будут полные пары $$(R,S)$$ (то
есть всевозможные непротиворечивые
Осталось определить порядок на множестве пар. Считаем, что $$(R_1,S_1)\hm\le(R_2,S_2)$$, если $$R_1\hm\subset R_2$$. (Такое определение не удивительно, если вспомнить, что истинность формул наследуется вверх.)
Лемма 3. В построенной шкале в мире $$(R,S)$$ истинны все формулы из $$R$$ и ложны все формулы из $$S$$.
Доказательство леммы 3 проводится индукцией по построению формул. Для переменных она верна по определению истинности. Пусть некоторая формула из $$F$$ не является переменной. Тогда она есть конъюнкция, дизъюнкция, импликация или отрицание и для ее частей утверждение леммы верно по предположению индукции. Рассмотрим все случаи по очереди, начав с конъюнкции и дизъюнкции (истинность которых не зависит от других миров).
( $$\land_R$$ ) Пусть формула $${\varphi\land\psi}$$ входит в $$R$$. Тогда формулы $$\varphi$$ и $$\psi$$ не могут входить в $$S$$, иначе пара $$(R,S)$$ была бы противоречивой (из $${\varphi\land\psi}$$ выводится $$\varphi$$ и $$\psi$$ ). Значит, $$\varphi$$ и $$\psi$$ входят в $$R$$ (полнота), поэтому они истинны (предположение индукции), и потому $${\varphi\land\psi}$$ истинна (определение истинности).
( $$\land_S$$ ) Пусть формула $${\varphi\land\psi}$$ входит в $$S$$. Могут ли обе формулы $$\varphi$$ и $$\psi$$ входить в $$R$$? Нет, так как в этом случае пара $$(R,S)$$ была бы противоречивой. Значит, хотя бы одна из формул входит в $$S$$, тогда по предположению индукции она ложна, и потому формула $${\varphi\land\psi}$$ ложна в мире $$(R,S)$$.
( $$\lor_R$$ ) Если формула $${\varphi\lor\psi}$$ входит в $$R$$, то формулы $$\varphi$$ и $$\psi$$ не могут одновременно входить в $$S$$, и потому хотя бы одна из них истинна, так что и вся формула $${\varphi\lor\psi}$$ истинна.
( $$\lor_S$$ ) Если формула $${\varphi\lor\psi}$$ входит в $$S$$, то формулы $$\varphi$$ и $$\psi$$ не могут входить в $$R$$, поэтому обе они ложны и формула $${\varphi\lor\psi}$$ ложна.
( $$\to_R$$ ) Пусть формула $${\varphi\to\psi}$$ входит в $$R$$. Проверим, что она истинна в $$(R,S)$$. Это значит, что в любом
мире $$(R',S')$$, который выше нашего (то есть $$R'\supset R$$ ) и в
котором
( $$\to_S$$ ) Это наиболее интересный случай, где нам снова
потребуется пополнение. Пусть формула $${\varphi\to\psi}$$ входит
в $$S$$. Мы должны доказать, что она ложна в мире $$(R,S)$$.
Согласно определению, это означает, что найдется мир $$(R',S')$$,
для которого $$R'\supset R$$ и в котором формула $$\varphi$$
истинна, а формула $$\psi$$ ложна (то есть $$\varphi\hm\in
R'$$ и $$\psi\in S'$$, согласно предположению индукции). Как найти такой
мир? Рассмотрим пару $$({R\cup\{\varphi\}},\{\psi\})$$. Эта пара
непротиворечива. В самом деле, если бы формула $${R\land\varphi}\hm\to\psi$$ была бы выводима, то и формула $$R\to(\varphi\to\psi)$$ была бы выводима (лемма о
Отрицание рассматривается аналогично импликации (как мы уже говорили, можно вместо отрицания ввести тождественную ложь $$\perp$$ и вообще его не рассматривать).
( $$\lnot_R$$ ) Пусть формула $$\lnot \varphi$$ входит в $$R$$. Надо доказать, что формула $$\varphi$$ ложна в любом мире $$(R',S')$$ выше мира $$(R,S)$$. Формула $$\varphi$$ не может входить в $$R'$$, так как в $$R'$$ входит формула $$\lnot\varphi$$ (напомним, что $$R\subset R'$$ ), а из $${\varphi\land\lnot\varphi}$$ выводится любая формула. Значит, $$\varphi$$ входит в $$S'$$ и по индуктивному предположению формула $$\varphi$$ ложна в $$(R',S')$$.
( $$\lnot_S)$$ Пусть формула $$\lnot\varphi$$ входит в $$S$$. В этом случае пара $$({R\cup \{\varphi\}},\varnothing)$$ непротиворечива (если из $$R$$ и $$\varphi$$ выводится противоречие, то из $$R$$ выводится $$\lnot\varphi$$ ). Расширив ее до полной, получаем высший мир $$(R',S')$$, в котором формула $$\varphi$$ истинна (по индуктивному предположению). Следовательно, формула $$\lnot\varphi$$ ложна в мире $$(R,S)$$.
Лемма 3 доказана. Она завершает доказательство
теоремы 26. Напомним еще раз его схему.
Пусть формула $$\varphi$$ не выводима в интуиционистском
исчислении высказываний. Тогда пара $$(\varnothing,\{\varphi\})$$
непротиворечива. Фиксируем множество $$F$$ всех
36. Покажите, что если формулы $$P$$ и $$Q$$ ложны в некоторых мирах некоторых шкал Крипке, то можно построить шкалу Крипке и мир в ней, для которого формула $${P\lor Q}$$ будет ложной. (Указание: соединим шкалы, в которых ложны формулы $$P$$ и $$Q$$, в одну, добавив новый мир, который меньше миров, где $$P$$ и $$Q$$ ложны.)
Из этой задачи и из теоремы о полноте вытекает такое следствие: если дизъюнкция двух формул выводима в интуиционистском исчислении высказываний, то хотя бы одна из формул тоже выводима. Это свойство выполнено для многих интуиционистских исчислений и соответствует начальной идее: доказать $$A\lor B$$ означает доказать одну из формул $$A$$ или $$B$$. Подобные свойства можно доказывать и синтаксически, используя генценовские варианты интуиционистских исчислений.
37. (а) Покажите, что формула $$\lnot\lnot(\varphi\lor\lnot\varphi)$$ выводима в интуиционистском исчислении высказываний. (б) Покажите, что если формулы $$\lnot\lnot\varphi$$ и $$\lnot\lnot(\varphi\hm\to\psi)$$ выводимы в интуиционистском исчислении высказываний, то и формула $$\lnot\lnot\psi$$ выводима в интуиционистском исчислении высказываний. (в) Докажите, что если формула $$\varphi$$ выводима в классическом исчислении высказываний, то формула $$\lnot\lnot\varphi$$ выводима в интуиционистском исчислении высказываний (теорема Гливенко) (г) Покажите, что для формул, содержащих лишь конъюнкцию и отрицание, разницы между классическим и интуиционистским исчислениями нет: из классической выводимости следует интуиционистская (теорема Геделя).
Покажите, что интуиционистское исчисление высказываний разрешимо: существует алгоритм, который по произвольной формуле определяет, выводима ли она в интуиционистском исчислении высказываний. (Указание: оцените мощность контрмодели Крипке; можно обойтись и без этого, заметив, что и множество выводимых формул, и множество формул, имеющих конечные контрмодели, перечислимы.)
В этом разделе мы построим другой вариант исчисления высказываний — так называемое исчисление секвенций. Такого рода исчисления изучаются в теории доказательств. Они оказываются более удобными для анализа синтаксической структуры выводов. Их называют исчислениями генценовского типа (по имени Генцена, который начал их изучать). Ранее приведенный вариант исчисления высказываний называют исчислением гильбертовского типа (по имени Гильберта, который использовал подобные исчисления в своей программе формального построения математики).
Для начала мы вообще не будем говорить ничего об аксиомах и
правилах вывода, а рассмотрим задачу поиска контрпримера. Пусть
дана некоторая формула $$A$$, про которую мы подозреваем, что она
не является
Введем необходимую терминологию и обозначения. Будем называть секвенцией выражение $$\Gamma\vdash\Delta$$, где $$\Gamma$$ и $$\Delta$$ — некоторые конечные множества формул. (Пока что знак $$\vdash$$ не имеет ничего общего с выводимостью, а только разделяет два множества формул.) С каждой секвенцией $$\Gamma\vdash\Delta$$ будем связывать задачу поиска таких значений переменных, при которых все формулы из $$\Gamma$$ истинны, а все формулы из $$\Delta$$ ложны. Такой набор значений мы по некоторым причинам будем называть контрпримером к секвенции $$\Gamma\vdash\Delta$$. Легко проверить, что контрпримеры к секвенции $$\Gamma\vdash\Delta$$ — это контрпримеры к формуле$$\land \Gamma\to\lor\Delta,$$ ( $$\land\Gamma$$ обозначает конъюнкцию формул из $$\Gamma$$, а $$\lor\Delta$$ — дизъюнкцию формул из $$\Delta$$ ), то есть те наборы значений, при которых эта формула ложна. При этом конъюнкцию пустого множества формул мы считаем тождественно истинной, а дизъюнкцию — тождественно ложной.
Наша исходная задача поиска контрпримера к формуле $$A$$ может быть теперь сформулирована как задача поиска контрпримера к секвенции $$\vdash A$$. (Мы позволяем себе писать так для краткости; полностью следовало бы написать $$\varnothing\vdash\{A\}$$.)
Задачу поиска контрпримера к секвенции можно решать с помощью следующих правил. В каждом из приведенных правил нижний заказ на контрпример выполним, если и только если выполним один из верхних заказов, т. е. нижняя секвенция имеет контрпример тогда и только тогда, когда хотя бы одна из верхних секвенций имеет контрпример.$$\begin{align*} \frac{\Gamma\vdash A,\Delta\qquad \Gamma\vdash B,\Delta} {\Gamma\vdash A\wedge B,\Delta} \qquad\qquad \frac{A,B,\Gamma\vdash\Delta} {A\wedge B,\Gamma\vdash\Delta} \\[0.7ex] \frac{\Gamma\vdash A, B,\Delta} {\Gamma\vdash A\vee B,\Delta} \qquad\qquad \frac{A,\Gamma\vdash \Delta\qquad B,\Gamma\vdash \Delta} {A\vee B,\Gamma\vdash \Delta} \\[0.7ex] \frac{\Gamma,A\vdash B,\Delta} {\Gamma\vdash A\to B,\Delta} \qquad\qquad \frac{\Gamma\vdash A,\Delta\qquad \Gamma,B\vdash\Delta} {A\to B,\Gamma\vdash \Delta} \\[0.7ex] \frac{A,\Gamma\vdash \Delta} {\Gamma\vdash \neg A,\Delta} \qquad\qquad \frac{\Gamma\vdash A,\Delta} {\neg A,\Gamma\vdash \Delta} \end{align*}$$
Каждое из правил соответствует анализу одной из формул нижней секвенции. Правила разделены на группы в зависимости от главной связки анализируемой формулы, и согласованы с таблицами истинности для этой связки (что легко проверить). Запятая в правилах используется как сокращение: $$\Gamma,A$$ обозначает $$\Gamma\hm\cup\{A\}$$ и т. д.
Как пользоваться этими правилами? Возьмем секвенцию, к которой мы ищем контрпример. Выберем в ней одну из формул слева или справа, посмотрим на главную связку и применим соответствующее правило (написав одну или две секвенции над исходной). Затем к каждой из них снова применим одно из правил и т. д. Постепенно будет расти "дерево поиска контрпримера", причем исходная секвенция будет иметь контрпример тогда и только тогда, когда одна из верхних секвенций (стоящих в "листьях") этого дерева имеет контрпример.
Когда этот процесс обрывается? Это происходит в том случае, если все формулы в оставшихся секвенциях представляют собой переменные, тогда ни одно из наших правил поиска контрпримера не применимо. Но к этому моменту все становится ясным: если в левой и правой части секвенции есть общая переменная, то к ней нет контрпримера (одна и та же переменная не может быть одновременно истинной и ложной). Если же левая и правая часть такой секвенции не пересекаются, то контрпример есть.
Вот как это делается с секвенцией $${\vdash(p\to q)}\hm\to q$$:$$\frac{\mathstrut\vdash p,q\;\qquad q\vdash q} {\frac{\displaystyle \mathstrut(p\to q)\vdash q} {\displaystyle \mathstrut\vdash (p\to q)\to q}}$$ Контрпример найден: $$p$$ и $$q$$ ложны (он является контрпримером к секвенции $$\vdash p,q$$ ).
Напротив, попытка поиска контрпримера к секвенции $${\vdash((p\to q)\to p)}\hm\to p$$
не дает результата:$$\frac{\frac{
\frac{\displaystyle \mathstrut p\vdash p,q}
{\displaystyle \mathstrut\vdash p,p\to q}\qquad
\displaystyle
\mathstrut p\vdash p}
{\displaystyle \mathstrut (p\to q)\to p\vdash p}}
{\mathstrut\vdash((p\to q)\to p)\to p}$$
Здесь обе секвенции $$p\hm\vdash p,q$$ и $$p\hm\vdash p$$ не
имеют контрпримеров. Следовательно, формула $$((p\to q)\to p)\to p$$
является
Построенный алгоритм можно одновременно рассматривать как доказательство полноты некоторого "исчисления секвенций".
Аксиомами исчисления секвенций будем называть секвенции, в левых и правых частях которых встречаются только переменные, причем некоторая переменная встречается в обеих частях.
Правилами вывода в исчислении секвенций являются правила нашей таблицы. Каждое из этих правил объявляет выводимой нижнюю секвенцию, если выводимы все верхние. (Процесс вывода естественно представлять в виде дерева, как в наших примерах, но можно развернуть и в последовательность секвенций.)
Теорема 23 (корректность и полнота исчисления секвенций). Секвенция выводима тогда и только тогда, когда она не имеет контрпримера.
Аксиомы не имеют контрпримера. Если все верхние секвенции какого-то правила вывода не имеют контрпримера, то и нижняя секвенция не имеет контрпримера. (Именно так мы подбирали правила: контрпример к нижней секвенции будет контрпримером к одной из верхних.) Следовательно, все выводимые секвенции не имеют контрпримера.
Обратно, пусть секвенция не имеет контрпримера. Тогда описанный процесс поиска контрпримера обрывается на аксиомах и тем самым дает ее вывод.
В частности, если формула $$A$$ является
Это требует довольно хлопотной проверки, впрочем. Сначала надо
проверить, что конъюнкция и дизъюнкция доказуемо ассоциативны, и
потому все равно, как расставлять скобки в формуле,
представляющей секвенцию. Затем полезно убедиться, что правила,
связанные с отрицанием (два последних правила таблицы) можно
применять в обе стороны, не меняя выводимости соответствующей
формулы. Другими словами, надо проверить, что формулы$$\Gamma\to(\Delta\lor A) \quad \text{и} \quad
(\Gamma\land\lnot A)\to\Delta,$$
а также формулы$$\Gamma\to(\Delta\lor \lnot A) \quad \text{и} \quad
(\Gamma\land A)\to\Delta$$
выводимы одновременно (здесь $$\Gamma$$ и $$\Delta$$ можно
считать формулами, а не множествами формул, расставив скобки надлежащим
образом). После этого мы можем переносить формулы из одной части
в другую (меняя их на противоположные), и потому можем считать
одно из множеств $$\Gamma$$ и $$\Delta$$ пустым, если это нам
удобно. Теперь ссылка на лемму о
30. Провести это рассуждение подробно.
Естественно возникает вопрос — чем уж так интересно исчисление
секвенций? Какая, собственно говоря, разница — иметь дело с
секвенциями или с формулами, раз всякую секвенцию можно
представить формулой? Принципиальное различие тут в следующем.
Правила вывода в исчислении секвенций таковы, что в их верхнюю
часть входят только
Заметим, что добавление к исчислению секвенций уже упоминавшегося правила сечения$$\frac{\Gamma\vdash \Delta,A \qquad \Gamma, A\vdash \Delta} {\Gamma \vdash \Delta}$$ нарушает свойство "подформульности", так как формула $$A$$ может быть никак не связана с нижней секвенцией. Отметим, что добавление правила сечения не нарушает корректности, как легко проверить, и не может нарушить полноты.
Задачи о поиске вывода и анализе его структуры, хотя и были одно
время модными в связи с "искусственным интеллектом",
представляют большой интерес, и про них есть целая наука, в
которой исчисления генценовского типа играют центральную роль.
Мы рассмотрели один из вариантов исчисления секвенций для
классического исчисления высказываний; бывают исчисления для
интуиционистских и модальных логик, для
Исключим из числа аксиом
Конечно, сразу же возникают естественные вопросы. Почему именно
эта аксиома вызывает сомнения? Вообще-то аксиом много, и можно
было бы исключить любую и смотреть, что получится без нее — но
ясно, что скорее всего получится что-то странное. Как понять,
какие формулы останутся теоремами без закона исключенного
третьего? Раньше у исчисления высказываний была "сверхзадача" —
вывести все
Интуиционистская логика возникла как попытка (сделанная Гейтингом) формализовать (пусть частично) методы рассуждений, практикуемые в "интуиционистской математике". Голландский математик Брауэр широко известен как автор классической (во всех смыслах) теоремы Брауэра о неподвижной точке (она утверждает, что любое непрерывное отображение многомерного шара $$D^n$$ в себя имеет неподвижную точку). Но одновременно он создал целую школу в области оснований математики — математический интуиционизм. Отчего, спрашивал Брауэр, в теории множеств возникли парадоксы? Можно считать, что это оттого, что мы стали рассуждать о каких-то уж очень абстрактных объектах, которые существуют лишь в нашей (порой противоречивой) фантазии, так что следует проявлять осторожность и не подходить к опасной черте. Но Брауэр пошел дальше, говоря, что противоречия лишь симптом болезни, а надо устранить ее причину. Причину он видел в том, что математические рассуждения и понятия утратили интуитивный смысл, и нужно вернуться к основам и пересмотреть смысл самих логических связок.
Что мы имеем в виду (или должны иметь в виду), говоря о том, что мы установили, что " $$A$$ или $$B$$ "? Это значит, по Брауэру, что либо мы установили $$A$$, либо установили $$B$$. Когда мы устанавливаем, что " $$A$$ и $$B$$ ", это значит, что мы установили и $$A$$, и $$B$$. "Если $$A$$, то $$B$$ " означает, что мы располагаем каким-то общим рассуждением, которое позволит нам установить $$B$$, как только кто-то установит нам $$A$$. Отрицание $$A$$ означает, что мы располагаем рассуждением, которое приводит к противоречию предположение, что $$A$$ установлено. (Как с точки зрения интуиционизма, так и с классической точки зрения, $$\lnot A$$ во всех смыслах эквивалентно $$A\to\perp$$, где $$\perp$$ — заведомо ложное утверждение. Можно было бы вообще не использовать отрицания, а иметь константу $$\perp$$ — это не очень привычно, но технически удобно.)
Интуиционизм отвергает идею о том, что все высказывания делятся
на истинные и ложные (пусть неизвестным нам образом). С этой
точки зрения
Обычно, говоря об интуиционизме, приводят следующий пример
рассуждения, неприемлемого с точки зрения интуиционизма.
Докажем, что существуют
Вообще интуиция — дело тонкое: если долго рассуждать, скажем, о действительных числах, то начинает казаться, что они в каком-то смысле существуют независимо от наших рассуждений. Именно поэтому психологически оправдан вопрос о том, скажем, как обстоят дела с континуум-гипотезой "на самом деле": существует ли несчетное множество действительных чисел, не равномощное всем действительным числам, или не существует?
Мы не будем говорить о философских предпосылках интуиционизма
подробно. Вкратце упрощенная история вопроса такова. Брауэр
наметил планы переустройства математики на интуиционистских
принципах и отстаивал их настолько горячо, что однажды Гильберт
в раздражении заметил: отменить
В планы Брауэра не входила формализация интуиционистской логики
и математики, скорее наоборот. Тем не менее анализ принципов
интуиционизма пошел именно по этому пути, когда Гейтинг
стал изучать пропозициональную логику без закона исключенного
третьего. Различные спорные интуиционистские принципы стали
предметом изучения с точки зрения формальной логики; были
построены интуиционистские варианты формальной арифметики, теории
множеств,
Возвращаясь к интуиционистскому исчислению высказываний, приведем несколько выводимых формул.
31. Провести подробно доказательство выводимости в интуиционистском исчислении высказываний всех перечисленных формул.
С другой стороны, многие законы классической логики перестают
быть выводимыми без
Довольно ясно, что эти формулы не согласуются с интуиционистским подходом. Например, в предпоследней формуле говорится, что если мы опровергли предположение $$(p \land q)$$, то мы можем указать на одно из предположений $$p$$ и $$q$$ и предъявить его опровержение. Вряд ли такой переход можно считать обоснованным с интуиционистской точки зрения. Но, разумеется, формальный вопрос о выводимости требует формального ответа.
Начнем с
Теорема 24.Формула $$p\lor\lnot p$$ не выводима в интуиционистской логике.
В классической логике каждая пропозициональная переменная может
принимать два значения — истина ( И ) и ложь ( Л ). В зависимости
от значений переменных каждой формуле также приписывается
значение И или Л. Расширим множество
Мы докажем, что интуиционистски выводимые формулы всегда принимают значение И, а формула $$p\lor\lnot p$$ не такова, и потому не выводима.
Чтобы определить
Сложнее всего определение истинности для импликации. Мы полагаем, что$$(\text{И}\to x)=x \quad\text{и}\quad (\text{Л}\to x)=\text{И}$$ для любого истинностного значения $$x$$, а также что$$(\text{Н}\to\text{Л})=\text{Л}, \quad (\text{Н}\to\text{Н})=\text{И} \text{ и }(\text{Н}\to\text{И})=\text{И}.$$
Назовем формулу $$3$$ -
Следовательно, всякая интуиционистски выводимая формула является $$3$$ -
32. Покажите, что всякая $$3$$ -
Использованный нами прием годится не всегда. Например,
интуиционистски невыводимая формула $$\lnot p \lor\lnot\lnot p$$
является $$3$$ -
33. Какие из перечисленных нами интуиционистски невыводимых формул являются $$3$$ -тавтологиями?
Более общий способ установления недоказуемости (невыводимости) различных формул доставляют шкалы Крипке (или модели Крипке, как еще говорят).
Чтобы задать шкалу Крипке, нужно:
При этом требуется, чтобы было выполнено следующее: если $$u\le v$$ и $$u\Vdash x$$, то $$v\Vdash x$$ (область истинности любой переменной наследственна вверх).
Когда шкала задана, можно определить истинность любой формулы (в
данном мире) индукцией по построению формулы. Мы пишем $$w\Vdash
A$$, если в мире $$w$$
Формула, не являющаяся истинной (в данном мире), называется ложной (в нем).
Определение истинности для отрицания, как легко проверить, согласовано с пониманием $$\lnot A$$ как $$A\to{\perp}$$, где $$\perp$$ — тождественно ложная (во всех мирах) формула.
Именно определение импликации (и отрицания) использует порядок на множестве миров. Если формула содержит лишь конъюнкции и дизъюнкции, то ее истинность по существу определяется отдельно в каждом мире.
Индукцией по построению формулы $$A$$ легко проверить, что если она истинна в каком-то мире, то истинна и во всех больших мирах. В самом деле, пересечение и объединение двух наследственных вверх множеств также обладает этим свойством, так что для случая конъюнкции и дизъюнкции можно сослаться на предположение индукции. А для импликации даже и этого не нужно, достаточно посмотреть на определение.
Философский смысл шкал Крипке иногда объясняют так. Пусть $$W$$ есть множество возможных состояний цивилизации (миров); $$w\le u$$ означает, что мир $$u$$ может получиться из мира $$w$$ в результате развития цивилизации. Утверждение $$w\Vdash A$$ означает, что в мире $$w$$ установлено, что высказывание $$A$$ истинно. (При этом оно останется истинным и при дальнейшем развитии цивилизации.) Истинность $$\lnot A$$ в мире $$w$$ означает, что ни при каком развитии цивилизации из состояния $$w$$ высказывание $$A$$ не станет истинным.
Определение истинности отрицания в шкалах Крипке предвосхитил Пушкин, когда писал "нет правды на земле. Но правды нет и выше, $$\ldots$$ " (Моцарт и Сальери).
34.Во что превращается определение истинности в шкале Крипке, если в ней только один мир? если в ней никакие два мира не сравнимы?
Теорема 25 (корректность интуиционистского исчисления высказываний относительно шкал Крипке). Формула, выводимая в интуиционистском исчислении высказываний, истинна во всех мирах всех шкал Крипке.
Надо проверить, что все аксиомы истинны во всех мирах, а также что правило modus ponens сохраняет это свойство. Второе очевидно: если $$A\to B$$ истинна во всех мирах и $$A$$ истинна во всех мирах, то по определению истинности импликации $$B$$ будет истинна во всех мирах.
Осталось проверить истинность всех аксиом. Чтобы установить,
что импликация $$\varphi\to\psi$$ истинна во всех мирах,
надо проверить, что в тех мирах, где
Проверим вторую аксиому $$(A\hm\to(B\hm\to C))\hm\to((A\hm\to B)\hm\to (A\hm\to C))$$. Пусть $$u\Vdash A\to(B\to C)$$. Надо убедиться, что $$u\Vdash (A\to B)\to(A\to C)$$. Это означает, что если $$v\ge u$$ и $$v\Vdash A\to B$$, то $$v\Vdash A\to C$$. Последнее, в свою очередь, значит, что если $$w\ge v$$ и $$w\Vdash A$$, то $$w\Vdash C$$. Но в силу монотонности мы знаем, что $${w\Vdash A\to(B\to C)}$$ и $$w\Vdash A\hm\to B$$. Поэтому из $$w\Vdash A$$ следует $$w\Vdash B$$, $$w\Vdash (B\to C)$$, и, наконец, $$w\Vdash C$$, что и требовалось.
Остальные аксиомы проверяются еще проще.
Таким образом, чтобы доказать, что некоторая формула не выводима в интуиционистском исчислении высказываний, достаточно предъявить шкалу Крипке, в одном из миров которой она ложна.
35. Покажите, что в этом случае есть шкала, в которой среди миров есть наименьший и в нем формула ложна.
Для формулы $$p\lor \lnot p$$ такая шкала строится легко. Возьмем два мира, первый меньше второго. Пусть $$p$$ истинна только во втором мире. Тогда $$\lnot p$$ не будет истинна нигде, а $$p\lor \lnot p$$ будет истинна только во втором мире.
На самом деле это доказательство в сущности совпадает с
приведенным выше (с
Теперь мы можем установить, что все перечисленные выше формулы невыводимы в интуиционистском исчислении высказываний. Для формулы $$\lnot\lnot p \to p$$ годится та же самая шкала ( $$p$$ истинно только в большем мире). Она же годится для формулы $$(\lnot q\to\lnot p)\to (p\to q)$$, если $$p$$ истинно в обоих мирах, а $$q$$ — только в большем. Для трех оставшихся формул можно рассмотреть шкалы с тремя мирами: начальным миром $$u$$, из которого можно попасть в $$v\ge u$$ и в $$w\ge u$$ ; миры $$v$$ и $$w$$ не сравнимы. Если формула $$p$$ истинна только в мире $$v$$, то формула $$\lnot p$$ истинна только в мире $$w$$, a $$\lnot\lnot p$$ истинна только в мире $$v$$, так что в мире $$u$$ обе формулы $$\lnot p$$ и $$\lnot\lnot p$$ ложны и дизъюнкция $$\lnot p \lor \lnot\lnot p$$ ложна. Чтобы построить контрмодель для формулы $$\lnot(p\land q)\to \lnot p\lor \lnot q$$, будем считать, что $$p$$ истинна только в мире $$v$$, а $$q$$ истинна только в мире $$w$$. Та же шкала годится и для формулы $$((p\lor q)\to p)\lor((p\lor q)\to q)$$.
Оказывается, что этот прием универсален, как показывает следующая теорема.
Теорема 26 (полноты интуиционистского исчисления высказываний относительно шкал Крипке). Для любой невыводимой в интуиционистском исчислении формулы $$\varphi$$ можно подобрать шкалу Крипке, в которой $$\varphi$$ ложна в некотором мире.
Напомним схему доказательства полноты классического исчисления высказываний, приведенного в разделе "Второе доказательство теоремы о полноте". Пусть формула $$\varphi$$ невыводима. Мы хотим найти значения переменных, при которых формула $$\varphi$$ ложна, то есть формула $$\lnot\varphi$$ истинна. Само по себе требование истинности $$\lnot\varphi$$ не определяет значения переменных однозначно. Чтобы избавиться от произвола, мы расширяем непротиворечивое множество $$\{\lnot\varphi\}$$ до полного множества $$\Gamma$$ и объявляем истинными те переменные, которые входят в $$\Gamma$$.
Для интуиционистского случая в этой схеме требуются некоторые изменения. Раньше ложность формулы $$\varphi$$ была равносильна истинности формулы $$\lnot\varphi$$. В шкалах Крипке это уже не так, и мы будем отдельно говорить об истинных и ложных (не истинных) формулах.
Пусть $$A$$ и $$B$$ — конечные множества пропозициональных формул. Будем говорить, что пара $$(A,B)$$ совместна, если существует шкала Крипке и ее мир, в котором все формулы из $$A$$ истинны, а все формулы из $$B$$ ложны. Будем говорить, что пара $$(A,B)$$ противоречива, если в интуиционистском исчислении высказываний выводима формула$$(A_1 \land A_2 \land\ldots\land A_n) \to (B_1 \lor B_2 \lor\ldots\lor B_m),$$ где $$A_1,\dots,A_n$$ — формулы множества $$A$$, а $$B_1,\dots,B_m$$ — формулы множества $$B$$. (Без ограничения общности можно считать, что перечислены все формулы множеств $$A$$ и $$B$$, поскольку пропущенные формулы можно добавить, не нарушив выводимость.)
Пример: если одна и та же формула входит в обе части пары, то такая пара противоречива.
Легко проверить, что противоречивая пара не может быть совместна. В самом деле, если в некотором мире все формулы из $$A$$ истинны, а все формулы из $$B$$ ложны, то посылка импликации в этом мире истинна, а заключение ложно. Поэтому импликация ложна, что противоречит ее выводимости (теорема о корректности).
Мы докажем, что верно и обратное: всякая непротиворечивая пара
совместна. В частности, когда $$B$$ состоит из единственной
формулы, получается утверждение теоремы о полноте. (Мы
предполагаем, как это обычно делается, что конъюнкция пустого
множества формул есть
Итак, пусть имеется непротиворечивая пара $$(A,B)$$. Как доказать ее совместность? Как и в классическом случае, мы устраним произвол, расширив $$A$$ и $$B$$. Основным средством здесь является такая лемма.
Лемма 1. Пусть $$(A,B)$$ — непротиворечивая пара, а $$\tau$$ — произвольная формула. Тогда хотя бы одна из пар $$(A\cup\{\tau\},B)$$ и $$(A,B\cup\{\tau\})$$ непротиворечива.
Доказательство леммы 1. Пусть обе пары с добавленным $$\tau$$ противоречивы. Надо доказать, что противоречива исходная пара. Другими словами, надо показать, что если в интуиционистском исчислении высказываний выводимы формулы$$\begin{align*} (A \land \tau)\to B,\\ A \to(B \lor \tau), \end{align*}$$ то выводима и формула $$A\to B$$ (для простоты мы отождествляем множества $$A$$ и $$B$$ с конъюнкцией и дизъюнкцией их элементов и считаем $$A$$ и $$B$$ формулами).
В самом деле, по лемме о
Проведенное рассуждение, как говорят, устанавливает допустимость (в интуиционистской логике) правила сечения, позволяющего "иссечь" формулу $$\tau$$ из формул $$(A\land\tau)\to B$$ и $$A\to(B\lor\tau)$$ и получить формулу $$A\to B$$.
Возвращаясь к доказательству теоремы, рассмотрим произвольную непротиворечивую пару $$(A,B)$$. Рассматривая по очереди различные формулы $$\tau$$, мы будем добавлять их к левой или правой части. Чтобы этот процесс ("пополнение") был конечным, мы ограничимся формулами из некоторого множества.
Фиксируем некоторое конечное множество формул $$F$$, которое
содержит все формулы из $$A,B$$ и замкнуто относительно перехода к
Пару $$(X,Y)$$, у которой $$X,Y\hm\subset F$$, будем называть полной, если она непротиворечива и любая формула из $$F$$ входит либо в $$X$$, либо в $$Y$$ (то есть $$X\hm\cup Y\hm=F$$ ). Заметим, что из непротиворечивости следует, что $$X\hm\cap Y\hm=\varnothing$$, так что полная пара задает разбиение $$F$$ на две части. (Более точно полные пары следовало бы называть "полными относительно $$F$$ ", но у нас множество $$F$$ фиксировано.)
Лемма 2. Исходная пара $$(A,B)$$ может быть расширена до полной: существует полная пара $$(X,Y)$$, для которой $$A\hm\subset X$$, $$B\hm\subset Y$$.
Доказательство очевидно: применяем по очереди лемму 1 ко всем формулам из $$F$$.
Точно так же любую непротиворечивую пару, составленную из формул множества $$F$$, можно расширить до полной. (Это замечание нам впоследствии понадобится.)
Для завершения доказательства теоремы 26. нам осталось показать, что всякая полная пара $$(A,B)$$ совместна (существует шкала и мир, в котором формулы из $$A$$ истинны, а формулы из $$B$$ ложны). В отличие от классического случая построение будет использовать не только пару $$(A,B)$$, но и все полные пары.
Шкала Крипке строится так. Мирами будут полные пары $$(R,S)$$ (то
есть всевозможные непротиворечивые
Осталось определить порядок на множестве пар. Считаем, что $$(R_1,S_1)\hm\le(R_2,S_2)$$, если $$R_1\hm\subset R_2$$. (Такое определение не удивительно, если вспомнить, что истинность формул наследуется вверх.)
Лемма 3. В построенной шкале в мире $$(R,S)$$ истинны все формулы из $$R$$ и ложны все формулы из $$S$$.
Доказательство леммы 3 проводится индукцией по построению формул. Для переменных она верна по определению истинности. Пусть некоторая формула из $$F$$ не является переменной. Тогда она есть конъюнкция, дизъюнкция, импликация или отрицание и для ее частей утверждение леммы верно по предположению индукции. Рассмотрим все случаи по очереди, начав с конъюнкции и дизъюнкции (истинность которых не зависит от других миров).
( $$\land_R$$ ) Пусть формула $${\varphi\land\psi}$$ входит в $$R$$. Тогда формулы $$\varphi$$ и $$\psi$$ не могут входить в $$S$$, иначе пара $$(R,S)$$ была бы противоречивой (из $${\varphi\land\psi}$$ выводится $$\varphi$$ и $$\psi$$ ). Значит, $$\varphi$$ и $$\psi$$ входят в $$R$$ (полнота), поэтому они истинны (предположение индукции), и потому $${\varphi\land\psi}$$ истинна (определение истинности).
( $$\land_S$$ ) Пусть формула $${\varphi\land\psi}$$ входит в $$S$$. Могут ли обе формулы $$\varphi$$ и $$\psi$$ входить в $$R$$? Нет, так как в этом случае пара $$(R,S)$$ была бы противоречивой. Значит, хотя бы одна из формул входит в $$S$$, тогда по предположению индукции она ложна, и потому формула $${\varphi\land\psi}$$ ложна в мире $$(R,S)$$.
( $$\lor_R$$ ) Если формула $${\varphi\lor\psi}$$ входит в $$R$$, то формулы $$\varphi$$ и $$\psi$$ не могут одновременно входить в $$S$$, и потому хотя бы одна из них истинна, так что и вся формула $${\varphi\lor\psi}$$ истинна.
( $$\lor_S$$ ) Если формула $${\varphi\lor\psi}$$ входит в $$S$$, то формулы $$\varphi$$ и $$\psi$$ не могут входить в $$R$$, поэтому обе они ложны и формула $${\varphi\lor\psi}$$ ложна.
( $$\to_R$$ ) Пусть формула $${\varphi\to\psi}$$ входит в $$R$$. Проверим, что она истинна в $$(R,S)$$. Это значит, что в любом
мире $$(R',S')$$, который выше нашего (то есть $$R'\supset R$$ ) и в
котором
( $$\to_S$$ ) Это наиболее интересный случай, где нам снова
потребуется пополнение. Пусть формула $${\varphi\to\psi}$$ входит
в $$S$$. Мы должны доказать, что она ложна в мире $$(R,S)$$.
Согласно определению, это означает, что найдется мир $$(R',S')$$,
для которого $$R'\supset R$$ и в котором формула $$\varphi$$
истинна, а формула $$\psi$$ ложна (то есть $$\varphi\hm\in
R'$$ и $$\psi\in S'$$, согласно предположению индукции). Как найти такой
мир? Рассмотрим пару $$({R\cup\{\varphi\}},\{\psi\})$$. Эта пара
непротиворечива. В самом деле, если бы формула $${R\land\varphi}\hm\to\psi$$ была бы выводима, то и формула $$R\to(\varphi\to\psi)$$ была бы выводима (лемма о
Отрицание рассматривается аналогично импликации (как мы уже говорили, можно вместо отрицания ввести тождественную ложь $$\perp$$ и вообще его не рассматривать).
( $$\lnot_R$$ ) Пусть формула $$\lnot \varphi$$ входит в $$R$$. Надо доказать, что формула $$\varphi$$ ложна в любом мире $$(R',S')$$ выше мира $$(R,S)$$. Формула $$\varphi$$ не может входить в $$R'$$, так как в $$R'$$ входит формула $$\lnot\varphi$$ (напомним, что $$R\subset R'$$ ), а из $${\varphi\land\lnot\varphi}$$ выводится любая формула. Значит, $$\varphi$$ входит в $$S'$$ и по индуктивному предположению формула $$\varphi$$ ложна в $$(R',S')$$.
( $$\lnot_S)$$ Пусть формула $$\lnot\varphi$$ входит в $$S$$. В этом случае пара $$({R\cup \{\varphi\}},\varnothing)$$ непротиворечива (если из $$R$$ и $$\varphi$$ выводится противоречие, то из $$R$$ выводится $$\lnot\varphi$$ ). Расширив ее до полной, получаем высший мир $$(R',S')$$, в котором формула $$\varphi$$ истинна (по индуктивному предположению). Следовательно, формула $$\lnot\varphi$$ ложна в мире $$(R,S)$$.
Лемма 3 доказана. Она завершает доказательство
теоремы 26. Напомним еще раз его схему.
Пусть формула $$\varphi$$ не выводима в интуиционистском
исчислении высказываний. Тогда пара $$(\varnothing,\{\varphi\})$$
непротиворечива. Фиксируем множество $$F$$ всех
36. Покажите, что если формулы $$P$$ и $$Q$$ ложны в некоторых мирах некоторых шкал Крипке, то можно построить шкалу Крипке и мир в ней, для которого формула $${P\lor Q}$$ будет ложной. (Указание: соединим шкалы, в которых ложны формулы $$P$$ и $$Q$$, в одну, добавив новый мир, который меньше миров, где $$P$$ и $$Q$$ ложны.)
Из этой задачи и из теоремы о полноте вытекает такое следствие: если дизъюнкция двух формул выводима в интуиционистском исчислении высказываний, то хотя бы одна из формул тоже выводима. Это свойство выполнено для многих интуиционистских исчислений и соответствует начальной идее: доказать $$A\lor B$$ означает доказать одну из формул $$A$$ или $$B$$. Подобные свойства можно доказывать и синтаксически, используя генценовские варианты интуиционистских исчислений.
37. (а) Покажите, что формула $$\lnot\lnot(\varphi\lor\lnot\varphi)$$ выводима в интуиционистском исчислении высказываний. (б) Покажите, что если формулы $$\lnot\lnot\varphi$$ и $$\lnot\lnot(\varphi\hm\to\psi)$$ выводимы в интуиционистском исчислении высказываний, то и формула $$\lnot\lnot\psi$$ выводима в интуиционистском исчислении высказываний. (в) Докажите, что если формула $$\varphi$$ выводима в классическом исчислении высказываний, то формула $$\lnot\lnot\varphi$$ выводима в интуиционистском исчислении высказываний (теорема Гливенко) (г) Покажите, что для формул, содержащих лишь конъюнкцию и отрицание, разницы между классическим и интуиционистским исчислениями нет: из классической выводимости следует интуиционистская (теорема Геделя).
Покажите, что интуиционистское исчисление высказываний разрешимо: существует алгоритм, который по произвольной формуле определяет, выводима ли она в интуиционистском исчислении высказываний. (Указание: оцените мощность контрмодели Крипке; можно обойтись и без этого, заметив, что и множество выводимых формул, и множество формул, имеющих конечные контрмодели, перечислимы.)
Для получения официальных документов о завершении программы дополнительного профессионального образования (удостоверения о повышении квалификации, дипломов о профессиональной переподготовке и MBA) необходимо предоставить:
Внимание! Вы можете не заказывать доставку бумажной версии официального документы, а скачать его в электронном виде и распечатать самостоятельно. Информация о выданном документе в течение 1 месяца загружается в Федеральную информационную систему «Федеральный реестр сведений о документах об образовании и (или) о квалификации, документах об обучении» - ФИС ФРДО.
Доступ на новый сайт осуществляется с использованием адреса электронной почты, который был указан вами при регистрации на "старом". Мы постарались перенести все ваши данные с прежнего ресурса, однако не исключена вероятность потери части информации.
При возникновении проблемы со входом, воспользуйтесь функцией сброса пароля
Если вы обнаружите несоответствия, пожалуйста, сообщите нам.