Непейвода Н.Н. Прикладная логика

Подождите немного. Документ загружается.

16.5. МОДЕЛИ КРИПКЕ

441

Еще Брауэр заметил, что содержательно интуиционистская логика

предполагает накопление знаний, а не их видоизменение, и это замеча-

ние было положено в основу моделей возможных миров, обычно назы-

ваемых моделями Крипке

Определение 16.5.1.

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

для сигнатуры

— алгебраи-

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

, называемой

сиг-

натурой отношений на мирах

, элементами универса которой

(часто

обозначаемого

или просто

) служат алгебраические системы сиг-

натуры

. Элементы универса называются

(возможными) мирами

. Уни-

верс мира

p ∈ W

обозначается

Для случая интуиционистской логики рассматривается конкретный

вид моделей Крипке — интуиционистские модели Крипке. Сигнатура

отношений $ состоит из одного двуместного отношения 4. Оно явля-

ется отношением частичного порядка. Миры согласованы с данным от-

ношением следующим образом:

p 4 q ⇒ U

⊆ U

p 4 q & U

|= P (a

, . . . , a

) ⇒ U

|= P (a

, . . . , a

Таким образом, при подъеме по мирам универсы могу лишь расширять-

ся, и истинность элементарных формул не может перети в ложность.

Вспоминая определение из гл. 1, получаем, что при

p 4 q q является

надструктурой p.

Истинность в модели Крипке интуиционистской логики определя-

ется следующим образом.

Определение 16.5.2.

Индуктивно определяем отношение

p |= A

, где

— мир,

— формула.

p |= P (a

, . . . , a

)

означает истинность

P (a

, . . . , a

)

в классиче-

ской алгебраической системе

История создания данного понятия, как всегда, более сложная. Этот класс моде-

лей неявно содержался еще в алгебраических моделях (см. замечание ниже). Явно он

был использован П. Дж. Коэном для доказательства независимости аксиомы выбора и

континуум-гипотезы от стандартной теории множеств. С. Крипке первым показал при-

менимость данной конструкции к широкому классу логик и ее гибкость.

Поскольку истинность элементарных формул в алгебраической системе задается не-

посредственно интерпретацией предикатов, можно было в данном случае обойтись без

представления мира как алгебраической системы, задав его просто как множество зна-

442

ГЛАВА 16. ИНТУИЦИОНИСТСКАЯ ЛОГИКА

p |= A & B

означает, что

p |= A

p |= B

p |= A ∨ B

означает, что

p |= A

или

p |= B

p |= A ⇒ B

означает, что для всех миров

, таких, что

p 4 q

, если

q |= A

, то

q |= B

p |=

означает, что для всех миров

, таких, что

p 4 q

, неверно,

что

q |= A

p |= ∃x A(x)

означает, что найдется такое

a ∈ U

, что

p |= A(a)

p |= ∀x A(x)

означает, что для всех миров

, таких, что

p 4 q

, и

для всех

a ∈ U

q |= A(a)

Пример 16.5.1.

Рассмотрим следующую модель Крипке.

∙

∙ A ∙

(16.16)

В ней не истинно

A ∨

, поскольку в начальной точке у нас не из-

вестно ни то, ни другое (нет

, но нельзя утверждать и

, поскольку

выше

может появиться).

Пример 16.5.2.

Покажем, что интуиционистская логика не задается ни-

какой конечной системой истинностных значений. В самом деле, если

бы это было так, то имелось бы не более

логических значений фор-

мул, и, значит, в любой интерпретации в любой совокупности из

n + 1

формулы две обязательно были бы эквивалентны

. Значит, была бы то-

ждественно истинна формула

⇔ A

) ∨ ∙∙∙ ∨ (A

⇔ A

n+1

чений истинности элементарных формул. Такое представление намного удобнее для

пропозициональных формул, поэтому мы широко пользуемся им в примерах. Но об-

щее определение не сложнее, зато намного гибче.

Здесь мы принимаем естественную гипотезу, что эквивалентность означает совпа-

дение истинностных значений.

16.5. МОДЕЛИ КРИПКЕ

443

где через дизъюнкцию соединены все возможные попарные эквивалент-

ности разных формул. Но следующая модель Крипке опровергает дан-

ную дизъюнкцию, поскольку ни одна из эквивалентностей не истинна в

нижней точке:

∙

n+1

∙

∙∙∙

(16.17)

И, наконец, рассмотрим пример модели Крипке для логики преди-

катов.

Пример 16.5.3.

∙

}

∙

{0, 1} A

(0)

∙

{0, 1, 2} A(0), A

(1)

∙

∙∙∙

(16.18)

В данной модели в любом из миров есть такое

, что не истинно

A(n) ∨

A(n)

. Значит ни в каком из миров не истинно

∀x(A(x) ∨

A(x))

. А

тогда,по определению истинности отрицания,в любой ее точке истинно

∀x(A(x) ∨

A(x)).

(16.19)

Итак, с интуиционистской логикой могут быть совместимы и фор-

мулы, противоречащие классической.

Упражнения к § 16.5

16.5.1. Постройте модель, в которой

∀x A(x)

, но не выполнено, что

∃x A(x).

16.5.2. Постройте модель, где опровергается

(A ⇒ B) ∨ (B ⇒ A).

Может ли такая модель не иметь ветвлений?

444

ГЛАВА 16. ИНТУИЦИОНИСТСКАЯ ЛОГИКА

§ 16.6. СЕМАНТИЧЕСКИЕ ТАБЛИЦЫ

ДЛЯ ИНТУИЦИОНИСТСКОЙ ЛОГИКИ

Как уже говорилось, конструкция семантических таблиц переносится

на неклассические логики. Здесь мы рассмотрим ее для интуиционист-

ской логики.

Правила разбиения остаются такими же,как и в классических табли-

цах, но добавляются новые спецификации и уточняется в соответствии

с ними понятие противоречия.

Определение 16.6.1. Интуиционистская спецификация

— фигура

αΞ

где

— спецификация истинностного значения

или

, а

—

ин-

туиционистский префикс

, описывающий множество миров, в которых

должно иметь место данное значение формулы.

Интуиционистский префикс

— кортеж, членами которого являются

натуральные числа и символы

Если префикс не содержит

, то он описывает единственный мир,

именем которого служит данный кортеж.

Если префикс содержит

,то он описывает все кортежи натуральных

чисел, образующиеся замещением символов

произвольными кортежа-

ми натуральных чисел, в том числе и пустым кортежем, так что кортеж,

образующийся выбрасыванием всех

из некоторого префикса, описы-

вается им.

(Символы

играют здесь ту же роль, что и в шаблонах для задания

строк либо имен файлов в программировании, поэтому мы их исполь-

зовали, несмотря на некоторое неудобство: они лишь жирностью отли-

чаются от операции соединения кортежей.)

Два префикса

совместимы

, если их множества миров пересекаются.

Исходная формула помечается как [ ] =| A.

Перепишем все правила классических семантических таблиц, ука-

16.6. ИНТУИЦИОНИСТСКИЕ ТАБЛИЦЫ

445

зывая, как видоизменяются префиксы.

α |= A&B

α |= A α |= B

α =| A&B

α =| A | α =| B

α |= A ∨

α |= A | α |= B

α =| A ∨ B

α =| A α =| B

α |= A ⇒

α =| A | α |= B

α =| A ⇒ B

α ∗ [n] ∗[?] |= A α ∗ [n] =| B

α |=

¬A

α =| A

α =| ¬A

α ∗ [n] ∗[?] |= A

α |= ∀x

α |= A(c

)

α =| ∀x A

α ∗ [n] =| A(c

n+1

)

α |= ∃x

α |= A(c

n+1

)

α =| ∃x A

α =| A(c

)

(16.20)

Индексы видоизменяются лишь в правилах

=| ⇒, =|

, =| ∀.Появивши-

еся в них формулы будут отвергаться либо утверждаться не в мире α, в

котором отвергалась исходная формула, а в новом мире вида α ∗[n], не-

посредственно следующем за ним. n в каждом из таких правил выбира-

ется новым. Противоречием считается лишь такая пара формул α |= A,

β =| A, в которой α и β совместимы.

Заметим, что формула, которая стала истинной, не может в дальней-

шем оказаться ложной, поскольку все правила, вводящие |= A, помеща-

ют звездочку в конец кортежа.

Пример 16.6.1.

Рассмотрим семантическую таблицу для закона исклю-

ченного третьего.

[ ] =| A ∨

[ ] =| A [ ] =|

[1, ?] |= A

(16.21)

Противоречия нет, потому что

отвергается на более раннем уровне,

чем утверждается. Из данной таблицы получается следующая модель

Крипке:

∙

[ ] =| A

[1] |= A

∙

(16.22)

Слева модель Крипке записана со всей информацией, которую можно

извлечь из семантической таблицы, а справа — так, как это принято де-

446

ГЛАВА 16. ИНТУИЦИОНИСТСКАЯ ЛОГИКА

лать, оставив лишь минимальную информацию, полностью ее опреде-

ляющую

Заметим, что у нас получилась несколько другая модель, чем (16.21),

чуть проще, но чуть менее наглядная. Действительно,

нет сейчас,

правда, тоже нет, но никогда и не будет. Так что на самом деле в дан-

ной модели истинно

¬¬

, но опровергается

, и она более сильна, чем

нужно для опровержения

A ∨

Пример 16.6.2.

Рассмотрим теперь следующую семантическую табли-

цу.

[ ] =|

¬¬

A ⇒ A

[1, ?] |=

¬¬

A [1] =| A

[1, 2] =|

[1, 2] |= A

(16.23)

Получившаяся модель отличается от (16.22) добавлением совершенно

избыточного промежуточного мира:

∙

(16.24)

Конечно же, полностью устранить избыточность построений, поставля-

емых семантическими таблицами,очень трудно, но данный конкретный

случай диагностируется просто:

Если на данном уровне отвергаемая формула, требующая

подъема на новый уровень, единственна, то новый уровень

можно не вводить.

Строгое обоснование данного сокращающего правила следует ниже.

Заметим, что в моделях Крипке интуиционистской логики (да зачастую и других

логик) не принято выписывать отвергаемые в данной точке утверждения, поскольку

формально достаточно принять положение о том, что все не истинное отвергается. Но

семантическая таблица ставит отвержение лишь там, где истинность данной формулы

недопустима для опровержения цели. Поэтому на самом деле мы теряем часть инфор-

мации, особенно ценную для преобразования моделей.

16.6. ИНТУИЦИОНИСТСКИЕ ТАБЛИЦЫ

447

Рассмотрим теперь семантическую таблицу для достаточно слож-

ной формулы (формулы Крипке

[ ] =| ((((A ⇒ B) ⇒ A) ⇒ A) ⇒ B) ⇒ B

[?] |= (((A ⇒ B) ⇒ A) ⇒ A) ⇒ B

[ ] =| B

[?] =| ((A ⇒ B) ⇒ A) ⇒ A [?] |= B

[?, 1, ?] |= (A ⇒ B) ⇒

[?, 1] =| A

[?, 1, ?] =| A ⇒ B [?, 1] |= A

[?, 1, ?, 2] =|

[?, 1, ?, 2, ?] |= A

(16.25)

И, наконец, построим таблицу для формулы логики предикатов.

[ ] =|

¬¬

∀x(A(x) ∨

A(x))

[?] |=

∀x(A(x) ∨

A(x))

[?] =| ∀x(A(x) ∨

A(x))

[?, 1] =| A(c

) ∨

A(c

)

[?, 1] =| A(c

)

[?, 1] =|

A(c

)

[?, 1, 2, ?] |= A(c

)

[?, 1, 2] =| A(c

) ∨

A(c

)

∙∙∙

(16.26)

Таким образом, в интуиционистской логике правило

=| ∀ тоже может

оказаться многократно применяемым. Если префикс данного правила

содержит ?, то в каждом совместимом с данным префиксом мире долж-

на порождаться новая константа, если только применение правила не

стало избыточным.

Упражнения к § 16.6

16.6.1. Разработайте быстрый алгоритм для проверки совместимость

префиксов.

Замечание для профессионалов. Данная формула была изобретена С. Крипке для

иллюстрации того, что в интуиционистском выводе и в интуиционистских таблицах

нужно, в отличие от классических, иногда по два раза разбивать одну и ту же пропо-

зициональную формулу. У нас оказалось достаточно одного раза из-за механизма ото-

ждествлений префиксов.

448

ГЛАВА 16. ИНТУИЦИОНИСТСКАЯ ЛОГИКА

16.6.2. (A ⇒ B ∨ C) ⇒ (A ⇒ B) ∨ (A ⇒ C).

16.6.3.

¬¬

(A ∨

16.6.4.

(A & B) ⇒

A ∨

16.6.5.

¬¬

∀x(A(x) ∨

A(x))

§ 16.7. ПОЛНОТА СЕМАНТИЧЕСКИХ ТАБЛИЦ

Как было замечено при доказательстве теоремы полноты классической

логики, полнота и корректность — первое, что необходимо доказывать

для нового формализма.

Те достаточно общие способы доказательства, которые были при-

менены для классической логики, также переносятся на доказательство

полноты многих систем семантических таблиц для неклассических ло-

гик. Интуиционистская логика показательна здесь типичностью приме-

няемых для нее модификаций, поэтому доказательство придется вновь

провести подробно (исключая те моменты, которые полностью анало-

гичны ходам, примененным для классической логики).

Начнем с обоснования сокращающих правил, специфических для

интуиционистской логики.

Предложение 16.7.1. Если на данном уровне в секвенции имеется лишь

единственная формула: отвергаемая формула, требующая подъема на

новый уровень, то новый уровень можно не вводить.

Доказательство. Пусть на уровне

α = α

∗[i] у нас имеется лишь фор-

мула α =|

A. Тогда, поскольку после разбиения формулы α =|

A на

уровне α больше не останется формул, формулы, специфицированные

на уровне α, в дальнейшем появиться не могут.

Предложение 16.7.2. Одну и ту же формулу достаточно на одном и

том же пути префиксов разбивать не более одного раза (многократно

используемую — не более одного раза по каждой константе).

Доказательство. Необходимость многократного разбиения может воз-

никнуть лишь для правил |=⇒ и |=

. Здесь возникают отвергаемые

формулы, которые автоматически не могут быть перенесены на следу-

ющие уровни. Детально разберем варианты, возникающие в |=⇒.

16.8. ИНТУИЦИОНИСТСКИЕ ДОКАЗАТЕЛЬСТВА

449

Если разбивается формула [α, ?] |= A ⇒ B, то в подтаблицах по-

являются формулы [α, ?] |= B и [α, ?] =| A. Первая из них сохраняет-

ся при переходе вверх по таблице, вторая не сохранялась бы, если бы

не было звездочки. Таким образом, при повторном разбиении такой же

формулы на более высоком уровне мы получаем такие же формулы с

более узкими спецификациями, которые являются избыточными

После сделанных замечаний конструкция теоремы полноты класси-

ческой логики переносится на интуиционистские семантические табли-

цы.

§ 16.8. ФУНДАМЕНТАЛЬНЫЕ РЕЗУЛЬТАТЫ

ТЕОРИИ ДОКАЗАТЕЛЬСТВ

Интуиционистская логика — одна из немногих логических систем, на

которые переносятся все главные результаты теории доказательств для

классической логики.

Система естественного вывода для интуиционистской логики обра-

зуется из классической системы заменой правила доказательства от про-

тивного на правило

ex falso quodlibet

Первым нетривиальным результатом теории доказательств для интуи-

ционисткой логики был следующий.

Предложение 16.8.1. (Теорема Гливенко)Классическая логика изоморф-

но погружается в интуиционистскую.

Доказательство. Построим следующее погружение классческой логи-

ки в интуциционистскую:

G(A) =

¬¬

A (A элементарна)

G(A & B) = G(A) & G(B)

G(A ∨ B) =

(

G(A) &

G(B))

G(A ⇒ B) = G(A) ⇒ G(B)

A) =

G(A)

G(∀x A) = ∀x G(A)

G(∃x A) =

∀x

G(A)

Итак, систематически устраняются дизъюнкция и существование.

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

450

ГЛАВА 16. ИНТУИЦИОНИСТСКАЯ ЛОГИКА

Этот результат произвел шокирующее впечатление.Ослабив одну из

логических аксиом, мы получили на самом деле более сильную систему,

включающую классическую логику как подсистему. Но, надеюсь, Вы

уже привыкли к тому, что самоограничение и отказ от лишнего слиш-

ком часто на самом деле означает получение дополнительных возмож-

ностей.

Теоремы устранения сечений и нормализуемости доказываются по-

чти одинаково для классической и инутционистской логики (на самом

деле они и впервые были установлены для них одновременно). В прави-

лах нормализации заменяется лишь правило, связанное с отрицанием,

когда вслед за введением отрицания идет его удаление.

∗ A



A A

⇒

(16.27)

При переносе на интуиционистскую логику теоремы Крейга об интер-

поляции опять пользуемся семантической таблицей. А из теоремы Крей-

га следует теорема Бета об определимости.

§ 16.9. РЕАЛИЗУЕМОСТИ И ВАРИАЦИИ

ИНТУИЦИОНИСТСКИХ ПРИНЦИПОВ

Рекурсивная реализуемость Клини может рассматриваться как непосред-

ственная конкретизация колмогоровской интерпретации следующим

образом:

1. Все функции — алгоритмы.

2. Во избежание трудностей с функционалами высших типов все

функции отождествляются с их программами, а эти программы

кодируются натуральными числами, так что формально все реа-

лизации — натуральные числа.

3. Все алгоритмы, в том числе и частично определенные, допуска-

ются в качестве функций.

4. При работе с программами функций мы не интересуемся вычи-

сляемой данной программой функцией, программа рассматрива-