命題・様相・情報概念の論理的構造と哲学的基礎

本研究の目的は、命題概念の哲学的意義を明らかにすることにあるが、命題とは第一義的に推論・論証の対象となるものであるため、特に証明の中でのその振る舞いを正確に分析することが必要となる。具体的には、ゲーデル・マッキンゼイ・タルスキの定理（直観主義論理がある種の翻訳のもとで様相論理S4に埋め込み可能であるという関係）の証明論的証明（証明図の構成という点を重視する方法を用いた証明）を与えることを通じて、各論理体系で扱われる命題がどのような性質を持つのかについての考察を行った。この埋め込み可能性は、直観主義論理以外の非様相論理の諸体系とそれぞれに対応する様相論理の間にも成立することが知られており、この関係を一般に様相同伴(Modal Companion)という。本研究では、こうした様相同伴を幅広く検討した。本年度の研究では、グローバルな形で演算子を扱う一般的なシークエント計算に対し、ローカルな形で代数的な演算子を扱うディスプレイ計算を用いることで、ゲーデル・マッキンゼイ・タルスキの定理の証明論的証明を与えることを試みた。ディスプレイ計算を用いては、まだその証明を与えることはできていないが、G3-styleのシークエント計算の体系を用いて、ゲーデル・マッキンゼイ・タルスキの定理に対する証明論的な別証明を与えることができた（この成果は、北海道大学の佐野勝彦准教授との共同研究の過程で得ることができたものである）。そこで、この結果と関連させることで、ディスプレイ計算を用いる証明を与えることを試み、今後論文の形にまとめるべく考察を行う予定である。また、昨年度より引き続き行っている、佐野勝彦准教授との共同研究の成果については、国際学会での発表を行い、結果をまとめたものが会議録として査読中である。

本研究の目的は、命題概念の哲学的意義を明らかにすることにあるが、命題とは第一義的に推論・論証の対象となるものであるため、特に証明の中でのその振る舞いを正確に分析することが必要となる。具体的には、ゲーデル・マッキンゼイ・タルスキの定理（直観主義論理がある種の翻訳のもとで様相論理S4に埋め込み可能であるという関係）の証明論的証明（証明図の構成という点を重視する方法を用いた証明）を与えることを通じて、各論理体系で扱われる命題がどのような性質を持つのかについての考察を行った。この埋め込み可能性は、直観主義論理以外の非様相論理の諸体系とそれぞれに対応する様相論理の間にも成立することが知られており、この関係を一般に様相同伴(Modal Companion)という。本研究では、こうした様相同伴を幅広く検討した。本年度の研究では、グローバルな形で演算子を扱う一般的なシークエント計算に対し、ローカルな形で代数的な演算子を扱うディスプレイ計算を用いることで、ゲーデル・マッキンゼイ・タルスキの定理の証明論的証明を与えることを試みた。ディスプレイ計算を用いては、まだその証明を与えることはできていないが、G3-styleのシークエント計算の体系を用いて、ゲーデル・マッキンゼイ・タルスキの定理に対する証明論的な別証明を与えることができた（この成果は、北海道大学の佐野勝彦准教授との共同研究の過程で得ることができたものである）。そこで、この結果と関連させることで、ディスプレイ計算を用いる証明を与えることを試み、今後論文の形にまとめるべく考察を行う予定である。また、昨年度より引き続き行っている、佐野勝彦准教授との共同研究の成果については、国際学会での発表を行い、結果をまとめたものが会議録として査読中である。