直観主義命題論理の決定可能性
Modal Companionを用いた決定可能性の証明
次の事実を用いて即座に証明することも出来る
Gödel-McKinsey-Tarskiの定理
より
$ \sf iPL
の証明可能性は
$ \sf S4
の証明可能性と適当な翻訳
$ T
を介して同じである．
$ \vdash_\mathsf{iPL} A \iff \vdash_\mathsf{S4} T(A)
$ \sf S4
は決定可能である．
正規様相論理の決定可能性
など参照