2019年6月10日のコメントペーパーより。レジュメは様相命題論理。
コメント：[古典] 命題論理と述語論理はタブローで計算できることを知っているのですが、様相命題論理や様相述語論理はタブローでできますか？
回答：できます。いつものように
を見てもらえればよいかと思います。
ちなみに細かいことですが「計算できる」あるいは「できる」というのは微妙な表現ですね。以前に
で書いたように、古典述語論理は「決定不可能 (妥当性の判定問題は計算不能)」なので、どのような推論に対してもタブローによる手続きで有限ステップ内で答えが出せるわけではありません (様相述語論理は古典述語論理を部分として含むので、当然決定不可能です)。
それでも「古典述語論理のタブロー」というものは存在していて、その意味で、タブローで「できる」と言うことはできます。では、決定可能性が成り立たない場合に、それにもかかわらず、「〇〇論理のタブロー」が存在するとは、あるいは「〇〇論理はタブローでできる」とはどういうことかというと、次の意味での完全性が成り立つことであると言えるでしょう。すなわち、任意の推論 について、
が論理
において妥当である
に対するタブローが
は妥当であると判定する。
決定可能性とこの完全性、ちがいはどこだと思いますか？
