Семантика Крипке

Семантика Крипке — это формальная семантика для модальных и интуиционистских логик, основанная на понятии возможных миров и отношений достижимости между ними. Разработана американским логиком и философом Солом Крипке в конце 1950-х — начале 1960-х годов. Семантика Крипке, также известная как реляционная семантика или семантика возможных миров, является одним из наиболее влиятельных инструментов в современной математической логике, теоретической лингвистике и философии языка. Она позволяет придать точный математический смысл модальным операторам необходимости (□) и возможности (◇), а также формализовать интуиционистскую логику.

Основные понятия

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

Фундаментальным объектом семантики Крипке является модель Крипке — тройка \( \mathcal{M} = \langle W, R, V \rangle \), где:

• W — непустое множество «возможных миров» (или ситуаций, состояний). Каждый мир представляет собой полное и непротиворечивое описание некоторого положения дел.
• R — бинарное отношение на множестве W, называемое отношением достижимости. Для миров \( w \) и \( v \) запись \( wRv \) означает, что мир \( v \) достижим из мира \( w \). Свойства этого отношения (рефлексивность, транзитивность, симметричность и др.) определяют, какая именно модальная логика описывается моделью.
• V — функция оценки, которая каждому атомарному высказыванию \( p \) ставит в соответствие множество миров \( V(p) \subseteq W \), в которых \( p \) истинно.

Истинность в возможных мирах

Истинность формулы в конкретном мире \( w \) модели \( \mathcal{M} \) определяется рекурсивно. Для атомарных формул истинность задаётся функцией \( V \). Для сложных формул используются следующие правила:

• \( \mathcal{M}, w \models \neg \varphi \) тогда и только тогда, когда неверно, что \( \mathcal{M}, w \models \varphi \).
• \( \mathcal{M}, w \models \varphi \land \psi \) тогда и только тогда, когда \( \mathcal{M}, w \models \varphi \) и \( \mathcal{M}, w \models \psi \).
• \( \mathcal{M}, w \models \varphi \lor \psi \) тогда и только тогда, когда \( \mathcal{M}, w \models \varphi \) или \( \mathcal{M}, w \models \psi \).
• \( \mathcal{M}, w \models \varphi \rightarrow \psi \) тогда и только тогда, когда если \( \mathcal{M}, w \models \varphi \), то \( \mathcal{M}, w \models \psi \).
• \( \mathcal{M}, w \models \Box \varphi \) (необходимо \( \varphi \)) тогда и только тогда, когда для любого мира \( v \), такого что \( wRv \), верно \( \mathcal{M}, v \models \varphi \).
• \( \mathcal{M}, w \models \Diamond \varphi \) (возможно \( \varphi \)) тогда и только тогда, когда существует мир \( v \), такой что \( wRv \) и \( \mathcal{M}, v \models \varphi \).

Формула называется общезначимой в модели \( \mathcal{M} \), если она истинна во всех мирах этой модели. Формула называется общезначимой в классе моделей (например, в классе моделей с рефлексивным отношением), если она истинна во всех мирах всех моделей этого класса.

История

Предпосылки

До появления семантики Крипке модальная логика развивалась преимущественно синтаксически, через аксиоматические системы. Кларенс Льюис в начале XX века разработал системы S1–S5, но их семантическая интерпретация оставалась неясной. В 1940-х годах Рудольф Карнап предложил семантику, основанную на «описаниях состояний», однако она была ограничена и не охватывала все модальные системы.

Разработка Крипке

Сол Крипке, будучи старшеклассником, в 1959 году опубликовал статью «A Completeness Theorem in Modal Logic», где впервые представил реляционную семантику для модальной логики. В последующих работах, включая «Semantical Considerations on Modal Logic» (1963), он обобщил подход и доказал теоремы полноты для основных модальных систем (K, T, S4, S5). Параллельно Крипке разработал семантику для интуиционистской логики, используя частично упорядоченные множества миров.

Влияние

Семантика Крипке произвела революцию в логике, позволив:

• Доказать метатеоремы (полноту, непротиворечивость) для многих логических систем.
• Связать модальные логики с теорией графов и алгебраическими структурами.
• Создать основу для формальной философии (метафизика возможных миров, теория референции).

Виды семантик Крипке

Семантика для нормальных модальных логик

Наиболее распространённый вариант. Отношение достижимости \( R \) может обладать различными свойствами, что соответствует различным аксиомам:

• Рефлексивность (\( \forall w: wRw \)) — аксиома T (\( \Box \varphi \rightarrow \varphi \)).
• Транзитивность (\( \forall w,u,v: (wRu \land uRv) \rightarrow wRv \)) — аксиома 4 (\( \Box \varphi \rightarrow \Box \Box \varphi \)).
• Симметричность (\( \forall w,v: wRv \rightarrow vRw \)) — аксиома B (\( \varphi \rightarrow \Box \Diamond \varphi \)).
• Евклидовость (\( \forall w,u,v: (wRu \land wRv) \rightarrow uRv \)) — аксиома 5 (\( \Diamond \varphi \rightarrow \Box \Diamond \varphi \)).

Комбинации этих свойств порождают известные системы:

• K — минимальная нормальная модальная логика (без ограничений на \( R \)).
• T — рефлексивность.
• S4 — рефлексивность + транзитивность.
• S5 — рефлексивность + транзитивность + симметричность (или евклидовость).

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

В интуиционистской версии семантики Крипке отношение достижимости является частичным порядком (рефлексивным, транзитивным, антисимметричным). Миры интерпретируются как «стадии познания», а истинность формулы означает, что она «установлена» на данной стадии и сохраняется во всех последующих. Ключевое отличие от классической логики: отрицание \( \neg \varphi \) истинно в мире \( w \), если ни в одном достижимом мире \( \varphi \) не установлено.

Семантика с вырожденным отношением

Если отношение \( R \) пусто или является универсальным, получаются вырожденные случаи. Например, если \( R \) — универсальное отношение (\( \forall w,v: wRv \)), то \( \Box \varphi \) эквивалентно истинности \( \varphi \) во всех мирах, а \( \Diamond \varphi \) — в некотором. Это соответствует системе S5.

Применение

Философия и метафизика

Семантика Крипке стала основой для метафизики возможных миров, развитой Крипке в книге «Именование и необходимость» (1972, рус. пер. 1982). Он использовал её для анализа модальных утверждений о сущностях, необходимости и случайности. Например, утверждение «вода есть H₂O» необходимо истинно, если во всех возможных мирах вода имеет тот же химический состав. Крипке также ввёл различие между априорным и необходимым, показав, что эти понятия не совпадают.

Теоретическая лингвистика

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

Информатика и искусственный интеллект

• Верификация программ: семантика Крипке используется в темпоральных логиках (LTL, CTL) для проверки моделей (model checking). Состояния программы интерпретируются как миры, а переходы между ними — как отношение достижимости.
• Базы знаний и рассуждения: модальные логики на основе семантики Крипке применяются в системах, моделирующих знания и убеждения агентов (логика знания, эпистемическая логика).
• Семантика языков программирования: используется для формального описания поведения программ с недетерминизмом и параллелизмом.

Математическая логика

Семантика Крипке является основой для изучения свойств логических систем: полноты, компактности, разрешимости. Она позволяет сводить логические задачи к задачам на графах, что даёт эффективные алгоритмы.

Критика и ограничения

Философская критика

• Реализм возможных миров: некоторые философы (Уиллард Куайн, Дэвид Льюис) критиковали онтологический статус возможных миров. Крипке придерживался «актуализма» — возможные миры не существуют как реальные объекты, а являются лишь абстрактными описаниями.
• Проблема трансмировой идентичности: как идентифицировать один и тот же объект в разных возможных мирах? Крипке предложил концепцию «жёстких десигнаторов» — имён, которые обозначают один и тот же объект во всех мирах, где он существует.

Технические ограничения

• Неполнота: существуют логики, которые не могут быть охарактеризованы классом фреймов Крипке (например, некоторые модальные логики с бесконечными аксиомами). Для таких случаев разработаны обобщения — семантика окрестностей, алгебраическая семантика.
• Сложность: для некоторых логик проблема общезначимости может быть неразрешима (например, для логики с двумя модальностями и транзитивным отношением).

Связанные понятия

• Фрейм Крипке: пара \( \langle W, R \rangle \) без функции оценки. Формула общезначима во фрейме, если она истинна во всех моделях на этом фрейме.
• Теорема полноты: утверждение, что любая общезначимая формула в классе моделей с заданными свойствами выводима в соответствующей аксиоматической системе.
• Каноническая модель: конструкция, используемая для доказательства полноты, в которой мирами являются максимальные непротиворечивые множества формул.

Источники

1. Крипке С. Именование и необходимость. — М.: Либроком, 2010. — 288 с.
2. Крипке С. Семантические соображения о модальной логике // Модальная логика. — М.: Наука, 1991. — С. 115–132.
3. Чёрч А. Введение в математическую логику. — М.: ИЛ, 1960. — Т. 1. — 484 с.
4. Голдблатт Р. Логика времени и вычислений. — М.: Мир, 1986. — 192 с.
5. Fitting M., Mendelsohn R. L. First-Order Modal Logic. — Kluwer Academic Publishers, 1998. — 277 p.
6. Hughes G. E., Cresswell M. J. A New Introduction to Modal Logic. — Routledge, 1996. — 432 p.