| 研究実績の概要 |
本研究課題である中間２階命題論理の基本は直観主義２階命題論理である。そして直観主義２階命題論理は２階型付きラムダ計算と実質的に同じである（カリー・ハワード同型対応）。このような背景のもとで、２階型付きラムダ計算の完全性に関する研究をおこなった。
一般に論理の体系（Lと呼ぶ）について、論理式の「意味」を適切に定義した上で、論理式に関する２条件「恒真である」と「Lで導出できる」が同値になることを、Lの完全性と呼ぶ。完全性は論理の体系に求めらる最も基本的な性質である。
ところが型付きラムダ計算の体系については、β同値な項を同一視するという特別な規則を加えた体系については完全性が知られていたが、特別な規則を入れない最も基本的な体系（単純型付きラムダ計算）については完全性が未解決であった。そこで文献[1]（研究協力者松田直祐ほか１名との共同研究）でこの問題を解決した。具体的には、ラムダ項の冪集合を用いて Term Space という自然な意味を定めて完全性を示した。さらにこの結果を、私の学生との共同研究によって２階型付きラムダ計算に拡張した（投稿論文準備中）。ただしここでの２階型付きラムダ計算の体系には、η同値な項を同一視するという特別な規則を追加してある。これはTerm Space を自然に定義するための必然的な追加であるのだが、この追加規則なしの最も基本的な体系に対する完全性は今後の研究課題である。
[1] Ryo Kashima, Naosuke Matsuda, and Takao Yuyama: Term-Space Semantics of Typed Lambda Calculus, Notre Dame Journal of Formal Logic 61[4], pp.591-600 (2020).
|
