S5 (модальная логика)

В логике и философии, S5является одной из пяти систем модальная логика, предложенная Кларенсом Ирвингом Льюисом и Купером Гарольдом Лэнгфордом в их книге «Символическая логика» 1932 года. Это нормальная модальная логика и одна из старейших систем модальной логики любого рода. Он сформирован с помощью формул исчисления высказываний, и тавтологий, и аппарата вывода с подстановкой и modus ponens, но расширением синтаксиса модальным оператор обязательно $◻\; \{\backslash \; displaystyle\; \backslash \; Box\}$и его двойственный возможный $◊\; \{\backslash \; displaystyle\; \backslash \; Diamond\}$.

• 1 Аксиомы S5
• 2 Семантика Крипке
• 3 Приложения
• 4 См. Также
• 5 Ссылки
• 6 Внешние ссылки

В следующем примере используются модальные операторы $◻\; \{\backslash \; displaystyle\; \backslash \; Box\}$(«обязательно») и $◊\; \{\backslash \; displaystyle\; \backslash \; Diamond\}$(«возможно»).

S5характеризуется аксиомами:

• K: $◻\; (A\; \to \; B)\; \to \; (◻\; A\; \to \; ◻\; B)\; \{\backslash \; displaystyle\; \backslash \; Box\; (A\; \backslash \; to\; B)\; \backslash \; to\; (\backslash \; Box\; A\; \backslash \; to\; \backslash \; Box\; B)\}$;
• T: $◻\; A\; \to \; A\; \{\backslash \; displaystyle\; \backslash \; Box\; A\; \backslash \; to\; A\}$,

и либо:

• 5: $◊\; A\; \to \; ◻\; ◊\; A\; \{\backslash \; displaystyle\; \backslash \; Diamond\; A\; \backslash \; to\; \backslash \; Box\; \backslash \; Diamond\; A\}$;
• или оба из следующих:

• 4: $◻\; A\; \to \; ◻\; ◻\; A\; \{\backslash \; displaystyle\; \backslash \; Box\; A\; \backslash \; to\; \backslash \; Box\; \backslash \; Box\; A\}$и
• B: $A\; \to \; ◻\; ◊\; A\; \{\backslash \; displaystyle\; A\; \backslash \; to\; \backslash \; Box\; \backslash \; Diamond\; A\}$.

Аксиома (5) ограничивает отношение доступности $R\; \{\backslash \; displaystyle\; R\}$рамки Крипке до быть евклидовым, т.е. $(w\; R\; v\; \wedge \; w\; R\; u)\; ⟹\; v\; R\; u\; \{\backslash \; displaystyle\; (wRv\; \backslash \; land\; wRu)\; \backslash \; подразумевает\; vRu\}$.

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

Определение выполнимости формулы S5 - это NP-полная проблема. Доказательство твердости тривиально, поскольку S5 включает в себя логику высказываний. Принадлежность доказывается, показывая, что любая выполнимая формула имеет модель Крипке, в которой количество миров максимально линейно по размеру формулы.

S5полезны, поскольку позволяют избежать лишних итераций квалификаторов разных типов. Например, в S5, если X обязательно, возможно, обязательно,, возможно, истинно, то X, возможно, истинно. Квалификаторы, не выделенные жирным шрифтом перед финальным словом «возможно», удаляются в S5 . Хотя это полезно для того, чтобы предложения были достаточно краткими, это также может показаться нелогичным в том смысле, что в рамках S5, если что-то возможно необходимо, то это необходимо.

Элвин Плантинга утверждал, что эта особенность S5 на самом деле не противоречит интуиции. Чтобы оправдать это, он аргументирует, что если X, возможно, необходим, то он необходим по крайней мере в одном возможном мире ; следовательно, это необходимо во всех возможных мирах и, следовательно, верно во всех возможных мирах. Такие рассуждения лежат в основе «модальных» формулировок онтологического аргумента .

• Модальная логика
• Нормальная модальная логика
• семантика Крипке

• http://home.utah.edu/~nahaj/logic/structures/systems/s5.html
• Modal Logic в Стэнфордской энциклопедии философии