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

Шаблон:Значения S5 — одна из пяти систем модальной логики, предложенных Льюисом и Лэнгфордом в книге «Символическая логика» (Шаблон:Lang-en, 1932). Является нормальной модальной логикой и одной из старейших систем модальной логики. Будучи простейшей модельной логикой, образуется формулами логики высказываний, тавтологиями, аппаратом вывода с подстановками и modus ponens. Синтаксис при этом дополнен модальным оператором необходимости $◻$ и двойственным ему оператором возможности $◊$ ^[1]^[2].

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

Аксиомы S5

В приведённых ниже выражениях используются операторы $◻$ («необходимость») и $◊$ («возможность»).

Система S5 определяется следующими аксиомами:

K:

◻ (A \to B) \to (◻ A \to ◻ B)

T:

◻ A \to A

,

и либо

5:

◊ A \to ◻ ◊ A

,

либо одновременно

4:

◻ A \to ◻ ◻ A

B:

A \to ◻ ◊ A

.

Аксиома (5) требует, чтобы отношение достижимости $R$ семантики Крипке было евклидовым, то есть $(w R v \land w R u) ⟹ v R u$ .

↑ Chellas, B. F. (1980) Modal Logic: An Introduction. Cambridge University Press. Шаблон:Isbn
↑ Hughes, G. E., and Cresswell, M. J. (1996) A New Introduction to Modal Logic. Routledge. Шаблон:Isbn