За пределами «истинно» и «ложно»
Классическая логика знает два значения: истина и ложь. Утверждение «2 + 2 = 4» истинно, «2 + 2 = 5» ложно. Но язык богаче: «2 + 2 необходимо равно 4», «возможно, завтра пойдёт дождь», «Иван должен вернуть долг». Слова «необходимо», «возможно», «должен» — модальности, и классическая логика их не охватывает.
Модальная логика добавляет два оператора: □ (необходимо) и ◇ (возможно). □p означает «p истинно во всех возможных ситуациях». ◇p — «p истинно хотя бы в одной». Эти операторы связаны: □p ≡ ¬◇¬p (если p необходимо, то невозможно не-p).
Аристотель и Средневековье
Аристотель в «Об истолковании» (IV век до н.э.) первым обсуждал модальные высказывания: «Завтра будет морское сражение» — истинно ли это утверждение сегодня? Если да — будущее предопределено. Если нет — как оно может стать истинным завтра? Средневековые логики (Абеляр, Оккам, Дунс Скот) развивали модальные рассуждения, но без формального аппарата.
Кларенс Ирвинг Льюис в 1918 году предложил первую формальную систему модальной логики (S1–S5), неудовлетворённый тем, что в классической логике из ложного следует что угодно (ex falso quodlibet).
Семантика Крипке
Прорыв совершил Сол Крипке в 1959 году — в 18 лет. Он предложил семантику возможных миров: модальные формулы оцениваются не в одном мире, а в множестве «возможных миров», связанных отношением достижимости. □p истинно в мире w, если p истинно во всех мирах, достижимых из w. ◇p — если p истинно хотя бы в одном.
Разные свойства отношения достижимости дают разные системы: если отношение рефлексивно — система T, транзитивно — система K4, рефлексивно и транзитивно — S4, рефлексивно, транзитивно и симметрично — S5. Каждая система подходит для разных задач.
Виды модальных логик
Алетическая — необходимость и возможность в метафизическом смысле. «Необходимо, что вода = H₂O» (истинно во всех возможных мирах). «Возможно, что Наполеон выиграл при Ватерлоо» (существует мир, где это так).
Деонтическая — обязательность, разрешённость, запрещённость. «Обязательно платить налоги» (O), «разрешено курить на улице» (P). Применяется в юридическом ИИ и нормативных системах.
Эпистемическая — знание и убеждение. «Агент A знает, что p» (Ka p). Используется в теории игр, криптографии (знание участников протокола), мультиагентных системах.
Темпоральная — время. «Всегда будет p» (G p), «когда-нибудь будет p» (F p), «p до тех пор, пока q» (p U q). Артур Прайор (1957) — основатель. Главное применение — верификация программ и протоколов.
Применение в информатике
Темпоральная логика — основа model checking (проверки моделей). Эдмунд Кларк, Аллен Эмерсон и Жозеф Сифакис получили за это премию Тьюринга в 2007 году. Программист записывает свойство: «светофор никогда не покажет зелёный обоим направлениям одновременно» (□¬(green_NS ∧ green_EW)). Алгоритм автоматически проверяет, выполняется ли свойство для всех возможных состояний системы.
Intel использует model checking для верификации процессоров. NASA проверяла бортовое ПО марсоходов. Amazon — корректность распределённых протоколов AWS. Без модальной логики формальная верификация программ была бы невозможна.