Введение

В логике строгий условный (символ: , или ⥽) — это условное высказывание, управляемое модальным оператором, то есть логической связкой модальной логики. Он логически эквивалентен материальному условному высказыванию классической логики, объединенному с оператором необходимости из модальной логики. Для любых двух высказываний p и q, формула p → q утверждает, что p материально влечет q, а ⥽ утверждает, что p строго влечет q. Строгие условные высказывания являются результатом попытки Кларенса Ирвинга Льюиса найти условное высказывание для логики, которое могло бы адекватно выражать индикативные условные высказывания в естественном языке. Они также использовались в исследованиях теологии Молина.

Избегайте парадоксов

Строгие условные высказывания позволяют избежать парадоксов материальной импликации. Например, следующее утверждение некорректно формализуется материальной импликацией: если Билл Гейтс получил медицинское образование, то Элвис никогда не умирал. Это условие должно быть ложным: образование Билла Гейтса никак не связано с тем, жив ли Элвис. Однако прямое кодирование этой формулы в классической логике с использованием материальной импликации приводит к следующему:

Билл Гейтс получил медицинское образование → Элвис никогда не умирал. Эта формула истинна, поскольку всякий раз, когда антецедент A ложен, формула A → B истинна. Следовательно, эта формула не является адекватным переводом исходного предложения. Кодирование с использованием строгой импликации выглядит так:

(Билл Гейтс получил медицинское образование → Элвис никогда не умирал). В модальной логике эта формула означает (приблизительно), что во всех возможных мирах, в которых Билл Гейтс получил медицинское образование, Элвис никогда не умирал. Поскольку легко представить мир, в котором Билл Гейтс – выпускник медицинского факультета, а Элвис мертв, эта формула ложна. Следовательно, эта формула представляется корректным переводом исходного предложения.

Конструктивная логика

В конструктивной обстановке симметрия между ⥽ и нарушается, и эти два связных элемента можно изучать независимо друг от друга. Конструктивная строгая импликация может быть использована для исследования интерпретируемости арифметики Хейтинга и моделирования стрелок и защищённой рекурсии в информатике.