I study

私の研究分野は数理論理学です。なかでも、現在ではハイブリッド論理を主な研究対象としています。

Hybrid Logic

ハイブリッド論理 (hybrid logic) は、様相論理を拡張した論理です。ハイブリッド論理では、通常の命題変数に加えて、「可能世界のうちただ一点で成り立つ」という特殊な命題変数を導入します（これを nominal と呼びます）。この特殊な命題変数とそれに伴う種々の論理記号を導入することによって、次のような利点が得られます。

• 「可能世界のうちただ一点で成り立つ命題」は、現実世界におけるさまざまな概念に対応します。 たとえば、時間概念における「瞬間」、あるいは人間関係における「個人」を、nominal で表すことができます。 実際に、ハイブリッド論理を用いて友人関係のモデルを与える研究もあります (Seligman et al., 2011)。
• クリプキモデルの性質をより豊かに表現できます。 たとえばモデルにおける非反射性（すべての可能世界は、自分自身に到達関係がつかない）は、様相論理の論理式では定義できず、ハイブリッド論理に拡張してはじめて定義できる性質の例です。 ハイブリッド論理の豊かな定義可能性を生かし、それをグラフ理論を分析する研究もあります (Benevides & Schechter, 2009)。
• 適当な制限を加えれば、ハイブリッド論理においても決定可能性が成り立ちます。 ある論理が決定可能であるとは、「与えられた論理式がその論理の定理かどうかが、有限時間で判定できる」という性質です。 様相論理は決定可能ですから、その意味では様相論理のよい拡張とも言えます。 なお、様相論理やハイブリッド論理よりはるかに強い表現力をもつ一階述語論理は、決定不能であることがわかっています。

ハイブリッド論理についてより詳しく知りたい方は、こちらのページをご覧ください。

Hybrid Logic (Stanford Encyclopedia of Philosophy)

現在の研究

現在は、ハイブリッド論理の証明体系をつくる研究をしています。 ハイブリッド論理においてはタブロー計算という証明体系がよく研究されており、私もその潮流にしたがった研究を行っています。 タブロー計算は、証明可能な命題に証明を、証明不可能な計算には反例モデルを与えられる道具です。 また、アルゴリズムに従った容易な証明技法であるという点でもすぐれています。

あわせて、タブロー計算の研究で得られた知見を活かし、さまざまな非古典論理に対しその証明体系を与える仕事も行っています。 様相論理をはじめ、さまざまな非古典論理について興味があります。

将来的には、言語をはじめとした世界にある様々な構造をロジックの言葉で表現するような研究をしたいです。 ハイブリッド論理は、その道具立てとして非常に有用なものであると考えています。