2006 Fiscal Year Annual Research Report
| Project/Area Number |
15540107
|
|---|
| Research Institution | Chiba University |
|---|
Principal Investigator |
古森 雄一 千葉大学, 総合メディア基盤センター, 教授 (10022302)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
多田 充 千葉大学, 総合メディア基盤センター, 助教授 (20303331)
山本 光晴 千葉大学, 理学部, 助教授 (00291295)
廣川 佐千男 九州大学, 情報基盤センター, 教授 (40126785)
藤田 憲悦 群馬大学, 工学部, 助教授 (30228994)
鹿島 亮 東京工業大学, 情報理工学研究科, 助教授 (10240756)
|
|---|
| Keywords | 数理論理学 / ラムダ計算 / 集合論 / P=NP問題 / BCK論理 / 古典論理 / 直観主義論理 / 極小論理式 |
|---|
| Research Abstract |
チャーチの論理を含んだラムダ計算を再生させるための休系として最も有力なものであるBCKβηについての問題「α^*が体系BCKβηで証明できるときαが直観主義論理で証明できるか」が前々年度の研究で提起された。
http://www.math.s.chiba-u.ac.jp/~komori/kouen/
昨年度および今年度,その問題について精力的な研究が行われた。その結果,模型による方法と構文論的な方法の融合による解決の可能性が示唆された。しかし,解決には至っていないので,その解決は今後に残された重要な課題となっている。
直観主義論理で証明できない極小論理式は古典論理の公理になっているか」という問題について,前年度に鹿島がそのための体系を作って部分的な解答を与えた。最終的解答は残されており非常に興味深い問題となっている。
また,古森と長はλρ計算の強正規化定理の証明を与えた。その方法は従来の方法とは全く異なった新しいものである。その方法は自然でかっ応用性に富んでおり,Parigotなどの他の体系の強正規化定理の証明にも使えるものとなっている。
前年度から今年度にかけて,古典命題論理の含意断片の極小論理式による公理化について次のような結果を得ている。体系BCPは独立な公理系となっている。体系BCIK'W'に極小論理式を加えて古典命題論理の含意断片の独立な公理系が作れるかどうかは未解決である。
直観主義論理の含意断片で論理和を表現できるか(この意味については注意を要する)という問題は部分的解を鹿島が与えているが,完全な解決が興味深い問題として残っている。
|
Research Products
(7 results)
