ГлавнаяS5 — одна из пяти систем модальной логики, предложенных Льюисом и Лэнгфордом в книге «Символическая логика» (англ. Symbolic Logic, 1932). Является нормальной модальной логикой и одной из старейших систем модальной логики. Будучи простейшей модельной логикой, образуется формулами логики высказываний, тавтологиями, аппаратом вывода с подстановками и modus ponens. Синтаксис при этом дополнен модальным оператором необходимости ◻ {displaystyle Box } и двойственным ему оператором возможности ◊ {displaystyle Diamond } .
С точки зрения семантики Крипке S5 относится к моделям, где отношение достижимости является отношением эквивалентности: оно рефлексивно, симметрично и транзитивно.
Аксиомы S5
В приведённых ниже выражениях используются операторы ◻ {displaystyle Box } («необходимость») и ◊ {displaystyle Diamond } («возможность»).
Система S5 определяется следующими аксиомами:
K: ◻ ( A → B ) → ( ◻ A → ◻ B ) {displaystyle Box (A o B) o (Box A o Box B)} T: ◻ A → A {displaystyle Box A o A} ,и либо
5: ◊ A → ◻ ◊ A {displaystyle Diamond A o Box Diamond A} ,либо одновременно
4: ◻ A → ◻ ◻ A {displaystyle Box A o Box Box A} B: A → ◻ ◊ A {displaystyle A o Box Diamond A} .Аксиома (5) требует, чтобы отношение достижимости R {displaystyle R} семантики Крипке было евклидовым, то есть ( w R v ∧ w R u ) ⟹ v R u {displaystyle (wRvland wRu)implies vRu} .