構成的論理の推論構造の研究

1994 年度 実績報告書

• 研究課題/領域番号: 05680276
• 研究機関: 九州大学
• 研究代表者: 廣川 佐千男 九州大学, 理学部, 助教授 (40126785)
• 研究分担者: 古森 雄一 静岡大学, 理学部, 助教授 (10022302)
• キーワード: 構成的論理 / 型理論 / ラムダ計算

研究概要

『論理式と型の対応』を拡張した『論理式とリダクション規則の対応』の定式化を得た。新しい結合子Pを導入しそのリダクション規則を求め、パースの論理式に対応する結合子論理を定式化した。このリダクション規則は古典論理の証明から構成的証明を抽出する自然な変形である。このリダクション規則によれば、同じ論理式に対する証明はすべて同等となるという知見を得た。従来、古典論理ではチャーチ・ロサ-の性質が成り立たないといわれているが、これを論理式と型との対応から説明するものである。ラムダ計算を拡張したラムダ・ニュー計算をそのリダクション規則による定式化も行なった。これは、継続についての計算規則に類似していることが分り、FelleisenやJacobの研究との関連は今後の課題となった。中間論理の論理式の解析により、一般的に論理式からリダクション規則を生成する見通しがついた。今後、クリプケ・モデルから含意論理式を生成するYankovやZakharyaschevの手法うことにより、統一的な解析実験が必要である。
古森は適切さの論理におけるP‐W問題に対し、Gentzen流の手法を用いた統語的証明を得た。廣川はP‐Wに対するラムダ計算の定式化を与え、P‐Wにおける証明の構造を明らかにした。廣川は、与えられた含意論理式に対し直観主義論理における証明図全体は、ある種の文法で記述できるという結果を得た。更にこのような証明図全体が有限か無限かという問題の複雑さが多項式領域完全であるという知見を得た。高橋、赤間との共同研究では、さらにこのアイデアが高階の型の体系にも拡張できるこという知見を得た。

研究成果

• [文献書誌] Sachio Hirokawa: "The proof of α→α in P-W" Jouvnal of Symbolic logic. (発表予定).
• [文献書誌] Sachio Hirokawa,Yuichi Komori Izumi Takeuti: "A reduction rule for Peirres formule makes all the torms with the same tyyce egucl" RIFIS-TR. 91. 1-4 (1994)
• [文献書誌] Sachio Hirokawa: "Infiniteress of proof(α→α)is polyhomial‐spaie complete" RIFIS-TR. 92. 1-11 (1994)
• [文献書誌] Sachio Hirokawa: "A charrcterization of implicational axiom scheme playing the role of Peirces law in intuitionistic logic" RIFIS-TR. 93. 1-4 (1994)
• [文献書誌] Yuichi Komori: "Syntactic Invostigation into BI Logic and BB′I Logic" Stadir Logica. 53. 397-416 (1994)
• [文献書誌] M.Takahashi,Y.Akama,S.Hirokawa: "Normal Proofs and Their Grammar" Springer Lecture Noter in Computer Science. 789. 465-493 (1994)