WikiDer > Семантика Крипке - Википедия
Эта статья включает в себя список общих Рекомендации, но он остается в основном непроверенным, потому что ему не хватает соответствующих встроенные цитаты. (апрель 2013) (Узнайте, как и когда удалить этот шаблон сообщения) |
Семантика Крипке (также известен как реляционная семантика или же семантика кадра, и часто путают с возможная мировая семантика) является формальным семантика за неклассическая логика системы, созданные в конце 1950-х - начале 1960-х годов Саул Крипке и Андре Жоял. Впервые он был задуман для модальная логика, а позже адаптирован к интуиционистская логика и другие неклассические системы. Развитие семантики Крипке было прорывом в теории неклассических логик, поскольку теория моделей такой логики почти не существовало до Крипке (алгебраическая семантика существовала, но считалась «замаскированным синтаксисом»).
Семантика модальной логики
Язык модальной логики высказываний состоит из счетно бесконечное множество из пропозициональные переменные, набор истинностно-функциональных связки (в этой статье и ), а модальный оператор ("обязательно"). Модальный оператор ("возможно") является (классически) двойной из и можно определить с точки зрения необходимости так: («возможно, А» определяется как эквивалент «не обязательно не А»).[1]
Основные определения
А Рамка Крипке или же модальная рамка пара , куда W является (возможно, пустым) множеством, и р это бинарное отношение на W. Элементы W называются узлы или же миры, и р известен как отношение доступности.[2]
А Модель Крипке это тройка , куда - фрейм Крипке, а это отношение между узлами W и модальные формулы, такие, что для всех ш ∈ W и модальные формулы A и B:
- если и только если ,
- если и только если или же ,
- если и только если для всех такой, что .
Мы читаем в качестве "ш удовлетворяетА”, “А удовлетворен в ш", или же"ш силы А». Соотношение называетсяотношение удовлетворения, оценка, или же принуждение связьОтношение удовлетворения однозначно определяется своим значением в пропозициональных переменных.
Формула А является действительный в:
- модель , если для всех ш ∈ W,
- рама , если он действителен в для всех возможных вариантов ,
- класс C фреймов или моделей, если это действительно в каждом члене C.
Определим Thm (C) как набор всех формул, которые верны вC. Наоборот, если Икс - набор формул, пусть Mod (Икс) быть классом всех фреймов, которые проверяют каждую формулу из Икс.
Модальная логика (т.е. набор формул) L является звук по классу кадров C, если L ⊆ Thm (C). L являетсяполный wrt C если L ⊇ Thm (C).
Соответствие и полнота
Семантика полезна для исследования логики (т.е. система вывода) только если семантическое следствие отношение отражает его синтаксический аналог, синтаксическое следствие отношение (выводимость).[3] Жизненно важно знать, какая модальная логика является правильной и полной по отношению к классу фреймов Крипке, а также определить, к какому классу это относится.
Для любого класса C рам Крипке, Thm (C) это нормальная модальная логика (в частности, теоремы минимальной нормальной модальной логики, K, действительны в каждой модели Крипке). Однако в общем случае обратное неверно: хотя большинство изучаемых модальных систем полны классов фреймов, описываемых простыми условиями, неполные нормальные модальные логики Крипке действительно существуют. Естественным примером такой системы является Полимодальная логика Джапаридзе.
Нормальная модальная логика L соответствует к классу рам C, если C = Мод (L). Другими словами, C - самый большой класс фреймов такой, что L звучит по C. Следует, что L полна по Крипке тогда и только тогда, когда она полна своего соответствующего класса.
Рассмотрим схему Т : .Т действует в любом рефлексивный Рамка : если, тогда поскольку ш р ш. С другой стороны, кадр, который проверяет Т должно быть рефлексивным: исправить ш ∈ W, и определить удовлетворение пропозициональной переменной п следующее: если и только если ш р ты. потом, таким образом к Т, что значит ш р ш используя определение. Т соответствует классу рефлексивных рам Крипке.
Часто бывает проще охарактеризовать соответствующий классL чем для доказательства ее полноты, таким образом, соответствие служит проводником для доказательства полноты. Переписка также используется, чтобы показатьнезавершенность модальных логик: предположим L1 ⊆ L2 нормальные модальные логики, которые соответствуют тому же классу фреймов, но L1 не доказывает все теоремы L2. потом L1 Крипке неполный. Например, схема порождает неполную логику, поскольку соответствует тому же классу кадров, что и GL (а именно, транзитивные и обратные хорошо обоснованные фреймы), но не доказывает GL-таутология .
Общие модальные схемы аксиом
В следующей таблице перечислены общие модальные аксиомы вместе с соответствующими классами. Названия аксиом часто меняются.
Имя | Аксиома | Состояние рамы |
---|---|---|
K | Нет данных | |
Т | рефлексивный: | |
4 | переходный: | |
плотный: | ||
D | или же | серийный: |
B | симметричный : | |
5 | Евклидово: | |
GL | р переходный, р−1 обоснованный | |
Grzа | р рефлексивный и переходный, р−1−Идентификатор обоснованный | |
ЧАС | ||
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, и Modus Ponens. А максимальное L-согласованное множество (ан L-MCSдля краткости) является L-согласованный набор, не имеющий собственно L-согласованный надмножество.
В каноническая модель из L модель Крипке, куда W это набор всех L-MCS, а отношения р и являются следующими:
- тогда и только тогда, когда для каждой формулы , если тогда ,
- если и только если .
Каноническая модель - это модель L, как и все L-MCS содержит все теоремы L. К Лемма Цорна, каждый L-согласованный набор содержится в L-MCS, в частности, каждая формула, недоказуемая в L имеет контрпример в канонической модели.
Основное применение канонических моделей - доказательства полноты. Свойства канонической модели K сразу подразумевает полноту K относительно класса всех фреймов Крипке. нет работать на произвольные L, поскольку нет гарантии, что базовый Рамка канонической модели удовлетворяет рамочным условиям L.
Мы говорим, что формула или набор Икс формул каноническийв отношении собственности п фреймов Крипке, если
- Икс действительно в каждом кадре, который удовлетворяет п,
- для любой нормальной модальной логики L который содержит Икс, основной фрейм канонической модели L удовлетворяет п.
Объединение канонических наборов формул само по себе является каноническим. Из предыдущего обсуждения следует, что любая логика, аксиоматизируемая каноническим набором формул, является полной по Крипке, икомпактный.
Аксиомы 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, и Kripkecomplete.
Мультимодальная логика
Семантика Крипке имеет прямое обобщение на логики с более чем одной модальностью. Рамка Крипке для языка с поскольку множество операторов его необходимости состоит из непустого множества W оснащенный бинарными отношениямиря для каждого я ∈ я. Определение отношения удовлетворенности изменяется следующим образом:
- если и только если
Упрощенная семантика, открытая Тимом Карлсоном, часто используется для полимодальных логика доказуемости. А Карлсон модель это структурас одним отношением доступности р, и подмножестваDя ⊆ W для каждой модальности. Удовлетворение определяется как
- если и только если
Модели Карлсона легче визуализировать и работать с ними, чем с обычными полимодальными моделями Крипке; есть, однако, полные полимодаллогики Крипке, которые неполны по Карлсону.
Семантика интуиционистской логики
Семантика Крипке для интуиционистская логика следует тем же принципам, что и семантика модальной логики, но использует другое определение удовлетворения.
An интуиционистская модель Крипке это тройка, куда это Предзаказанный Рама Крипке и удовлетворяет следующим условиям:
- если п пропозициональная переменная, , и , тогда (настойчивость состояние (ср. монотонность)),
- если и только если и ,
- если и только если или же ,
- если и только если для всех , подразумевает ,
- нет .
Отрицание А, ¬А, можно определить как аббревиатуру для А → ⊥. Если для всех ты такой, что ш ≤ ты, нет ты ⊩ А, тогда ш ⊩ А → ⊥ это пусто правда, так ш ⊩ ¬А.
Интуиционистская логика верна и полна по отношению к своей крипкесемантике, и в ней есть конечное свойство модели.
Интуиционистская логика первого порядка
Позволять L быть первый заказ язык. Крипкемодель L это тройка, куда - интуиционистский фрейм Крипке, Mш это (классический) L-структура для каждого узла ш ∈ W, и следующие условия совместимости выполняются всякий раз, когда ты ≤ v:
- область Mты входит в домен Mv,
- реализации функциональных символов в Mты и Mv согласовать элементы Mты,
- для каждого п-арный предикат п и элементы а1,...,ап ∈ Mты: если п(а1,...,ап) держится в Mты, то держится Mv.
Учитывая оценку е переменных по элементам Mш, мы определяем отношение удовлетворения :
- если и только если держит в Mш,
- если и только если и ,
- если и только если или же ,
- если и только если для всех , подразумевает ,
- нет ,
- тогда и только тогда, когда существует такой, что ,
- если и только если для каждого и каждый , .
Здесь е(Икс→а) - оценка, которая дает Икс Значение а, и в остальном соглашается с е.
Смотрите немного другую формализацию в.[4]
Семантика Крипке – Джояла
В рамках самостоятельной разработки теория связок, примерно в 1965 году стало ясно, что семантика Крипке тесно связана с обработкой экзистенциальная количественная оценка в теория топоса.[5] То есть «локальный» аспект существования участков пучка был своего рода логикой «возможного». Хотя эта разработка была работой нескольких людей, имя Семантика Крипке – Джояла часто используется в этой связи.
Модельные конструкции
Как в классическом теория моделей, существуют методы построения новой модели Крипке из других моделей.
Естественный гомоморфизмы в семантике Крипке называютсяp-морфизмы (сокращенно от псевдоэпиморфизм, но последний термин используется редко). P-морфизм фреймов Крипке и это отображение такой, что
- ж сохраняет отношение доступности, т.е. u R v подразумевает ж(ты) Р' ж(v),
- в любое время ж(ты) Р' v', Существует v ∈ W такой, что u R v и ж(v) = v’.
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-морфизмы) моделей сохраняют удовлетворение все формулы, а не только пропозициональные переменные.
Мы можем преобразовать модель Крипке в дерево с помощьюраспутывание. Учитывая модель и фиксированный узел ш0 ∈ W, мы определяем модель, куда W ’ это совокупность всех конечных последовательностей такой, что шя R wя + 1 для всехя < п, и если и только если для пропозициональной переменнойп. Определение отношения доступности Р'варьируется; в простейшем случае положим
- ,
но многие приложения нуждаются в рефлексивном и / или транзитивном замыкании этого отношения или подобных модификациях.
Фильтрация полезная конструкция, которая используется для доказательства FMP по многим логикам. Позволять Икс - множество формул, замкнутое относительно взятия подформул. An Икс-фильтрация модели это отображение ж из W к модели такой, что
- ж это сюрприз,
- ж сохраняет отношение доступности и (в обоих направлениях) удовлетворение переменных п ∈ Икс,
- если ж(ты) Р' ж(v) и , куда , тогда .
Следует, что ж сохраняет выполнение всех формул изИкс. В типичных приложениях мы берем ж как проекция на частное из W по отношению
- ты ≡Икс v если и только если для всех А ∈ Икс, если и только если .
Как и в случае распутывания, определение отношения доступности к коэффициенту варьируется.
Общая семантика фрейма
Основным недостатком семантики Крипке является существование неполных логик Крипке и логик, которые являются полными, но не компактными. Это можно исправить, оснастив фреймы Крипке дополнительной структурой, которая ограничивает набор возможных оценок, используя идеи из алгебраической семантики. Это приводит к общая рамка семантика.
Приложения для информатики
Blackburn et al. (2001) отмечают, что, поскольку реляционная структура - это просто набор вместе с набором отношений в этом наборе, неудивительно, что реляционные структуры можно найти практически везде. В качестве примера из теоретическая информатика, они дают маркированные переходные системы, какая модель выполнение программы. Blackburn et al. таким образом утверждают, что из-за этой связи модальные языки идеально подходят для обеспечения «внутренней, локальной перспективы на реляционные структуры». (стр. xii)
История и терминология
Эта секция не цитировать любой источники. (Октябрь 2009 г.) (Узнайте, как и когда удалить этот шаблон сообщения) |
Похожая работа, предшествовавшая революционным семантическим прорывам Крипке:[6]
- Рудольф Карнап кажется, был первым, кто придумал, что можно возможная мировая семантика для модальностей необходимости и возможности посредством предоставления функции оценки параметра, который охватывает возможные миры Лейбница. Баярт развивает эту идею дальше, но не дает рекурсивных определений удовлетворения в стиле, введенном Тарским;
- J.C.C. McKinsey и Альфред Тарский разработал подход к моделированию модальных логик, который до сих пор играет важную роль в современных исследованиях, а именно алгебраический подход, в котором булевы алгебры с операторами используются в качестве моделей. Бьярни Йонссон и Тарский установили представимость булевых алгебр с операторами в терминах шкал. Если бы эти две идеи были объединены, результатом были бы именно каркасные модели, то есть модели Крипке, созданные за много лет до Крипке. Но тогда никто (даже Тарский) не видел связи.
- Артур Прайор, опираясь на неопубликованные работы К. А. Мередит, разработал перевод сентенциальной модальной логики в классическую логику предикатов, которая, если бы он объединила ее с обычной теорией моделей для последней, произвела бы теорию моделей, эквивалентную моделям Крипке для первой. Но его подход был решительно синтаксическим и анти-модельным.
- Стиг Кангер дал более сложный подход к интерпретации модальной логики, но тот, который содержит многие ключевые идеи подхода Крипке. Он первым отметил взаимосвязь между условиями отношений доступности и Льюисаксиомы стиля модальной логики. Кангер, однако, не смог предоставить доказательство полноты своей системы;
- Яакко Хинтикка дал семантику в своих статьях, вводя эпистемологическую логику, которая является простой вариацией семантики Крипке, эквивалентной характеристике оценок с помощью максимальных согласованных множеств. Он не дает правил вывода для эпистемической логики и поэтому не может предоставить доказательства полноты;
- Ричард Монтегю у него было много ключевых идей, содержащихся в работе Крипке, но он не считал их значительными, потому что у него не было доказательства полноты, и поэтому он не публиковал его до тех пор, пока статьи Крипке не произвели сенсацию в сообществе логиков;
- Эверт Виллем Бет представила семантику интуиционистской логики, основанную на деревьях, которая очень похожа на семантику Крипке, за исключением использования более громоздкого определения удовлетворения.
Смотрите также
Примечания
- а^ После Анджей Гжегорчик.
- ^ Шохам, Йоав; Лейтон-Браун, Кевин (2008). Мультиагентные системы: алгоритмические, теоретико-игровые и логические основы. Издательство Кембриджского университета. п. 397. ISBN 978-0521899437.
- ^ Гаске, Оливье; и другие. (2013). Миры Крипке: введение в модальную логику через таблицы. Springer. С. 14–16. ISBN 978-3764385033. Получено 24 декабря 2014.
- ^ Джакинто, Маркус (2002). Поиски определенности: философское изложение основ математики: философское изложение основ математики. Издательство Оксфордского университета. п. 256. ISBN 019875244X. Получено 24 декабря 2014.
- ^ Интуиционистская логика. Написано Джоан Мощовакис. Опубликовано в Стэнфордской энциклопедии философии.
- ^ Голдблатт, Роберт (2006). "Семантика Крипке-Джояла для некоммутативной логики в квантах" (PDF). In Governatori, G .; Hodkinson, I .; Венема Ю. (ред.). Достижения в модальной логике. 6. Лондон: публикации колледжа. С. 209–225. ISBN 1904987206.
- ^ Стохоф, Мартин (2008). "Архитектура смысла: Витгенштейновская Tractatus и формальная семантика ". В Замунере, Эдоардо; Леви, Дэвид К. (ред.). Неизменные аргументы Витгенштейна. Лондон: Рутледж. С. 211–244. ISBN 9781134107070. препринт (См. Последние два абзаца в разделе 3 Квазиисторическая интерлюдия: дорога из Вены в Лос-Анджелес.)
Рекомендации
- Blackburn, P .; де Рийке, М.; Венема, Иде (2002). Модальная логика. Издательство Кембриджского университета. ISBN 978-1-316-10195-7.
- Бык, Роберт А .; Сегерберг, К. (2012) [1984]. «Базовая модальная логика». In Gabbay, D.M .; Guenthner, F. (ред.). Расширения классической логики. Справочник по философской логике. 2. Springer. С. 1–88. ISBN 978-94-009-6259-0.
- Чагров, А .; Захарящев, М. (1997). Модальная логика. Кларендон Пресс. ISBN 978-0-19-853779-3.
- Даммит, Майкл А. Э. (2000). Элементы интуиционизма (2-е изд.). Кларендон Пресс. ISBN 978-0-19-850524-2.
- Фиттинг, Мелвин (1969). Интуиционистская логика, теория моделей и принуждение. Северная Голландия. ISBN 978-0-444-53418-7.
- Голдблатт, Роберт (2006). «Математическая модальная логика: взгляд на ее эволюцию» (PDF). В Габбае, Дов М .; Вудс, Джон (ред.). Логика и модальности в двадцатом веке (PDF). Справочник по истории логики. 7. Эльзевир. С. 1–98. ISBN 978-0-08-046303-2.
- Cresswell, M.J .; Хьюз, Г. (2012) [1996]. Новое введение в модальную логику. Рутледж. ISBN 978-1-134-80028-5.
- Мак-Лейн, Сондерс; Мурдейк, Ике (2012) [1991]. Пучки в геометрии и логике: первое введение в теорию топоса. Springer. ISBN 978-1-4612-0927-0.
- ван Дален, Дирк (2013) [1986]. «Интуиционистская логика». В Габбае, Дов М .; Гентнер, Франц (ред.). Альтернативы классической логике. Справочник по философской логике. 3. Springer. С. 225–339. ISBN 978-94-009-5203-4.
внешняя ссылка
Викискладе есть медиафайлы по теме Крипке модели. |
- Гарсон, Джеймс. «Модальная логика». Стэнфордская энциклопедия философии.
- Мощовакис, Джоан (2018). «Интуиционистская логика». Стэнфордская энциклопедия философии. Лаборатория метафизических исследований Стэнфордского университета.
- Детловс, В .; Подниекс, К. «4.4 Конструктивная логика высказываний - семантика Крипке». Введение в математическую логику. Латвийский университет. Примечание: конструктивное = интуиционистское.
- Берджесс, Джон П. «Модели Крипке». Архивировано из оригинал на 2004-10-20.
- «Крипке модели», Энциклопедия математики, EMS Press, 2001 [1994]