Семантика Крипке - Kripke semantics

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

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

Язык пропозициональной модальной логики состоит из счетного множества из пропозициональных переменных , набора истинности функциональных связок (в этой статье , и ), и модального оператор ( «обязательно»). Модальный оператор ( «возможно») является (классическим) двойным из и может быть определен в терминах необходимости , как так: ( «возможно» определяются как эквивалент « не обязательно не»).

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

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

Модель Крипке - это тройка , где - фрейм Крипке, и это отношение между узлами W и модальными формулами, такое, что для всех w  ∈  W и модальных формул A и B :

  • тогда и только тогда ,
  • если и только если или ,
  • если и только если для всех таких то .

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

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

  • модель , если для всех ж  ∈  W ,
  • фрейм , если он действителен для всех возможных вариантов ,
  • класс C кадров или модели, если она действует в каждом члене С .

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

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

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

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

Для любого класса 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, используя определение . T соответствует классу рефлексивных фреймов Крипке.       

Часто гораздо проще охарактеризовать соответствующий класс L, чем доказать его полноту, поэтому соответствие служит руководством для доказательства полноты. Переписка также используется , чтобы показать неполноту модальных логик: предположит , что L 1  ⊆  L 2 являются нормальными модальными логиками , которые соответствуют одному и тому же классу кадров, но и L - не доказывающие всем теоремы L 2 . Тогда L 1 неполна по Крипке. Например, схема генерирует неполную логику, поскольку она соответствует тому же классу фреймов, что и GL (а именно, транзитивные и обратные хорошо обоснованные фреймы), но не доказывает GL -таутологию .

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

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

Имя Аксиома Состояние рамы
K N / A
Т рефлексивный :
4 переходный :
плотный :
D или серийный номер :
B симметричный  :
5 Евклидово :
GL R транзитивный, R −1 обоснованный
Grz R рефлексивно и транзитивно, R −1 - Id хорошо обосновано
ЧАС
M (сложное свойство второго порядка )
грамм сходящийся:
дискретный:
частичная функция :
функция:
или пустой:

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

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

Имя Аксиомы Состояние рамы
K - все кадры
Т Т рефлексивный
K4 4 переходный
S4 Т, 4 предзаказ
S5 Т, 5 или Д, Б, 4 отношение эквивалентности
S4.3 Т, 4, Н общий предварительный заказ
S4.1 Т, 4, М предзаказ,
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 и заключаются в следующем:

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

Каноническая модель представляет собой модель 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 . Определение отношения удовлетворения модифицируется следующим образом:

если и только если

Упрощенная семантика, открытая Тимом Карлсоном, часто используется для полимодальных логик доказуемости . Модель Карлсона - это структура с одним отношением доступности R и подмножествами D i  ⊆  W для каждой модальности. Удовлетворение определяется как

если и только если

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

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

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

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

  • если p - пропозициональная переменная, и , то ( условие постоянства (см. монотонность )),
  • если и только если и ,
  • если и только если или ,
  • тогда и только тогда, когда для всех , подразумевает ,
  • нет .

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

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

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

Пусть L - язык первого порядка . Модель Крипке L - это тройка , где - интуиционистский фрейм Крипке, 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 , мы определяем отношение удовлетворения :

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

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

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

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

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

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

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

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

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

P-морфизм моделей Крипке и p-морфизм лежащих в их основе фреймов , удовлетворяющий

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

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

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

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

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

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

Мы можем превратить модель Крипке в дерево, используя распутывание . Для данной модели и фиксированного узла w 0  ∈  W мы определяем модель , где W ' - это множество всех конечных последовательностей таких, что w i  R w i + 1 для всех i  <  n , и тогда и только тогда, когда для пропозиционального переменная p . Определение отношения доступности R ' варьируется; в простейшем случае положим

,

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

Фильтрация - это полезная конструкция, которая используется для доказательства FMP для многих логик. Пусть X - множество формул, замкнутое относительно взятия подформул. Х -фильтрация модели является отображением F из W в модели таким образом, что

  • f - сюръекция ,
  • f сохраняет отношение доступности и (в обоих направлениях) удовлетворение переменных p  ∈  X ,
  • если f ( uR '  f ( v ) и , где , то .

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

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

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

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

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

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

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

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

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

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

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

Примечания

a ^ По Анджею Гжегорчику .
  1. ^ Шохам, Йоав; Лейтон-Браун, Кевин (2008). Мультиагентные системы: алгоритмические, теоретико-игровые и логические основы . Издательство Кембриджского университета. п. 397. ISBN. 978-0521899437.
  2. ^ Гаске, Оливье; и другие. (2013). Миры Крипке: Введение в модальную логику через таблицы . Springer. С. 14–16. ISBN 978-3764385033. Проверено 24 декабря 2014 .
  3. ^ Обратите внимание, что понятие «модель» в семантике Крипке модальной логики отличается от понятия «модель» в классической немодальной логике: в классической логике мы говорим, что некоторая формула F имеет «модель», если она существует. интерпретация переменных F, которая делает формулу F истинной; эта интерпретация конкретных затем модель с формулой F . В семантике модальной логики Крипке, напротив, «модель» - это не конкретное «нечто», которое делает конкретную модальную формулу истинной; в семантике Крипке «модель», скорее, следует понимать как более широкую вселенную дискурса, в рамках которой любые модальные формулы могут быть осмысленно «поняты». Таким образом: в то время как понятие «имеет модель» в классической немодальной логике относится к некоторой отдельной формуле внутри этой логики, понятие «имеет модель» в модальной логике относится к самой логике в целом (т.е. система его аксиом и правил дедукции).
  4. ^ Giaquinto, Marcus (2002). Поиск определенности: философское изложение основ математики: философское изложение основ математики . Издательство Оксфордского университета. п. 256. ISBN 019875244X. Проверено 24 декабря 2014 .
  5. ^ Интуиционистская логика . Автор Джоан Мощовакис . Опубликовано в Стэнфордской энциклопедии философии.
  6. ^ Голдблатт, Роберт (2006). «Семантика Крипке-Джояла для некоммутативной логики в квантах» (PDF) . In Governatori, G .; Hodkinson, I .; Венема Ю. (ред.). Успехи в модальной логике . 6 . Лондон: Публикации колледжа. С. 209–225. ISBN 1904987206.
  7. ^ Stokhof, Мартин (2008). «Архитектура смысла: Витгенштейн Tractatus и формальная семантика» . В Замунере, Эдоардо; Леви, Дэвид К. (ред.). Неизменные аргументы Витгенштейна . Лондон: Рутледж. С. 211–244. ISBN 9781134107070. препринт (см. последние два абзаца в разделе 3 « Квазиисторическая интерлюдия: дорога из Вены в Лос-Анджелес» .)

использованная литература

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