Главная
Статьи





07.05.2021


07.05.2021


07.05.2021


07.05.2021


07.05.2021





Яндекс.Метрика
         » » S5 (модальная логика)

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

28.02.2021

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} .