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

Formal semantics for non-classical logic systems

Семантика Крипке (также известная как реляционная семантика или семантика фреймов , и ее часто путают с семантикой возможного мира ) ^[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}$

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

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

Аксиому K также можно переписать как , что логически устанавливает 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 и таковы: ${\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 для доказательства полноты логики по Крипке: каждая нормальная модальная логика полна относительно класса модальных алгебр , и конечная модальная алгебра может быть преобразована в фрейм Крипке. Например, Роберт Булл с помощью этого метода доказал, что каждое нормальное расширение 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).}$

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

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

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

Интуиционистская модель Крипке представляет собой тройку , где – предупорядоченный фрейм Крипке, и удовлетворяет следующим условиям: ^[7] ${\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 переменных элементами Mw _, мы определяем отношение удовлетворения : ${\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 . ^[8]

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

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

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

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

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

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

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

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

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

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

Примечания

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

Рекомендации

• Блэкберн, П.; де Рейке, М .; Венема, Иде (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 г.). «Интуиционистская логика». В Залте, Эдвард Н. (ред.). Стэнфордская энциклопедия философии .