Модальная логика
Модальная логика — формальная логика, использующая модальности, то есть, специализированные смыслы, в которых высказывания могут быть истинными.
Разновидности[править]
- Алетическая — добавляет модальности □ («необходимо, что») и ◊ («возможно, что»). Одна из самых часто используемых модальных логик.
- Темпоральная — класс логик, где модальности связаны со временем («верно всегда», «станет верным», «было верным» и т. д.)
- Эпистемическая — модальность К («известно что»), так же может дополнятся указанием на конкретного знающего субъекта
- Деонтическая — модальности O («обязательно»), P («разрешено») и F («запрещено»).
- Доксастическая — модальность веры («X верит, что»)
- Динамическая — используется в информатике, расширяет □ и ◊ указаниями на конкретные инструкции («после выполнения A обязательно/возможно, что»)
- Логика доказуемости — металогика, позволяющая рассуждать о других логиках с помощью модальности «доказуемо что»
- Проcтранственная — добавляет модальности, связанные с геометрией или топологией
- Стрелочная — добавляет модальности «композиции», «идентичности» и «обращения», позволяя работать с высказываниями как направленными стрелками (например, морфизмами или векторами)
Семантика[править]
С синтаксической точки зрения, модальные логики лишь накладывают различные ограничения на использование переменных. Суть модальностей заключается в их интерпретациях, то есть семантике. Самый распространенный способ интерпретировать модальности — так называемая «семантика возможных миров», также известная как семантика Крипке. Согласно ей, мы рассматриваем истинность высказываний в некоторой совокупности параллельных реальностей (собственно миров), связанных системой достижимостей (т.е. не из каждого мира можно напрямую достичь любого другого).
формула | интерпретация |
---|---|
(базовая формула) A | A истинно в текущем мире |
□A | A истинно во всех мирах |
◊A | A истинно в некотором мире |
Применения[править]
Используется в философии, лингвистике, юриспруденции. Имеет множество применений в информатике:
- Темпоральные логики — базис инструментов проверки моделей. В качестве миров Крипке здесь используется граф состояний программы, что позволяет логически выводить достижимость желательных или нежелательных (т.е. ошибочных или опасных) состояний.
- Субструктурные логики (например, линейная логика) используют модальности для переключения между ограниченным и неограниченным использованием переменных.
- В качестве систем типов могут служить для формализации метапрограммирования, реактивного программирования, распределенных систем, уровней доступа и математических теорий для доказывателей теорем.