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

редактировать

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

Содержание

1 Семантика модальной логики
- 1.1 Основные определения
- 1.2 Соответствие и полнота
  - 1.2.1 Общие схемы модальных аксиом
  - 1.2.2 Общие модальные системы
- 1.3 Канонические модели
- 1.4 Свойство конечной модели
- 1.5 Мультимодальная логика
2 Семантика интуиционистской логики
- 2.1 Интуиционистская логика первого порядка
- 2.2 Семантика Крипке – Джояла
3 Конструкции модели
4 Общая рамка семантика
5 Приложения для информатики
6 История и терминология
7 См. также
8 Примечания
9 Ссылки
10 Внешние ссылки

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

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

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

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

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

$вес ⊩ ¬ A {\ displaystyle w \ Vdash \ neg A}$ $w\Vdash \neg A$ тогда и только тогда, когда $w ⊮ A {\ displaystyle w \ nVdash A}$ $w\nVdash A$ ,
$w ⊩ A → B {\ displaystyle w \ Vdash A \ to B}$ $w\Vdash A\to B$ тогда и только тогда, когда $w ⊮ A {\ displaystyle w \ nVdash A}$ $w\nVdash A$ или $w ⊩ B {\ displaystyle w \ Vdash B}$ $w\Vdash B$ ,
$w ⊩ ◻ A {\ displaystyle w \ Vdash \ Box A}$ $w\Vdash \Box A$ тогда и только тогда, когда $u ⊩ A {\ displaystyle u \ Vdash A }$ $u\Vdash A$ для всех $u {\ displaystyle u}$ $u$ таких, что $w R u {\ displaystyle w \; R \; u}$ $w\;R\;u$ .

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

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

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

Мы определяем Thm (C) как набор всех формул, которые действительны в 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 - это самый большой класс фреймов, таких что L надежна относительно C. Отсюда следует, что L полна по Крипке тогда и только тогда, когда она полна для своего соответствующего класса.

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

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

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

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

Имя	Аксиома	Состояние кадра
K	$◻ (A → B) → (◻ A → ◻ B) {\ displaystyle \ Box (A \ to B) \ to ( \ Box A \ to \ Box B)}$ $\Box (A\to B)\to (\Box A\to \Box B)$	N / A
T	$◻ A → A {\ displaystyle \ Box A \ to A}$ $\Box A\to A$	рефлексивный : $w R w {\ displaystyle w \, R \, w}$ $w\,R\,w$
4	$◻ A → ◻ ◻ A {\ displaystyle \ Box A \ to \ Box \ Box A}$ $\Box A\to \Box \Box A$	транзитивный : $w R v ∧ v R u ⇒ вес R U {\ Displaystyle ш \, R \, v \ клин v \, R \, u \ Rightarrow w \, R \, u}$ $w\,R\,v\wedge v\,R\,u\Rightarrow w\,R\,u$
	$◻ ◻ A → ◻ A {\ displaystyle \ Box \ Box A \ в \ Box A}$ $\Box \Box A\to \Box A$	плотный : $w R u ⇒ ∃ v (w R v ∧ v R u) {\ displaystyle w \, R \, u \ Rightarrow \ exists v \, (w \, R \, v \ land v \, R \, u)}$ $w\,R\,u\Rightarrow \exists v\,(w\,R\,v\land v\,R\,u)$
D	$◻ A → ◊ A {\ displaystyle \ Box A \ to \ Diamond A}$ $\Box A\to \Diamond A$ или $◊ ⊤ { \ Displaystyle \ Diamond \ top}$ $\Diamond \top$	серийный : $∀ w ∃ v (w R v) {\ displaystyle \ forall w \, \ exists v \, (w \, R \, v)}$ $\forall w\,\exists v\,(w\,R\,v)$
B	$A → ◻ ◊ A {\ displaystyle A \ to \ Box \ Diamond A}$ $A\to \Box \Diamond A$	симметричный : $w R v ⇒ v R w {\ displaystyle w \, R \, v \ Rightarrow v \, R \, w}$ $w\,R\,v\Rightarrow v\,R\,w$
5	$◊ A → ◻ ◊ A {\ displaystyle \ Diamond A \ to \ Box \ Diamond A}$ $\Diamond A\to \Box \Diamond A$	евклидово : $w R u ∧ вес R v ⇒ u R v {\ displaystyle w \, R \, u \ land w \, R \, v \ Rightarrow u \, R \, v}$ $w\,R\,u\land w\,R\,v\Rightarrow u\,R\,v$
GL	$◻ (◻ A → A) → ◻ A {\ displaystyle \ Box (\ Box A \ to A) \ to \ Box A}$ $\Box (\Box A\to A)\to \Box A$	R транзитивный, R хорошо обоснованный
Grz	$◻ (◻ (A → ◻ A) → A) → A {\ displaystyle \ Box (\ Box (A \ to \ Box A) \ to A) \ to A}$ $\Box (\Box (A\to \Box A)\to A)\to A$	R рефлексивно и транзитивно, R − Id хорошо обосновано
H	$◻ (◻ A → B) ∨ ◻ (◻ B → A) {\ Displaystyle \ Box (\ Box A \ to B) \ lor \ Box (\ Box B \ to A)}$ $\Box (\Box A\to B)\lor \Box (\Box B\to A)$	$w R u ∧ w R v ⇒ U R v ∨ v R U {\ displaystyle w \, R \, u \ land w \, R \, v \ Rightarrow u \, R \, v \ lor v \, R \, u}$ $w\,R\,u\land w\,R\,v\Rightarro w u\,R\,v\lor v\,R\,u$
M	$◻ ◊ A → ◊ ◻ A {\ displaystyle \ Box \ Diamond A \ to \ Diamond \ Box A}$ $\Box \Diamond A\to \Diamond \Box A$	(сложное свойство второго порядка )
G	$◊ ◻ A → ◻ ◊ A { \ displaystyle \ Diamond \ Box A \ to \ Box \ Diamond A}$ $\Diamond \Box A\to \Box \Diamond A$	сходящийся: $w R u ∧ w R v ⇒ ∃ x (u R x ∧ v R x) {\ displaystyle w \, R \, и \ земля ш \, р \, v \ Rightarrow \ существует х \, (и \, R \, х \ земля v \, R \, x)}$ $w\,R\,u\land w\,R\,v\Rightarrow \exists x\,(u\,R\,x\land v\,R\,x)$
	$A → ◻ A {\ Displaystyle A \ to \ Box A}$ $A\to \Box A$	дискретный: $w R v ⇒ w = v {\ displaystyle w \, R \, v \ Rightarrow w = v}$ $w\,R\,v\Rightarrow w=v$
	$◊ A → ◻ A {\ displ aystyle \ Diamond A \ to \ Box A}$ $\Diamond A\to \Box A$	частичная функция : $w R u ∧ w R v ⇒ u = v {\ displaystyle w \, R \, u \ land w \, R \, v \ Rightarrow u = v}$ $w\,R\,u\land w\,R\,v\Rightarrow u=v$
	$◊ A ↔ ◻ A {\ displaystyle \ Diamond A \ leftrightarrow \ Box A}$ $\Diamond A\leftrightarrow \Box A$	функция: $∀ w ∃! uw R u {\ displaystyle \ forall w \, \ exists! u \, w \, R \, u}$ $\forall w\,\exists !u\,w\,R\,u$
	$◻ A {\ displaystyle \ Box A}$ $\Box A$ или $◻ ⊥ { \ displaystyle \ Box \ bot}$ $\Box \bot$	пустой: $∀ вес ∀ u ¬ (w R u) {\ displaystyle \ forall w \, \ forall u \, \ neg (w \, R \, u)}$ $\forall w\,\forall u\,\neg (w\,R\,u)$

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

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

Имя	Аксиомы	Состояние кадра
K	—	все кадры
T	T	рефлексивный
K4	4	переходный
S4	T, 4	предзаказ
S5	T, 5 или D, B, 4	отношение эквивалентности
S4.3	T, 4, H	общий предварительный заказ
S4.1	T, 4, M	предварительный заказ, $∀ w ∃ u (w R u ∧ ∀ v (u R v ⇒ u = v)) {\ displaystyle \ forall w \, \ существует u \, (w \, R \, u \ land \ forall v \, (u \, R \, v \ Rightarrow u = v))}$ $\forall w\,\exists u\,(w\,R\,u\land \forall v\,(u\,R\,v\Rightarrow u=v))$
S4.2	T, 4, G	направленный предварительный заказ
GL, K4W	GL или 4, GL	конечный строгий частичный порядок
Grz, S4Grz	Grz или T, 4, Grz	конечный частичный порядок
D	D	последовательный
D45	D, 4, 5	переходный, последовательный и Евклидовы

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

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

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

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

XRY {\ displaystyle X \; R \ ; Y}

X\;R\;Y

тогда и только тогда, когда для каждой формулы

A {\ displaystyle A}

A

, если

◻ A ∈ X {\ displaystyle \ Box A \ in X}

\Box A\in X

затем

A ∈ Y {\ displaystyle A \ in Y}

A\in Y

X ⊩ A {\ displaystyle X \ Vdash A}

X\Vdash A

тогда и только тогда, когда

A ∈ X {\ displaystyle A \ in X}

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 ) канонична.

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

формула Сахлквиста является канонической,
класс фреймов, соответствующий Сахлквисту. формула first-order definable,
существует алгоритм, который вычисляет соответствующее условие кадра для данной формулы Сахлквиста.

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

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

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

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

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

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

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

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

w ⊩ ◻ i A {\ displaystyle w \ Vdash \ Box _ {i} A}

w\Vdash \Box _{i}A

тогда и только тогда, когда

∀ u (w R iu ⇒ u ⊩ A). {\ displaystyle \ forall u \, (w \; R_ {i} \; u \ Rightarrow u \ Vdash A).}

\forall u\,(w\;R_{i}\;u\Rightarrow u\Vdash A).

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

w ⊩ ◻ i A {\ displaystyle w \ Vdash \ Box _ {i} A}

w\Vdash \Box _{i}A

тогда и только тогда, когда

∀ u ∈ D i (w R u ⇒ u ⊩ А). {\ displaystyle \ forall u \ in D_ {i} \, (w \; R \; u \ Rightarrow u \ Vdash A).}

\forall u\in D_{i}\,(w\;R\;u\Rightarrow u\Vdash A).

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

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

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

интуиционистская модель Крипке представляет собой тройку $⟨W, ≤, ⊩⟩ {\ displaystyle \ langle W, \ leq, \ Vdash \ rangle}$ $\langle W,\leq,\Vdash \rangle$ , где $⟨W, ≤⟩ {\ displaystyle \ langle W, \ leq \ rangle}$ $\langle W,\leq \rangle$ - это предварительно заказанный фрейм Крипке, а $⊩ {\ displaystyle \ Vdash }$ $\Vdash$ удовлетворяет следующим условиям:

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

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

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

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

Пусть L будет язык первого порядка. Модель Крипке L представляет собой тройку $⟨W, ≤, {M w} w ∈ W⟩ {\ displaystyle \ langle W, \ leq, \ {M_ {w} \} _ {w \ in W} \ rangle}$ $\langle W,\leq,\{M_{w}\}_{w\in W}\rangle$ , где $⟨W, ≤⟩ {\ displaystyle \ langle W, \ leq \ 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 1,..., a n ∈ M u : если P (a 1,..., a n) выполняется в M u, то оно выполняется в M v.

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

$вес ⊩ P (t 1,…, tn) [e] {\ displaystyle w \ Vdash P (t_ {1}, \ dots, t_ {n}) [e]}$ $w\Vdash P(t_{1},\dots,t_{n})[e]$ тогда и только тогда, когда $P (t 1 [e],…, tn [e]) {\ displaystyle P (t _ {1} [e], \ dots, t_ {n} [e])}$ $P(t_{1}[e],\dots,t_{n}[e])$ сохраняется в M w,
$w ⊩ (A ∧ B) [e] {\ displaystyle w \ Vdash (A \ land B) [e]}$ $w\Vdash (A\land B)[e]$ тогда и только тогда, когда $w ⊩ A [e] {\ displaystyle w \ Vdash A [e]}$ $w\Vdash A[e]$ и $w ⊩ B [e] {\ displaystyle w \ Vdash B [e]}$ $w\Vdash B[e]$ ,
$вес ⊩ (A ∨ B) [e] {\ displaystyle w \ Vdash (A \ lor B) [e]}$ $w\Vdash (A\lor B)[e]$ тогда и только тогда, когда $вес ⊩ A [e] {\ displaystyle w \ Vdash A [e]}$ $w\Vdash A[e]$ или $w ⊩ B [e] {\ displaystyle w \ Vdash B [e] }$ $w\Vdash B[e]$ ,
$вес ⊩ (A → B) [e] {\ displaystyle w \ Vdash (A \ to B) [e]}$ $w\Vdash (A\to B)[e]$ тогда и только тогда, когда для всех $u ≥ w {\ displaystyle u \ geq w}$ $u\geq w$ , $u ⊩ A [e] {\ displaystyle u \ Vdash A [e]}$ $u\Vdash A[e]$ подразумевает $u ⊩ B [e] {\ displaystyle u \ Vdash B [ e]}$ $u\Vdash B[e]$ ,
не $вес ⊩ ⊥ [e] {\ displaystyle w \ Vdash \ bot [e]}$ $w\Vdash \bot [e]$ ,
$w ⊩ (∃ x A) [e] {\ displaystyle w \ Vdash (\ существует x \, A) [e]}$ $w\Vdash (\exists x\,A)[e]$ тогда и только тогда, когда существует $a ∈ M w {\ displaystyle a \ in M_ {w}}$ $a\in M_{w}$ такой, что $вес ⊩ A [е (Икс → а)] {\ Displaystyle ш \ Vdash A [е (х \ к а)]}$ $w\Vdash A[e(x\to a)]$ ,
$вес ⊩ (∀ х А) [е] {\ Displaystyl ew \ Vdash (\ forall x \, A) [e]}$ $w\Vdash (\forall x\,A)[e]$ тогда и только тогда, когда для каждого $u ≥ w {\ displaystyle u \ geq w}$ $u\geq w$ и каждого $a ∈ M u {\ displaystyle a \ in M_ {u}}$ $a\in M_{u}$ , $u ⊩ A [e (x → a)] {\ displaystyle u \ Vdash A [e (x \ to a)]}$ $u\Vdash A[e(x\to a)]$ .

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

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

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

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

Построение модели

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

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

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

p-морфизм моделей Крипке $⟨W, R, ⊩⟩ {\ displaystyle \ langle W, R, \ Vdash \ rangle}$ $\langle W,R,\Vdash \rangle$ и $⟨ W ′, R ′, ⊩ ′⟩ {\ displaystyle \ langle W ', R', \ Vdash '\ rangle}$ $\langle W',R',\Vdash '\rangle$ - это p-морфизм их базовых фреймов $f: W → W ′ {\ displaystyle f \ двоеточие W \ to W '}$ $f\colon W\to W'$ , что удовлетворяет

w ⊩ p {\ displaystyle w \ Vdash p}

w\Vdash p

тогда и только тогда, когда

f ( w) ⊩ ′ p {\ displaystyle f (w) \ Vdash 'p}

f(w)\Vdash 'p

, для любой пропозициональной переменной p.

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

if 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 ⊩ p {\ displaystyle w \ Vdash p }

w\Vdash p

тогда и только тогда, когда

w ′ ⊩ ′ p {\ displaystyle w '\ Vdash' p}

w'\Vdash 'p

для любой пропозициональной переменной p.

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

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

⟨w 0, w 1,…, wn⟩ R ′ ⟨w 0, w 1,…, wn, wn + 1⟩ {\ displaystyle \ langle w_ {0}, w_ {1 }, \ dots, w_ {n} \ rangle \; R '\; \ langle w_ {0}, w_ {1}, \ dots, w_ {n}, w_ {n + 1} \ rangle}

\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-фильтрация модели $⟨W, R, ⊩⟩ {\ displaystyle \ langle W, R, \ Vdash \ rangle}$ $\langle W,R,\Vdash \rangle$ - это отображение f из W в модель $⟨ W ′, R ′, ⊩ ′⟩ {\ displaystyle \ langle W ', R', \ Vdash '\ rangle}$ $\langle W',R',\Vdash '\rangle$ такой, что

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

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

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

u ⊩ A {\ displaystyle u \ Vdash A}

u\Vdash A

тогда и только тогда, когда

v ⊩ A {\ displaystyle v \ Vdash A}

v\Vdash A

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

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

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

Приложения для информатики

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

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

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

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

См. также

Примечания

^Шохам, Йоав; Лейтон-Браун, Кевин (2008). Многоагентные системы: алгоритмические, теоретико-игровые и логические основы. Издательство Кембриджского университета. п. 397. ISBN 978-0521899437.
^Гаске, Оливье; и другие. (2013). Миры Крипке: введение в модальную логику через таблицы. Springer. С. 14–16. ISBN 978-3764385033. Проверено 24 декабря 2014 г.
^Джакинто, Маркус (2002). Поиск достоверности: философское изложение основ математики: философское изложение основ математики. Издательство Оксфордского университета. п. 256. ISBN 019875244X. Проверено 24 декабря 2014 г.
^Intuitionistic Logic. Автор Джоан Мощовакис. Опубликовано в Стэнфордской энциклопедии философии.
^Голдблатт, Роберт (2006). «Семантика Крипке-Джояла для некоммутативной логики в квантах» (PDF). In Governatori, G.; Hodkinson, I.; Венема Ю. (ред.). Успехи в модальной логике. 6 . Лондон: публикации колледжа. С. 209–225. ISBN 1904987206.
^Stokhof, Martin (2008). "The architecture of meaning: Wittgenstein's Tractatus and formal semantics". In Zamuner, Edoardo; Levy, David K. (eds.). Wittgenstein's Enduring Arguments. Лондон: Рутледж. pp. 211–244.preprint (See the last two paragraphs in Section 3 Quasi-historical Interlude: the Road from Vienna to Los Angeles.)

References

Blackburn, P.; de Rijke, M. ; Venema, Yde (2002). Modal Logic. Издательство Кембриджского университета. ISBN 978-1-316-10195-7.
Bull, Robert A.; Segerberg, K. (2012) [1984]. "Basic Modal Logic". In Gabbay, D.M.; Guenthner, F. (eds.). Extensions of Classical Logic. Handbook of Philosophical Logic. 2. Springer. С. 1–88. ISBN 978-94-009-6259-0.
Chagrov, A.; Zakharyaschev, M. (1997). Modal Logic. Кларендон Пресс. ISBN 978-0-19-853779-3.
Dummett, Michael A. E. (2000). Elements of Intuitionism (2nd ed.). Кларендон Пресс. ISBN 978-0-19-850524-2.
Fitting, Melvin (1969). Intuitionistic Logic, Model Theory and Forcing. Северная Голландия. ISBN 978-0-444-53418-7.
Goldblatt, Robert (2006). "Mathematical Modal Logic: a View of its Evolution" (PDF). In Gabbay, Dov M.; Woods, John (eds.). Logic and the Modalities in the Twentieth Century (PDF). Справочник по истории логики. 7. Эльзевир. pp. 1–98. ISBN 978-0-08-046303-2.
Cresswell, M.J.; Hughes, G.E. (2012) [1996]. A New Introduction to Modal Logic. Рутледж. ISBN 978-1-134-80028-5.
Mac Lane, Saunders ; Moerdijk, Ieke (2012) [1991]. Sheaves in Geometry and Logic: A First Introduction to Topos Theory. Springer. ISBN 978-1-4612-0927-0.
van Dalen, Dirk (2013) [1986]. "Intuitionistic Logic". In Gabbay, Dov M.; Guenthner, Franz (eds.). Alternatives to Classical Logic. Handbook of Philosophical Logic. 3. Springer. pp. 225–339. ISBN 978-94-009-5203-4.

External links

Wikimedia Commons has media related to Kripke models.

Garson, James. "Modal Logic". The Stanford Encyclopedia of Philosophy.
Moschovakis, Joan (2018). "Intuitionistic Logic". Стэнфордская энциклопедия философии. Metaphysics Research Lab, Stanford University.
Detlovs, V.; Podnieks, K. "4.4 Constructive Propositional Logic — Kripke Semantics". Introduction to Mathematical Logic. University of Latvia.N.B: Constructive = intuitionistic.
Burgess, John P. "Kripke Models". Archived from the original on 2004-10-20.
, Encyclopedia of Mathematics, EMS Press, 2001 [1994]