|
型付きラムダ計算と圏論の対応を直観主義理論の新しい定式化と捉え、直観主義の含意切片に対する形式化を与えることができた。これは、EilenberやKellyによる射だけの圏の定式化へ新しい可能性を示す。同様な考えに基づき、カリ-・ハワードの対応の古典論理への拡張を調べた。古典論理を特徴付けるパースの論理式に対する計算規則を得た。そこでは、同じ論理式の証明はすべて同等となることが得られ、雑誌Studia Logicaに採録され印刷中である。またこの結果は、ブール代数以外にブール的な圏はないという事実を直積や始対象を用いずに示したものとも考えられ、計算論理と圏論との対応の解明が今後更に必要である。ゲンチェンのシーケント計算LKでの構造についての右側の推論規則の組合せで決まる古典論理の部分構造論理を調べた。その結果、右増と右縮の規則は分離できないことが分かった。さらに、この右増と右縮の両方がある論理では、左の右増と右縮の推論が導けることが分かった。これは、増と縮の推論はシーケントの左右で意味が異なることを表す。従って、左右の構造に関する推論規則をどのように組合せたとしても、得られる論理は古典論理、直観主義論理、BCK論理、適切さの論理あるいは線形論理のいずれかしかないという知見を得た。LKの証明図の構造解析により、LKからパースの推論を使う自然推論への証明図の変換の方式が今後の課題となった。
|
