| 研究課題/領域番号 |
15540107
|
|---|
| 研究機関 | 千葉大学 |
|---|
研究代表者 |
古森 雄一 千葉大学, 総合メディア基盤センター, 教授 (10022302)
|
|---|
| 研究分担者 |
多田 充 千葉大学, 総合メディア基盤センター, 助教授 (20303331)
山本 光晴 千葉大学, 理学部, 助教授 (00291295)
廣川 佐千男 九州大学, 情報基盤センター, 教授 (40126785)
藤田 憲悦 群馬大学, 工学部, 助教授 (30228994)
鹿島 亮 東京工業大学, 情報理工学研究科, 助教授 (10240756)
|
|---|
| キーワード | 数理論理学 / ラムダ計算 / 集合論 / P=NP問題 / BCK論理 / 古典論理 / 直観主義論理 / 極小論理式 |
|---|
| 研究概要 |
チャーチの論理を含んだラムダ計算を再生させるための体系として最も有力なものであるBCKβηについての問題「α^*が体系BCKβηで証明できるときαが直観主義論理で証明できるか」が前年度の研究で提起された。
http://www.math.s.chiba-u.ac.jp/〜komori/kouen/
今年度,その問題について精力的な研究が行われたが問題が難しく若干の進展があったが来年度に残された重要な問題となっている。
前年度に提出した「直観主義論理で証明できない極小論理式は古典論理の公理になっているか」という問題については鹿島がそのための体系を作って部分的な解答を与えた。最終的解答は残された問題である。
また,鹿島は含意と論理積しか含まない直観主義命題論理について,それに2階の任意を加えて言語を拡張しても任意が外側にしか現れないならば保存拡張であるという興味深い結果を得た。この結果は論理和を言語として加えた体系の保存拡張性についての問題に部解答を与える。完全な解答については今年度も本科研費で招いたAgata Ciabattoni氏と共同研究を進めている。
古典命題論理の含意断片の極小論理式による公理化について次のような結果を得た。体系BCPは独立な公理系となっている。体系BCIK'W'に極小論理式を加えて古典命題論理の含意断片の独立な公理系が作れるかどうかは未解決である。
|
