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

S5 — одна из пяти систем модальной логики, предложенных Льюисом и Лэнгфордом в книге «Символическая логика» (англ. Symbolic Logic, 1932). Является нормальной модальной логикой и одной из старейших систем модальной логики. Будучи простейшей модельной логикой, образуется формулами логики высказываний, тавтологиями, аппаратом вывода с подстановками и modus ponens. Синтаксис при этом дополнен модальным оператором необходимости $\Box$ и двойственным ему оператором возможности $\Diamond$.

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

Аксиомы S5

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

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

K: $\Box (A\to B)\to (\Box A\to \Box B)$

T: $\Box A\to A$,

и либо

5: $\Diamond A\to \Box \Diamond A$,

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

4: $\Box A\to \Box \Box A$

B: $A\to \Box \Diamond A$.

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

См. также

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

Ссылки

• Некоторые замечания по S5
• Модальная логика в Стэнфордской энциклопедии философии