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

Эта статья включает в себя список общих ссылок , но он остается в значительной степени непроверенным, поскольку в нем отсутствует достаточное количество соответствующих встроенных ссылок . Пожалуйста, помогите улучшить эту статью, добавив более точные цитаты. ( Апрель 2013 г. ) ( Узнайте, как и когда удалить этот шаблон сообщения )

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

Семантика модальной логики [ править ]

Язык пропозициональной модальной логики состоит из счетного множества из пропозициональных переменных , набора истинности функциональных связок (в этой статье , и ), и модального оператор ( «обязательно»). Модальный оператор ( «возможно») является (классическим) двойным из и может быть определен в терминах необходимости , как так: ( «возможно» определяются как эквивалент « не обязательно не»). ^[1]${\ displaystyle \ to}$${\ displaystyle \ neg}$${\ displaystyle \ Box}$${\ displaystyle \ Diamond}$${\ displaystyle \ Box}$${\ Displaystyle \ Diamond A: = \ neg \ Box \ neg A}$

Основные определения [ править ]

Крипка кадр или модальный кадр представляет собой пару , где W представляет собой (возможно , пустое) множество, а R представляет собой бинарное отношение на W . Элементы W называются узлами или мирами , а R - отношением доступности . ^[2]${\displaystyle \langle W,R\rangle }$

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

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

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

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

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

Определим THM ( C ) как множество всех формул, которые действительны в C . И наоборот, если Х представляет собой набор формул, пусть Mod ( X ) класс всех кадров , которые Validate каждую формулу из X .

Модальная логика (то есть, набор формул) L является звук по отношению к классу кадров С , если L  ⊆ THM ( C ). L является полной WRT С , если L  ⊇ THM ( C ).

Соответствие и полнота [ править ]

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

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

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

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

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

Общие схемы модальных аксиом [ править ]

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

Имя	Аксиома	Состояние рамы
K	${\displaystyle \Box (A\to B)\to (\Box A\to \Box B)}$	Нет данных
Т	${\displaystyle \Box A\to A}$	рефлексивный :${\displaystyle w\,R\,w}$
4	${\displaystyle \Box A\to \Box \Box A}$	переходный :${\displaystyle w\,R\,v\wedge v\,R\,u\Rightarrow w\,R\,u}$
	${\displaystyle \Box \Box A\to \Box A}$	плотный :${\displaystyle w\,R\,u\Rightarrow \exists v\,(w\,R\,v\land v\,R\,u)}$
D	${\displaystyle \Box A\to \Diamond A}$ или же ${\displaystyle \Diamond \top }$	серийный номер :${\displaystyle \forall w\,\exists v\,(w\,R\,v)}$
B	${\displaystyle A\to \Box \Diamond A}$	симметричный  : ${\displaystyle w\,R\,v\Rightarrow v\,R\,w}$
5	${\displaystyle \Diamond A\to \Box \Diamond A}$	Евклидово :${\displaystyle w\,R\,u\land w\,R\,v\Rightarrow u\,R\,v}$
GL	${\displaystyle \Box (\Box A\to A)\to \Box A}$	R транзитивный, R −1 обоснованный
Grz a	${\displaystyle \Box (\Box (A\to \Box A)\to A)\to A}$	R рефлексивно и транзитивно, R −1 - Id хорошо обосновано
ЧАС	${\displaystyle \Box (\Box A\to B)\lor \Box (\Box B\to A)}$	${\displaystyle w\,R\,u\land w\,R\,v\Rightarrow u\,R\,v\lor v\,R\,u}$
M	${\displaystyle \Box \Diamond A\to \Diamond \Box A}$	(сложное свойство второго порядка )
грамм	${\displaystyle \Diamond \Box A\to \Box \Diamond A}$	сходящийся: ${\displaystyle w\,R\,u\land w\,R\,v\Rightarrow \exists x\,(u\,R\,x\land v\,R\,x)}$
	${\displaystyle A\to \Box A}$	дискретный: ${\displaystyle w\,R\,v\Rightarrow w=v}$
	${\displaystyle \Diamond A\to \Box A}$	частичная функция : ${\displaystyle w\,R\,u\land w\,R\,v\Rightarrow u=v}$
	${\displaystyle \Diamond A\leftrightarrow \Box A}$	функция: ${\displaystyle \forall w\,\exists !u\,w\,R\,u}$
	${\displaystyle \Box A}$ или же ${\displaystyle \Box \bot }$	пустой: ${\displaystyle \forall w\,\forall u\,\neg (w\,R\,u)}$

Общие модальные системы [ править ]

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

Имя	Аксиомы	Состояние рамы
K	-	все кадры
Т	Т	рефлексивный
K4	4	переходный
S4	Т, 4	Предварительный заказ
S5	Т, 5 или Д, Б, 4	отношение эквивалентности
S4.3	Т, 4, Н	общий предварительный заказ
S4.1	Т, 4, М	Предварительный заказ, ${\displaystyle \forall w\,\exists u\,(w\,R\,u\land \forall v\,(u\,R\,v\Rightarrow u=v))}$
S4.2	Т, 4, Г	направленный предварительный заказ
GL , K4W	GL или 4, GL	конечный строгий частичный порядок
Grz, S4Grz	Grz или T, 4, Grz	конечный частичный порядок
D	D	серийный
D45	Д, 4, 5	переходные, последовательные и евклидовы

Канонические модели [ править ]

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

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

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

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

${\displaystyle X\Vdash A}$если и только если .${\displaystyle A\in X}$

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

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

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

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

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

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

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

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

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

Свойство конечной модели [ править ]

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

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

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

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

Мультимодальная логика [ править ]

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

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

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

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

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

Семантика интуиционистской логики [ править ]

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

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

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

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

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

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

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

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

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

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

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

См. Несколько иную формализацию в ^[4].

Семантика Крипке – Джояла [ править ]

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

Модельные конструкции [ править ]

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

Естественные гомоморфизмы в семантике Крипке называются p-морфизмами (это сокращение от псевдоэпиморфизма , но последний термин используется редко). P-морфизм шкал Крипке и отображение такое, что${\displaystyle \langle W,R\rangle }$${\displaystyle \langle W',R'\rangle }$${\displaystyle 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-морфизм моделей Крипке и p-морфизм их базовых систем отсчета , который удовлетворяет${\displaystyle \langle W,R,\Vdash \rangle }$${\displaystyle \langle W',R',\Vdash '\rangle }$${\displaystyle f\colon W\to W'}$

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

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

• если 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 ' , то тогда и только тогда , когда для любой пропозициональной переменной p .${\displaystyle w\Vdash p}$${\displaystyle w'\Vdash 'p}$

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

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

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

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

Фильтрация - это полезная конструкция, которая используется для доказательства FMP для многих логик. Пусть X - множество формул, замкнутое относительно взятия подформул. Х -фильтрация модели является отображением F из W в модели таким образом, что${\displaystyle \langle W,R,\Vdash \rangle }$${\displaystyle \langle W',R',\Vdash '\rangle }$

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

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

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

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

Общая семантика кадра [ править ]

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

Приложения для информатики [ править ]

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

История и терминология [ править ]

Подобные работы, предшествовавшие революционным семантическим прорывам Крипке: ^[6]

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

См. Также [ править ]

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

Примечания [ править ]

а ^ По Анджею Гжегорчику .

Ссылки [ править ]

• Blackburn, P .; де Рийке, М .; Венема, Иде (2002). Модальная логика . Издательство Кембриджского университета. ISBN 978-1-316-10195-7.
• Бык, Роберт А .; Сегерберг, К. (2012) [1984]. «Базовая модальная логика» . В Габбее, DM; Guenthner, F. (ред.). Расширения классической логики . Справочник по философской логике. 2 . Springer. С. 1–88. ISBN 978-94-009-6259-0.
• Чагров, А .; Захарящев, М. (1997). Модальная логика . Кларендон Пресс. ISBN 978-0-19-853779-3.
• Даммит, Майкл AE (2000). Элементы интуиционизма (2-е изд.). Кларендон Пресс. ISBN 978-0-19-850524-2.
• Фиттинг, Мелвин (1969). Интуиционистская логика, теория моделей и принуждение . Северная Голландия. ISBN 978-0-444-53418-7.
• Голдблатт, Роберт (2006). "Математическая модальная логика: взгляд на ее развитие" (PDF) . В Габбае, Дов М .; Вудс, Джон (ред.). Логика и модальности в двадцатом веке (PDF) . Справочник по истории логики. 7 . Эльзевир. С. 1–98. ISBN 978-0-08-046303-2.
• Крессуэлл, MJ; Хьюз, GE (2012) [1996]. Новое введение в модальную логику . Рутледж. ISBN 978-1-134-80028-5.
• Мак Лейн, Сондерс ; Moerdijk, Ieke (2012) [1991]. Пучки в геометрии и логике: первое введение в теорию топоса . Springer. ISBN 978-1-4612-0927-0.
• ван Дален, Дирк (2013) [1986]. «Интуиционистская логика» . В Габбае, Дов М .; Гентнер, Франц (ред.). Альтернативы классической логике . Справочник по философской логике. 3 . Springer. С. 225–339. ISBN 978-94-009-5203-4.

Внешние ссылки [ править ]

Викискладе есть медиафайлы по теме моделей Крипке .

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