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

Формальная семантика для неклассических логических систем

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

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

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

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

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

Модель Крипке — это тройка , ^[4] где — фрейм Крипке, а — отношение между узлами 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  ∈  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 фреймов или моделей, если он действителен для каждого члена C.

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

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

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

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

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

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

Рассмотрим схему T  : . T действителен в любой рефлексивной рамке : если , то поскольку w R w . С другой стороны, рама, которая подтверждает T, должна быть рефлексивной: зафиксируем w  ∈  W , и определим удовлетворение пропозициональной переменной p следующим образом: если и только если w R u . Тогда , таким образом , через T , что означает w R w с использованием определения . T соответствует классу рефлексивных рамок Крипке. ${\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 (а именно, транзитивным и обратным хорошо обоснованным фреймам), но не доказывает GL -тавтологию . ${\displaystyle \Box (A\leftrightarrow \Box A)\to \Box A}$ ${\displaystyle \Box A\to \Box \Box A}$

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

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

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

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

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

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

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

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

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

Канонической моделью L является модель Крипке , где W — множество всех L - MCS , а отношения R и 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).}$

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

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

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

Интуиционистская модель Крипке представляет собой тройку , где — предупорядоченный фрейм Крипке, и удовлетворяет следующим условиям: ^[8] ${\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 таких, что w ≤ u , не u ⊩ A , то w ⊩ A → ⊥ является бессмысленно истинным , поэтому w ⊩ ¬ 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 ₁ ,..., an _∈ M _u : если P ( a ₁ ,..., _an ) выполняется в 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 . ^[9]

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

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

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

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

Естественные гомоморфизмы в семантике Крипке называются 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 — множество формул, замкнутое относительно взятия подформул. 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}$

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

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

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

Приложения компьютерных наук

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

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

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

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

Смотрите также

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

Примечания

1. Семантика возможных миров — более широкий термин, охватывающий различные подходы, включая семантику Крипке. Обычно он относится к идее анализа модальных утверждений путем рассмотрения альтернативных возможных миров, где различные предложения являются истинными или ложными. Хотя семантика Крипке — это особый тип семантики возможных миров, существуют и другие способы моделирования возможных миров и их отношений. Семантика Крипке — это особая форма семантики возможных миров, которая использует реляционные структуры для представления отношений между возможными мирами и предложениями в модальной логике. ^{[ необходима ссылка ]}
2. Шохам и Лейтон-Браун 2008.
3. Гаске и др. 2013, стр. 14–16.
4. Обратите внимание, что понятие «модель» в семантике модальной логики Крипке отличается от понятия «модель» в классической немодальной логике: в классической логике мы говорим, что некоторая формула F имеет «модель», если существует некоторая «интерпретация» переменных F , которая делает формулу F истинной; эта конкретная интерпретация тогда является моделью формулы F. В семантике модальной логики Крипке, напротив, «модель» не является конкретным «чем-то», что делает конкретную модальную формулу истинной; в семантике Крипке «модель» скорее следует понимать как более обширную вселенную дискурса , в рамках которой любые модальные формулы могут быть осмысленно «поняты». Таким образом: в то время как понятие «имеет модель» в классической немодальной логике относится к некоторой индивидуальной формуле внутри этой логики, понятие «имеет модель» в модальной логике относится к самой логике в целом (т. е. ко всей системе ее аксиом и правил вывода).
5. Джаквинто 2002.
6. По Анджею Гжегорчику .
7. Булос, Джордж (1993). Логика доказуемости . Cambridge University Press. стр. 148, 149. ISBN 0-521-43342-8.
8. Симпсон 1994, стр. 20, 2.2 Семантика интуиционистской логики.
9. См. немного иную формализацию в Moschovakis (2022)
10. Голдблатт 2006b.
11. Stokhof 2008, см. последние два абзаца в разделе 3 Квазиисторическая интерлюдия: дорога из Вены в Лос-Анджелес ..

Ссылки

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

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

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