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

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

17.2. МОДАЛЬНЫЕ ЛОГИКИ И ИХ МОДЕЛИ КРИПКЕ

461

же сигнатурой. А уж если говорить об объектно-ориентированном про-

граммировании, здесь аналогия с моделями еще более прямая, посколь-

ку изменяются не только значения констант, но и алгоритмы функций.

§ 17.2. МОДАЛЬНЫЕ ЛОГИКИ И ИХ МОДЕЛИ КРИПКЕ

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

щая идея моделей Крипке.

17.2.1. Язык и общая конструкция модели

Чуть-чуть обобщим определение моделей Крипке 16.5.1.

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

Пусть задан некоторый класс моделей

сигнату-

ры

(например, алгебраические модели, или классические модели, или

реализационные).

Общая модель Крипке K

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

над классом моделей

—

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

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

, на-

зываемой

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

, элементам

универса ко-

торой

сопоставлены модели

∈ Ξ

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

назы-

ваются

(возможными) интерпретациями

либо

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

В обозначении

обычно будем опускать

. Если в моделях определе-

но понятие универса, то универс мира

p ∈ W

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

Простейший и наиболее часто рассматриваемый вид моделей Крип-

ке — реляционные системы с одним бинарным отношением R, обычно

называемым отношением достижимости. Естественно определяются

две новые логические связки в таких моделях. A читается “необхо-

димо A” и естественно интерпретируется как истинность A во всех воз-

можных мирах, достижимых из нынешнего. ♦A читается “возможно A”

и естественно интерпретируется как истинность A в некотором возмож-

ном мире, достижимом из нынешнего. Таким образом, имеем следую-

щие определения семантики необходимости и возможности:

p |= A ⇔ ∀q(p R q ⇒ q |= A),

p |= ♦A ⇔ ∃q(p R q & q |= A).

(17.8)

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

ными связками (традиционными модальностями) называются в насто-

462

ГЛАВА 17. СЕМАНТИКИ КРИПКЕ

ящее время модальными. Практически всегда семантика модальностей

задается именно так, как мы только что разобрали.

Есть одно свойство модальностей, которое всегда выполнено при

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

надстройка, — классическая):

(A ⇔

♦

A) & (♦A ⇔



A).

Таким образом,в классической модальной логике достаточно взять одну

из модальностей, вторая определяется через нее.

17.2.2. Свойства отношения достижимости

и конкретные логики

На модальную логику переносится техника семантических таблиц (она

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

нятия модели Крипке). Так же, как и в интуиционистской логике, специ-

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

ность миров, связанных отношением достижимости, ведущая из ны-

нешнего мира в тот, в котором рассматривается формула. В этом пре-

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

один мир. Например, префикс [1,?,2,?,5] означает, что мы идем из исход-

ного мира в мир 1, оттуда в любой из миров, связанных с 1 отношением

достижимости, оттуда в мир 2, и так далее. Рассмотрим пример семан-

тической таблицы.

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

[ ] =| ♦A & ♦B

[ ] |= ♦(A & B)

[1] |= A & B

[1] |= A [1] |= B

[ ] =| ♦A [ ] =| ♦B

[?] =| A [?] =| B

В данном случае семантическая таблица закрылась, и, таким образом,

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

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

можных миров. Но рассмотрим еще одну простую формулу.

[ ] =| A ⇒ ♦A

[ ] |= A [ ] =| ♦A

[?] =| A

17.2. МОДАЛЬНЫЕ ЛОГИКИ И ИХ МОДЕЛИ КРИПКЕ

463

Есть ли здесь противоречие и закрывается ли таблица? Только в том слу-

чае, если нынешний мир достижим сам из себя, т. е. отношение дости-

жимости рефлексивно. Это предположение крайне естественно, но уже

не универсально.

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

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

формула будет истинна.

Заметим полную аналогию между правилами раскрытия модально-

стей и правилами раскрытия кванторов в обычной семантической та-

блице. Необходимость ведет себя как всеобщность, а возможность —

как существование (это видно и из определения их семантики).

Абсолютная модальная логика (без ограничений на отношение до-

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

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

миров наложены некоторое естественные ограничения. В частности, в

логике S5 предполагается, что отношение достижимости является от-

ношением эквивалентности, а в логике S4 — что оно рефлексивно и

транзитивно. Другие логики насчитываются уже сотнями, если не ты-

сячами...

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

Постройте семантические таблицы, и, если формула не абсолют-

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

обладать отношение достижимости, чтобы она была истинной.

17.2.1.

A ⇒ ♦A.

17.2.2.

♦A & ♦B ⇒ ♦(A & B).

17.2.3.

A ⇒ A.

17.2.4.

A & B ⇒ (A & B).

17.2.5.

A ⇒ ♦A.

17.2.6.

♦A ⇒ A.

17.2.3. Нешкальные логики

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

Логика

называется

шкальной

,если есть класс си-

стем миров

, такой, что для всякой модели Крипке

, с

K ∈ L

, все

464

ГЛАВА 17. СЕМАНТИКИ КРИПКЕ

теоремы

истинны на

, и для любой формулы, не выводимой в

найдется модель с системой миров из

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

Итак, шкальные логики можно охарактеризовать классом моделей,

в котором конкретные миры не ограничиваются, ограничивается лишь

структура миров.

Не все логики можно задать таким способом. Рассмотрим простей-

ший пример.

Принцип

♦A ⇒ ♦A (17.9)

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

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

на быть истинной еще во многих других мирах. Формула

♦A & ♦B ⇒

♦(A & B) не выводится в данной логике, требует для своего опровер-

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

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

пределение истинностных значений, при которых (17.9) не выполнена.

§ 17.3. ВАРИАЦИИ НА ТЕМУ МОДАЛЬНОСТЕЙ И КРИПКЕ

17.3.1. Временные, динамические и программные логики

Миры понимаются как срезы одного и того же Мира в разные моменты

времени. Рассматривается модели Крипке с несколькими отношениями,

моделирующими отношения на временной оси. Например, если взять

отношения «предшествовать по времени» и «непосредственно предше-

ствовать по времени», то естественно определяются логики с модаль-

ностями “завтра будет A”, “когда-то было A” и так далее.

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

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

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

венно, программу (в динамических логиках) или оператор программы

(в программных логиках) как преобразующую эти миры модальность,

и далее поступать аналогично.

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

гике записывается как

(A ⇒ αB) & (B ⇒ βC) ⇒ (A ⇒ α; βC), (17.10)

17.3. ВАРИАЦИИ НА ТЕМУ МОДАЛЬНОСТЕЙ И КРИПКЕ

465

а в программной —

A{S

}B & B{S

}C ⇒ A{S

; S

}C. (17.11)

Здесь можно рекомендовать книгу [13].

Глава 18. Проблема отрицания

§ 18.1. ТРИ СТОРОНЫ КЛАССИЧЕСКОГО ОТРИЦАНИЯ

И ЧЕТВЕРТАЯ — СОДЕРЖАТЕЛЬНОГО

Отрицание — та связка, которая доставляла наибольшие неприятности

в неклассических логиках. Дело в том, что в классическом отрицании

соединены три стороны, гармонически сочетающиеся в классической

логике, но сразу расходящиеся при отступлении от нее.

Первая сторона отрицания состоит в алгоритме формулировки от-

рицаний (§ 4.6). Такой способ отрицания назовем прямым отрицанием.

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

иционистской логике жаль их исчезновения. Сформулируем эти прави-

ла в виде законов, обобщающих законы де Моргана. Соответствующий

вариант отрицания естественно обозначать −.

−(A & B) = −A ∨ −B −(A ∨ B) = −A & −B (18.1)

−−A = A −(A ⇒ B) = A & −B (18.2)

−∀x A = ∃x −A −∃x A = ∀x −A (18.3)

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

цание в неклассической логике сформулировано хорошо, но, как уже

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

Вторая сторона отрицания состоит в выведении из данного пред-

положения явно неприемлемых следствий (редукционное,или дедуктив-

ное, отрицание). На нее было обращено большое внимание Карри и

Марковым. Здесь определение отрицания просто:

из A следует неприемлемое утверждение F .

(18.4)

18.1. ЧЕТЫРЕ СТОРОНЫ

467

Правилом,подчеркивающим эту сторону отрицания,является reductio

ad absurdum:

A ⇒ F

(18.5)

где

F — какое-либо неприемлемое утверждение. Карри ввел даже мно-

жество контраксиом, каждая из которых служит основанием для отри-

цания.

Пример 18.1.1.

М.Крейнович [19]применил данный вид отрицания для

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

тических утверждений. Он вывел из них закон исключенного третьего.

Закон исключенного третьего имеет максимальную степень интуицио-

нистской неприемлемости среди классически истинных формул логи-

ки предикатов. Поэтому рассуждение Крейновича показало, в частно-

сти, что утверждение о существовании верхней грани у любого огра-

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

неприемлемо, а вот лемму Гейне-Бореля о возможности выбрать конеч-

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

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

конструктивного анализа.

Третья сторона отрицания состоит в том, что

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

не может быть никогда (тривиализирующее отрицание)

. Ее отражает

правило ex falso quodlibet (из лжи следует все):

(18.6)

Карри еще в 30-е годы заметил, что подобное правило может оказать-

ся определением противоречивости для систем без отрицания: система

противоречива по Карри, если в ней выводимы все формулы. Более то-

го, оно может служить основой для введения отрицания в безотрица-

тельный язык.

Пример 18.1.2.

Рассмотрим формальную арифметику, из которой уда-

лены отрицание и, соответственно, аксиома

∀n

n + 1 = 0

. Если к ней

добавить аксиому

0 = 1

, она становится противоречивой по Карри. До-

кажем это.

Прежде всего докажем по индукции

∀n 0 = n

Базис

0 = 0

Этого быть не может, потому что этого не может быть никогда!

468

ГЛАВА 18. ПРОБЛЕМА ОТРИЦАНИЯ

Шаг

. Пусть

0 = n

, где

— произвольное. Докажем

0 = n + 1

Поскольку

0 = n

, имеем

1 = n + 1

(по аксиоме

∀x, y(x = y ⇒ x + 1 =

y + 1)

). Тогда по транзитивности равенства

0 = n+1

, что и требовалось

доказать.

Отсюда по аксиоме равенства следует

∀x, y x = y

.Подстановкой по-

лучаем произвольную элементарную формулу

t = u

А теперь индукцией по построению

произвольной

формулы

дока-

зываем, что она выводима. В самом деле, для элементарных это доказа-

но, а далее, поскольку все наши связки ведут от истинных к истинным

(нет отрицания), это легко видеть.

Итак, формула

A ⇒ 0 = 1 (18.7)

является полноценной заменой отрицания в арифметике.

Более того, в классической безотрицательной арифметике она сразу

же оказывается полноценным классическим отрицанием. В самом деле,

закон приведения к абсурду, очевидно, выполнен, поскольку

⊥

опреде-

лена как

0 = 1

A ∨

является частным случаем классической тавто-

логии

A ∨ (A ⇒ B).

Четвертая сторона отрицания была первоначально предложена

Брауэром в качестве определения конструктивного смысла отрицания,

но Брауэр сразу же отказался от своей идеи. Это — определение отрица-

ния A как такого действия, которое препятствует реализации (либо

обоснованию) A (превентивное отрицание).

§ 18.2. МИНИМАЛЬНАЯ ЛОГИКА

Минимальную логику предложил Иогансон как исправление интуици-

онистской логики в связи с тем, что она не отказалась от казавшегося

парадоксальным закона ex falso quodlibet. Он просто устранил это пра-

вило из гейтинговской формализации.

После такой модификации отрицание стало действительно очень сла-

бым высказыванием. Оно сохранило лишь одну сторону классического

отрицания — редукционное отрицание.

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

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

виальной. Но тем не менее она в каком-то смысле вырожденна.

18.2. МИНИМАЛЬНАЯ ЛОГИКА

469

Предложение 18.2.1. В минимальной логике из противоречия выводит-

ся отрицание любой формулы.

Доказательство. В самом деле, если у нас имеется противоречие

B и

, то мы можем импортировать его в любой вспомогательный вывод.

После импорта мы можем, предположив A, заключить по правилу при-

ведения к абсурду (которое сохраняется)

Пример 18.2.1.

Рассмотрим интерпретацию лжи как истины

.Тогда пра-

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

из всего что угодно. Значит, данная интерпретация моделирует мини-

мальную логику. Но в такой интерпретации истинна (либо реализуема)

любая формула вида

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

отрицания. Из 0 = 1 выводима с помощью аксиомы индукции любая

позитивная формула.

Таким образом, в реальных аксиоматических теориях минимальная

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

ской, и поэтому представляет интерес лишь для перепроверки области

применения интуиционистских результатов.

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

18.2.1. Дайте определение модели Крипке для минимальной логики.

18.2.2. Проверьте, будут ли минимально доказуемы следующие форму-

лы:

(A ∨ B) &

A ⇒ B.

(

¬¬

A ⇒ A) & (

¬¬

A ∨

A) ⇒ (A ∨

A).

(

A ∨ B) ⇒ (A ⇒ B).

(A & B) ⇒

A ∨

B ⇒

(A & B)

∃x A(x) ⇒ ∀x

A(x)

18.2.3. Догадайтесь, на что заменить в арифметике без отрицания акси-

ому

∀x

x = 0.

Именно так!

470

ГЛАВА 18. ПРОБЛЕМА ОТРИЦАНИЯ

18.2.4. Каково соотношение безотрицательных фрагментов минималь-

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

§ 18.3. ЛОГИКА С СИЛЬНЫМ ОТРИЦАНИЕМ

Нельсон модифицировал интуиционистскую логику в другом направле-

нии, введя в нее сильное отрицание ∼, определяемое по правилам пря-

мого отрицания, и сохранив ex falso quodlibet. Правила естественного

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

ности для связок и для отрицаний связок. Таким образом, сильное от-

рицание работает по-разному в различных контекстах

. Для обычных

связок правила остаются прежними. Для отрицания исчезает правило

приведения к абсурду, но остается правило

ex falso quodlibet

Устранение

∼⇒ Введение ∼⇒

∼ (A ⇒ B

)

A ∼ B

∼ (A ⇒ B)

(18.8)

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

классическим правилам формулировки отрицаний.В том числе имеется

и два правила для комбинации

∼∼.

Устранение

∼∼ Введение ∼∼

∼∼

∼∼ A

(18.9)

Рассмотрим теперь определение модели Крипке для логики Нельсона.

Структура миров остается такой же,как в интуиционистской логике (см.

определение 16.5.1). В каждом мире теперь элементарная формула мо-

жет иметь одно из трех значений:

>, ⊥ или u, что означает, что значение

формулы в данном мире неизвестно.При подъеме по модели возрастают

как множество истинных, так и множество ложных элементарных фор-

мул (что можно интерпретировать следующим образом: неизвестность

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

янием высказывания, которое в любой момент может быть заменено на

Но, конечно, эти его действия взаимно согласованы, иначе не получилась бы ло-

гическая система, имеющая, как и полагается отличной конструктивной логике, четы-

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

модели Крипке, реализуемость.