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

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

Семантика модальной логики

Основная статья: Модальная логика

Язык пропозициональной модальной логики состоит из счетного бесконечного множества пропозициональных переменных , набора истинностно-функциональных связок (в данной статье $\to$ и $\neg$) и модальный оператор $\Box$ ("обязательно"). Модальный оператор $\Diamond$ («возможно») является (классически двойственным ) $\Box$ и может быть определен с точки зрения необходимости следующим образом: $\Diamond A:=\neg \Box \neg A$ («возможно А» определяется как эквивалент «не обязательно не А»).

Основные определения

Кадр Крипке , или модальный фрейм, представляет собой пару. $\langle W,R\rangle$, где W — множество (возможно, пустое), а — бинарное отношение на W. R ЭлементыW известен называются узлами или мирами , а R как отношение доступности .

Модель Крипке представляет собой тройку $\langle W,R,\Vdash \rangle$, где $\langle W,R\rangle$ является фреймом Крипке, а $\Vdash$ — это связь между узлами W и модальными формулами, такая, что для всех w ∈ W и модальных формул A и B :

• $w\Vdash \neg A$ тогда и только тогда, когда $w\nVdash A$,
• $w\Vdash A\to B$ тогда и только тогда, когда $w\nVdash A$ или $w\Vdash B$,
• $w\Vdash \Box A$ тогда и только тогда, когда $u\Vdash A$ для всех $u$ такой, что $w\;R\;u$.

Мы читаем $w\Vdash A$ как « w удовлетворяет A », « A удовлетворяется в w », или« w силы А ». Отношение $\Vdash$ называется Отношение удовлетворения , оценка или принуждения отношение .Отношение удовлетворенности однозначно определяется своимзначение пропозициональных переменных.

Формула А действительна в :

• модель $\langle W,R,\Vdash \rangle$, если $w\Vdash A$ для всех w ∈ W ,
• рамка $\langle W,R\rangle$, если оно действительно в $\langle W,R,\Vdash \rangle$ для всех возможных вариантов $\Vdash$,
• класс C фреймов или моделей, если он действителен для каждого члена C .

Мы определяем Thm( C ) как набор всех формул, действительных в С. ​И наоборот, если X — набор формул, пусть Mod( X ) — этокласс всех фреймов, которые подтверждают каждую формулу X. из

. набор формул) L корректна с Модальная логика (т. е относительно класса шкал C , если L ⊆ Thm( C ). L есть полным относительно C , если L ⊇ Thm( C ).

Соответствие и полнота

Семантика полезна для исследования логики (т. е. системы вывода ) только в том случае, если отношение семантического следствия отражает его синтаксический аналог, отношение синтаксического следствия ( выводимость ). Крайне важно знать, какая модальная логика является правильной и полной по отношению к классу фреймов Крипке, а также определить, какой это класс.

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

Нормальная модальная логика L соответствует классу фреймов C , если C = Mod( L ). Другими словами, C — это самый большой класс кадров, в котором является достоверным относительно C. L Отсюда следует, что L полна по Крипке тогда и только тогда, когда она полна соответствующего класса.

Рассмотрим схему Т : $\Box A\to A$. T действует в любом рефлексивном фрейме $\langle W,R\rangle$: если $w\Vdash \Box A$, затем $w\Vdash A$поскольку w   R   w . С другой стороны, кадр, которыйподтверждает, что T должен быть рефлексивным: fix w ∈ W иопределите удовлетворение пропозициональной переменной p следующим образом: $u\Vdash p$ тогда и только тогда, когда w   R   u . Затем $w\Vdash \Box p$, таким образом $w\Vdash p$через T , что означает w   R   w, используя определение $\Vdash$. T соответствует классу рефлексивныхРамки Крипке.

Часто гораздо легче охарактеризовать соответствующий класс L, чем доказать его полноту, поэтому соответствие служит руководством к доказательству полноты. Соответствие также используется для показа неполноты модальных логик: предположим, что L ₁ ⊆ L ₂ — нормальные модальные логики, соответствующие одному и тому же классу фреймов, но L ₁ не доказывает все теоремы L ₂ . Тогда L ₁ неполна по Крипке. Например, схема $\Box (A\leftrightarrow \Box A)\to \Box A$ порождает неполную логику, посколькусоответствует тому же классу кадров, что и GL (т.е. транзитивному иобратные обоснованные фреймы), но не доказывает GL -тавтологию $\Box A\to \Box \Box A$.

Общие схемы модальных аксиом

В следующей таблице перечислены общие модальные аксиомы вместе с соответствующими классами. Названия аксиом часто различаются; Здесь аксиома К названа в честь Саула Крипке ; аксиома T названа в честь аксиомы истины в эпистемической логике ; аксиома D названа в честь деонтической логики ; аксиома B названа в честь Л. Дж. Брауэра ; а аксиомы 4 и 5 названы на основе К.И. Льюиса нумерации систем символической логики .

Имя	Аксиома	Состояние рамы
К	$\Box (A\to B)\to (\Box A\to \Box B)$	справедливо для любых кадров
Т	$\Box A\to A$	рефлексивный : $w\,R\,w$
-	$\Box \Box A\to \Box A$	плотный : $w\,R\,u\Rightarrow \exists v\,(w\,R\,v\land v\,R\,u)$
4	$\Box A\to \Box \Box A$	переходный : $w\,R\,v\wedge v\,R\,u\Rightarrow w\,R\,u$
Д	$\Box A\to \Diamond A$ или $\Diamond \top$ или $\neg \Box \bot$	сериал : $\forall w\,\exists v\,(w\,R\,v)$
Б	$A\to \Box \Diamond A$ или $\Diamond \Box A\to A$	симметричный : $w\,R\,v\Rightarrow v\,R\,w$
5	$\Diamond A\to \Box \Diamond A$	Евклидово : $w\,R\,u\land w\,R\,v\Rightarrow u\,R\,v$
ГЛ	$\Box (\Box A\to A)\to \Box A$	R транзитивный, R −1 обоснованный
Грз	$\Box (\Box (A\to \Box A)\to A)\to A$	R рефлексивный и транзитивный, R −1 − Я вполне обоснован
ЧАС	$\Box (\Box A\to B)\lor \Box (\Box B\to A)$	$w\,R\,u\land w\,R\,v\Rightarrow u\,R\,v\lor v\,R\,u$
М	$\Box \Diamond A\to \Diamond \Box A$	(сложное свойство второго порядка )
Г	$\Diamond \Box A\to \Box \Diamond A$	конвергентный: $w\,R\,u\land w\,R\,v\Rightarrow \exists x\,(u\,R\,x\land v\,R\,x)$
-	$A\to \Box A$	дискретный: $w\,R\,v\Rightarrow w=v$
-	$\Diamond A\to \Box A$	частичная функция : $w\,R\,u\land w\,R\,v\Rightarrow u=v$
-	$\Diamond A\leftrightarrow \Box A$	функция: $\forall w\,\exists !u\,w\,R\,u$ ( $\exists !$ это количественная оценка уникальности )
-	$\Box A$ или $\Box \bot$	пустой: $\forall w\,\forall u\,\neg (w\,R\,u)$

Аксиому K также можно переписать как $\Box [(A\to B)\land A]\to \Box B$, который логически устанавливает modus ponens как правило вывода во всех возможных мирах.

Заметим, что для D аксиомы $\Diamond A$ неявно подразумевает $\Diamond \top$, что означает, что для каждого возможного мира в модели всегда существует хотя бы один возможный мир, доступный из нее (который может быть самим собой). Этот неявный смысл $\Diamond A\rightarrow \Diamond \top$ аналогично неявному импликации квантора существования в диапазоне количественной оценки .

Общие модальные системы

В следующей таблице перечислены несколько распространенных нормальных модальных систем. Условия фреймов для некоторых систем были упрощены: логика верна и полна по отношению к классам фреймов, приведенным в таблице, но они могут соответствовать более широкому классу фреймов.

Имя	Аксиомы	Состояние рамы
К	—	все кадры
Т	Т	рефлексивный
К4	4	переходный
С4	Т, 4	Предварительный заказ
С5	Т, 5 или Д, Б, 4	отношение эквивалентности
С4.3	Т, 4, Ч	общий предзаказ
С4.1	Т, 4, М	Предварительный заказ, $\forall w\,\exists u\,(w\,R\,u\land \forall v\,(u\,R\,v\Rightarrow u=v))$
С4.2	Т, 4, Г	направленный предзаказ
ГЛ , K4W	ГЛ или 4, ГЛ	конечный строгий частичный порядок
Грз, С4Грз	Грз или Т, 4, Грз	конечный частичный порядок
Д	Д	сериал
Д45	Д, 4, 5	транзитивный, серийный и евклидов

Канонические модели

Для любой нормальной модальной логики L можно построить модель Крипке (называемую канонической моделью ), которая в точности опровергает не-теоремы L , путем адаптации стандартной техники использования максимальных непротиворечивых множеств в качестве моделей. Канонические модели Крипке играют роль, аналогичную конструкции алгебры Линденбаума–Тарского в алгебраическихсемантика.

Набор формул является L - непротиворечивым, если из него нельзя вывести противоречие с помощью теорем L и Modus Ponens. Максимальное L-согласованное множество ( L - MCS для краткости) — это L -согласованное множество, не имеющее собственного L -согласованного надмножества.

Каноническая модель L . является моделью Крипке $\langle W,R,\Vdash \rangle$, где W — множество всех L - MCS ,и отношения R и $\Vdash$ следующие:

$X\;R\;Y$ тогда и только тогда, когда для каждой формулы $A$, если $\Box A\in X$ затем $A\in Y$,

$X\Vdash A$ тогда и только тогда, когда $A\in X$.

Каноническая модель является моделью L , поскольку каждый L - MCS содержитвсе Л. теоремы По лемме Цорна каждое L -непротиворечивое множествосодержится в L - MCS , в частности, каждая формуланедоказуемое в L имеет контрпример в канонической модели.

Основное применение канонических моделей — доказательства полноты. Из свойств канонической модели K непосредственно вытекает полнота K относительно класса всех шкал Крипке.Этот аргумент не работает для произвольного L , поскольку нет гарантии, что базовый канонической модели удовлетворяет условиям фрейма L. фрейм

Мы говорим, что формула или множество X формул каноничны. относительно свойства P шкал Крипке, если

• X действителен в каждом кадре, который удовлетворяет P ,
• для любой нормальной модальной логики L , которая содержит X основной фрейм канонической модели L удовлетворяет P. ,

Объединение канонических множеств формул само по себе является каноническим.Из предыдущего обсуждения следует, что любая логика, аксиоматизированнаяканонический набор формул полон по Крипке и компактный .

Аксиомы T, 4, D, B, 5, H, G (и, следовательно,любая их комбинация) каноничны. ГЛ и Грз нетканоничны, поскольку они некомпактны. Аксиома M сама по себе естьне каноническая (Goldblatt, 1991), а комбинированная логика S4.1 (вболее того, даже К4.1 ) каноничен.

В общем, неразрешимо, верна ли данная аксиома.канонический. Мы знаем хорошее достаточное условие: Хенрик Сальквист выделил широкий класс формул (ныне называемых формулы Сальквиста ) такие, что

• формула Сальквиста канонична,
• класс фреймов, соответствующий формуле Сальквиста, определим первого порядка ,
• существует алгоритм, который вычисляет соответствующее условие кадра по заданной формуле Салквиста.

Это мощный критерий: например, все аксиомыперечисленные выше как канонические (эквивалентны) формулам Сальквиста.

Конечное свойство модели

Логика обладает свойством конечной модели (FMP), если она полна.относительно класса конечных фреймов. Применение этогопонятие — это вопрос разрешимости : оноследует из Теорема Поста о том, что рекурсивно аксиоматизированная модальная логика L которая имеет FMP, разрешима при условии, что разрешимо, является ли данноеконечный фрейм является моделью L . В частности, каждое конечноеаксиоматизируемая логика с FMP разрешима.

Существуют различные методы установления FMP для заданной логики.Уточнения и расширения конструкции канонической модели частоработать, используя такие инструменты, как фильтрация или разгадывание . В качестве еще одной возможностидоказательства полноты, основанные на без разрезов исчислении секвенций , обычно создают конечные модели.напрямую.

Большинство используемых на практике модальных систем (включая все перечисленные выше) имеют ФМП.

В некоторых случаях мы можем использовать FMP, чтобы доказать полноту логики по Крипке:любая нормальная модальная логика полна относительно класса модальные алгебры , а конечная модальная алгебра может быть преобразованав систему Крипке. В качестве примера Роберт Булл доказал с помощью этого методачто каждое нормальное расширение S4.3 имеет FMP и является крипкеполный.

Мультимодальная логика

См. Также: Мультимодальная логика

Семантика Крипке имеет прямое обобщение на логику сболее одной модальности. Фрейм Крипке для языка с $\{\Box _{i}\mid \,i\in I\}$ как множество его операторов необходимостисостоит из непустого множества W, снабженного бинарными отношениями R _i для каждого i ∈ I . ОпределениеОтношение удовлетворения модифицируется следующим образом:

$w\Vdash \Box _{i}A$ тогда и только тогда, когда $\forall u\,(w\;R_{i}\;u\Rightarrow u\Vdash A).$

Упрощенная семантика, открытая Тимом Карлсоном, часто используется дляполимодальные логики доказуемости . Модель Карлсона – это структура $\langle W,R,\{D_{i}\}_{i\in I},\Vdash \rangle$с одним отношением доступности R и подмножествами D _i ⊆ W для каждой модальности. Удовлетворениеопределяется как

$w\Vdash \Box _{i}A$ тогда и только тогда, когда $\forall u\in D_{i}\,(w\;R\;u\Rightarrow u\Vdash A).$

Модели Карлсона легче визуализировать и работать с ними, чем обычно.полимодальные модели Крипке; существуют, однако, полные полимодальные крипкелогики, которые являются неполными по Карлсону.

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

Семантика Крипке для интуиционистской логики следует тем же принципам, что и семантика модальной логики, но использует другое определение удовлетворения.

Интуиционистская модель Крипке представляет собой тройку $\langle W,\leq ,\Vdash \rangle$, где $\langle W,\leq \rangle$ представляет собой предзаказную рамку Крипке, а $\Vdash$ удовлетворяет следующим условиям:

• если p - пропозициональная переменная, $w\leq u$, и $w\Vdash p$, затем $u\Vdash p$ ( постоянства условие (ср. монотонность )),
• $w\Vdash A\land B$ тогда и только тогда, когда $w\Vdash A$ и $w\Vdash B$,
• $w\Vdash A\lor B$ тогда и только тогда, когда $w\Vdash A$ или $w\Vdash B$,
• $w\Vdash A\to B$ тогда и только тогда, когда для всех $u\geq w$, $u\Vdash A$ подразумевает $u\Vdash B$,
• нет $w\Vdash \bot$.

Отрицание A , ¬ A можно определить как сокращение от A → ⊥. Если для всех u таких, что w ⊩ u , а не ⊩ A , то w ⊩ A → ⊥ бессмысленно истинно , поэтому w ⊩ ¬ A. u

Интуиционистская логика здрава и полна по отношению к своей теории Крипке.семантику и обладает свойством конечной модели .

Интуиционистская логика первого порядка

Пусть L — язык первого порядка . Крипкемодель L представляет собой тройку $\langle W,\leq ,\{M_{w}\}_{w\in W}\rangle$, где $\langle W,\leq \rangle$ — интуиционистская шкала Крипке, M _w —(классическая) L -структура для каждого узла w ∈ W иследующие условия совместимости выполняются всякий раз, когда u ≤ v :

• домен M _u включен в домен M _v ,
• реализации функциональных символов в M _u и M _v согласуются на элементах M _u ,
• для каждого n -арного предиката P и элементов a ₁ ,..., an _∈ в M _u : если P ( a ₁ ,..., ) _an выполняется в M _u , то оно выполняется и M _v .

Учитывая оценку e переменных элементами M _w , мыопределить отношение удовлетворения $w\Vdash A[e]$:

• $w\Vdash P(t_{1},\dots ,t_{n})[e]$ тогда и только тогда, когда $P(t_{1}[e],\dots ,t_{n}[e])$ выполняется в M _w ,
• $w\Vdash (A\land B)[e]$ тогда и только тогда, когда $w\Vdash A[e]$ и $w\Vdash B[e]$,
• $w\Vdash (A\lor B)[e]$ тогда и только тогда, когда $w\Vdash A[e]$ или $w\Vdash B[e]$,
• $w\Vdash (A\to B)[e]$ тогда и только тогда, когда для всех $u\geq w$, $u\Vdash A[e]$ подразумевает $u\Vdash B[e]$,
• нет $w\Vdash \bot [e]$,
• $w\Vdash (\exists x\,A)[e]$ тогда и только тогда, когда существует $a\in M_{w}$ такой, что $w\Vdash A[e(x\to a)]$,
• $w\Vdash (\forall x\,A)[e]$ тогда и только тогда, когда для каждого $u\geq w$ и каждый $a\in M_{u}$ , $u\Vdash A[e(x\to a)]$.

Здесь e ( x → a ) — оценка, которая x дает значение a , а в остальном согласуется с e .

Семантика Крипке – Радости

В рамках независимого развития теории снопов примерно в 1965 году стало понятно, что семантика Крипке тесно связана с трактовкой экзистенциальной квантификации в теории топоса . То есть «локальный» аспект существования участков связки был своего рода логикой «возможного». Хотя эта разработка была работой ряда людей, семантика имени Крипке-Джойала в этой связи часто используется .

Модельные конструкции

Как и в классической теории моделей , существуют методыпостроение новой модели Крипке из других моделей.

Естественные гомоморфизмы в семантике Крипке называются p-морфизмы (сокращение от псевдоэпиморфизма , нопоследний термин используется редко). p-морфизм фреймов Крипке. $\langle W,R\rangle$ и $\langle W',R'\rangle$ это отображение $f\colon W\to W'$ такой, что

• f сохраняет отношение доступности, т. е. u R v влечет f ( u ) R'   f ( v ),
• всякий раз, когда f ( u ) R'   v ', существует v ∈ W такой, что u R v и f ( v ) = v '.

P-морфизм моделей Крипке $\langle W,R,\Vdash \rangle$ и $\langle W',R',\Vdash '\rangle$ является p-морфизмом ихбазовые фреймы $f\colon W\to W'$, которыйудовлетворяет

$w\Vdash p$ тогда и только тогда, когда $f(w)\Vdash 'p$, для любой пропозициональной переменной p .

P-морфизмы — это особый вид бисимуляций . В целом, бисимуляция между кадрами $\langle W,R\rangle$ и $\langle W',R'\rangle$ это отношение B ⊆ W × W' , что удовлетворяет условиюследующее «зигзагообразное» свойство:

• если u B u' и u R v , существует v' ∈ W' такой, что v B v' и u' R' v' ,
• если u B u' и u' R' v' , существует v ∈ W такой, что v B v' и u R v .

Дополнительно требуется бисимуляция моделей для сохранения воздействияатомных формул :

если w B w' , то $w\Vdash p$ тогда и только тогда, когда $w'\Vdash 'p$, для любой пропозициональной переменной p .

Ключевое свойство, которое следует из этого определения, заключается в том, чтобисимуляции (а значит, и p-морфизмы) моделей сохраняютудовлетворение всех формул, а не только пропозициональных переменных.

Мы можем преобразовать модель Крипке в дерево, используя разгадывание . Учитывая модель $\langle W,R,\Vdash \rangle$ и фиксированныйузел w ₀ ∈ W , определим модель $\langle W',R',\Vdash '\rangle$, где W' —множество всех конечных последовательностей $s=\langle w_{0},w_{1},\dots ,w_{n}\rangle$ такойчто w _i R w _i+1 для всех я < n и $s\Vdash p$ тогда и только тогда, когда $w_{n}\Vdash p$ для пропозициональной переменной п . Определение отношения доступности R' варьируется; в простейшем случае положим

$\langle w_{0},w_{1},\dots ,w_{n}\rangle \;R'\;\langle w_{0},w_{1},\dots ,w_{n},w_{n+1}\rangle$,

но многим приложениям требуется рефлексивное и/или транзитивное замыканиеэто отношение или подобные модификации.

Фильтрация — полезная конструкция, которая используется для доказательства FMP для многих логик. Пусть X — множествоформулы, замкнутые при взятии подформул. X ​ -фильтрация модель $\langle W,R,\Vdash \rangle$ является отображением f из W в модель $\langle W',R',\Vdash '\rangle$ такой, что

• f — сюръекция ,
• f сохраняет отношение доступности и (в обоих направлениях) удовлетворение переменных p ∈ X ,
• если ж ( ты ) R'   ж ( v ) и $u\Vdash \Box A$, где $\Box A\in X$, затем $v\Vdash A$.

Отсюда следует, что f сохраняет выполнение всех формул из Х. ​В типичных приложениях мы принимаем f как проекциюна фактор W по отношению

u ≡ _X v когда для всех A ∈ X тогда и только тогда , $u\Vdash A$ тогда и только тогда, когда $v\Vdash A$.

Как и в случае с разгадкой, определение доступностиОтношение к частному варьируется.

Общая семантика фрейма

Основным недостатком семантики Крипке является существование неполных логик Крипке, а также полных, но некомпактных логик. Это можно исправить, снабдив фреймы Крипке дополнительной структурой, которая ограничивает набор возможных оценок, используя идеи алгебраической семантики. Это порождает общую семантику фрейма .

Приложения в области информатики

Основные статьи: структура Крипке , система перехода состояний и проверка модели.

Блэкберн и др. (2001) отмечают, что, поскольку реляционная структура представляет собой просто набор вместе с набором отношений в этом множестве, неудивительно, что реляционные структуры можно найти практически повсюду. В качестве примера из теоретической информатики они приводят помеченные системы переходов , которые моделируют выполнение программы . Блэкберн и др. таким образом, утверждайте, что из-за этой связи модальные языки идеально подходят для обеспечения «внутреннего, локального взгляда на реляционные структуры». (стр. XII)

История и терминология

Аналогичная работа, предшествовавшая революционным семантическим прорывам Крипке:

• Рудольф Карнап , по-видимому, был первым, у кого возникла идея о том, что можно задать семантику возможного мира для модальностей необходимости и возможности посредством присвоения функции оценки параметра, который варьируется в пределах возможных миров Лейбница. Баярт развивает эту идею дальше, но ни один из них не дал рекурсивных определений удовлетворения в стиле, введенном Тарским;
• JCC McKinsey и Альфред Тарский разработали подход к моделированию модальных логик, который до сих пор оказывает влияние в современных исследованиях, а именно алгебраический подход, в котором в качестве моделей используются булевы алгебры с операторами. Бьярни Йонссон и Тарский установили представимость булевых алгебр с операторами в терминах фреймов. Если бы эти две идеи были объединены, результатом были бы именно рамочные модели, то есть модели Крипке, созданные за годы до Крипке. Но тогда никто (даже Тарский) не увидел этой связи.
• Артур Прайор , опираясь на неопубликованную работу К. А. Мередита , разработал перевод сентенциальной модальной логики в классическую логику предикатов, который, если бы он объединил ее с обычной теорией моделей для последней, создал бы модельную теорию, эквивалентную моделям Крипке для бывший. Но его подход был решительно синтаксическим и антимодельным.
• Стиг Кангер предложил гораздо более сложный подход к интерпретации модальной логики, но содержащий многие ключевые идеи подхода Крипке. Он первым отметил связь между условиями отношений доступности и Льюиса аксиомами модальной логики в стиле . Однако Кангеру не удалось предоставить доказательство полноты своей системы;
• Яакко Хинтикка в своих статьях дал семантику, вводящую эпистемическую логику, которая представляет собой простую вариацию семантики Крипке, эквивалентную характеристике оценок с помощью максимальных непротиворечивых множеств. Он не дает правил вывода для эпистемической логики и поэтому не может дать доказательство полноты;
• У Ричарда Монтегю были многие ключевые идеи, содержащиеся в работах Крипке, но он не считал их значимыми, поскольку у него не было доказательств полноты, и поэтому не публиковал их до тех пор, пока статьи Крипке не произвели сенсацию в логическом сообществе;
• Эверт Виллем Бет представил семантику интуиционистской логики, основанную на деревьях, которая очень напоминает семантику Крипке, за исключением использования более громоздкого определения удовлетворения.

См. также

• Топология Александрова
• Нормальная модальная логика
• Двумерность
• Грязные детские головоломки

Ссылки

• Блэкберн, П.; де Рейке, М .; Венема, Иде (2002). Модальная логика . Издательство Кембриджского университета. ISBN  978-1-316-10195-7 .
• Булл, Роберт А.; Сегерберг, К. (2012) [1984]. «Базовая модальная логика» . В Габбае, DM; Гентнер, Ф. (ред.). Расширения классической логики . Справочник по философской логике. Том. 2. Спрингер. стр. 1–88. ISBN  978-94-009-6259-0 .
• Чагров А.; Захарьящев, М. (1997). Модальная логика . Кларендон Пресс. ISBN  978-0-19-853779-3 .
• Крессвелл, MJ ; Хьюз, GE (2012) [1996]. Новое введение в модальную логику . Рутледж. ISBN  978-1-134-80028-5 .
• Ван Дален, Дирк (2013) [1986]. «Интуиционистская логика» . В Габбае, Дов М.; Гентнер, Франц (ред.). Альтернативы классической логике . Справочник по философской логике. Том. 3. Спрингер. стр. 225–339. ISBN  978-94-009-5203-4 .
• Даммет, Майкл А.Е. (2000). Элементы интуиционизма (2-е изд.). Кларендон Пресс. ISBN  978-0-19-850524-2 .
• Фиттинг, Мелвин (1969). Интуиционистская логика, теория моделей и принуждение . Северная Голландия. ISBN  978-0-444-53418-7 .
• Гаске, Оливье; Тепло, Андреас; Саид: Билал; Шварцентрубер, Франсуа (2013). Миры Крипке: введение в модальную логику через таблицы . Спрингер. стр. XV, 198. ISBN.  978-3764385033 . Проверено 24 декабря 2014 г.
• Джаквинто, Маркус (2002). В поисках уверенности: Философское описание оснований математики: Философское описание оснований математики . Издательство Оксфордского университета. п. 256. ИСБН  019875244X . Проверено 24 декабря 2014 г.
• Голдблатт, Роберт (2006a). «Математическая модальная логика: взгляд на ее эволюцию» (PDF) . В Габбае, Дов М.; Вудс, Джон (ред.). Логика и модальности в двадцатом веке (PDF) . Справочник по истории логики. Том. 7. Эльзевир. стр. 1–98. ISBN  978-0-08-046303-2 .
• Голдблатт, Роберт (2006b). «Семантика Крипке-Джойала для некоммутативной логики в квантах» (PDF) . В Говернатори, Г.; Ходкинсон, И.; Венема, Ю. (ред.). Достижения в модальной логике . Том. 6. Лондон: Публикации колледжа. стр. 209–225. ISBN  1904987206 .
• Мак Лейн, Сондерс ; Мурдейк, Ике (2012) [1991]. Пучки в геометрии и логике: первое введение в теорию топоса . Спрингер. ISBN  978-1-4612-0927-0 .
• Шохам, Йоав; Лейтон-Браун, Кевин (2008). Мультиагентные системы: алгоритмические, теоретико-игровые и логические основы . Издательство Кембриджского университета. п. 397. ИСБН  978-0521899437 .
• Симпсон, Алекс (1994). Теория доказательств и семантика интуиционистской модальной логики (Диссертация). Эдинбургский исследовательский архив (ERA) .
• Стокхоф, Мартин (2008). «Архитектура значения: Трактат Витгенштейна и формальная семантика» . В Замунере, Эдоардо; Леви, Дэвид К. (ред.). Непреходящие аргументы Витгенштейна . Лондон: Рутледж. стр. 211–244. ISBN  9781134107070 .

Внешние ссылки

• Берджесс, Джон П. «Модели Крипке» . Архивировано из оригинала 20 октября 2004 г.
• Детловс В.; Подниекс, К. «4.4 Конструктивная логика высказываний — семантика Крипке» . Введение в математическую логику . Латвийский университет. Примечание: Конструктивный = интуиционистский.
• Гарсон, Джеймс (23 января 2023 г.). «Модальная логика» . В Залте, Эдвард Н. (ред.). Стэнфордская энциклопедия философии .
• «Модели Крипке» , Математическая энциклопедия , EMS Press , 2001 [1994]
• Мошовакис, Джоан (16 декабря 2022 г.). «Интуиционистская логика» . В Залте, Эдвард Н. (ред.). Стэнфордская энциклопедия философии .