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

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

Аксиомы S5

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

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

• K : ; ${\ Displaystyle \ Box (от A \ до B) \ до (\ Box A \ до \ Box B)}$
• Т : , ${\ displaystyle \ Box A \ to A}$

и либо:

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

• 4 :, и ${\ displaystyle \ Box A \ to \ Box \ Box A}$
• B : . ${\ Displaystyle A \ to \ Box \ Diamond A}$

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

Семантика Крипке

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

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

Приложения

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

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

Смотрите также

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

Рекомендации

внешние ссылки

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