直観主義論理は可能世界モデルに対して完全性定理が成り立つから
世界番号付きのタブロー法とかで証明可能か簡単に分かるよ。