チャーチのラムダ計算のBCK論理による再生

2003 Fiscal Year Annual Research Report

• Project/Area Number: 15540107
• Research Institution: Chiba University
• Principal Investigator: 古森 雄一 千葉大学, 総合メディア基盤センター, 教授 (10022302)
• Co-Investigator(Kenkyū-buntansha): 廣川 佐千男 九州大学, 情報基盤センター, 教授 (40126785) ; 山本 光晴 千葉大学, 理学部, 助教授 (00291295) ; 桜井 貴文 千葉大学, 理学部, 助教授 (60183373) ; 鹿島 亮 東京工業大学, 情報理工学研究科, 助教授 (10240756) ; 藤田 憲悦 島根大学, 総合理工学部, 助教授 (30228994)
• Keywords: 数理論理学 / ラムダ計算 / 集合論 / 部分構造論理 / BCK論理 / 古典論理 / 直観主義論理

Research Abstract

チャーチの論理を含んだラムダ計算を再生させるための体系として最も有力なものであるBCKβηについて新たな知見が得られた。体系BCKβηはラムダ計算を含んでいるので万能なシステムである。そのため直観主義論理や古典論理のシミュレートできることは明らかである。しかしながらラムダ計算の万能性を使ってのシミュレーションにはゲーデル数化などの複雑な変換が必要である。グリベンコの定理を利用した直観主義論理による古典論理のシミュレーションのように簡単で論理らしい変換が望ましい。そのような直観主義述語論理から体系BCKβηへの変換を見つけることができた。その変換*を使うと直観主義述語論理の論理式αに対してαが直観主義論理で証明できるならばα*が体系BCKβηで証明できることが分かった。しかし,その逆であるα*が体系BCKβηで証明できるときαが直観主義論理で証明できるかどうかは未解決である。この問題は興味深い問題として来年度以降に残された。
体系λρ計算については弱正規化定理の直接証明がうまくいかずに強正規化定理を経由して証明した。その証明には体系λ計算の強正規化定理が用いられた。これは体系λ計算の強正規化定理が証明論的に役立った珍しい例となった。また,体系λρ計算に変形規則を加えた体系については弱正規化定理を直接証明することができた。しかしこの体系は合流性が成立しない。この体系にさらに変形規則を付け加えて合流性が成り立つつぶれない体系が作れるかということも興味深い問題として残された。

Research Products

• [Publications] Sachio Hirokawa: "Semi-Automatic Construction of Metadata from A Series of Web Documents"Lecture Notes in Computer Science. 2903. 942-953 (2003)
• [Publications] 藤田 憲悦: "λμ計算のモデルについて"コンピュータソフトウェア. 20・3. 120-134 (2003)
• [Publications] Ken-etsu Fujita: "A sound and complete CPS-translation for λμ-calculus"Lecture Notes in Computer Science. 2701. 120-134 (2003)
• [Publications] Ryo Kashima: "On Semilattice Relevant Logics"Mathematical Logic Quarterly. 49・4. 401-414 (2003)
• [Publications] Masahiko Sato: "Calculi of Meta-variables"Lecture Notes in Computer Science. 2803. 484-497 (2003)
• [Publications] Katsumasa Ishii: "Sequent Calculi for Visser's Propositional Logics"Notre Dame Journal of Formal Logic. 42・1. 1-22 (2003)