2004 Fiscal Year Annual Research Report
| Project/Area Number |
15540107
|
|---|
| Research Institution | Chiba University |
|---|
Principal Investigator |
古森 雄一 千葉大学, 総合メディア基盤センター, 教授 (10022302)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
桜井 貴文 千葉大学, 理学部, 助教授 (60183373)
山本 光晴 千葉大学, 理学部, 助教授 (00291295)
廣川 左千男 九州大学, 情報基盤センター, 教授 (40126785)
藤田 憲悦 群馬大学, 工学部, 助教授 (30228994)
鹿島 亮 東京工業大学, 情報理工学研究科, 助教授 (10240756)
|
|---|
| Keywords | 数理論理学 / ラムダ計算 / 集合論 / 部分構造論理 / BCK論理 / 古典論理 / 直観主義論理 / 極小論理式 |
|---|
| Research Abstract |
前年度の研究で,チャーチの論理を含んだラムダ計算を再生させるための体系として最も有力なものであるBCKβηについて新たな知見が得られた。その知見とは体系BCKβηで論理らしい変換により直観主義論理や古典論理のシミュレートできそうだというものである。その変換^*についてはより簡単なものが考案された。詳しいことは産業総合研究所での講演で述べた。その内容は以下に置いた:
http://www.math.s.chiba-u.ac.jo/〜komori/kouen/
その変換^*を使うと直観主義述語論理の論理式αに対してαが直観主義論理で証明できるならばα^*が体系BCKβηで証明できることの証明は以下に置いた:
http://www.math.s.chiba-u.ac.jp/〜04um0304/
その逆であるα^*が体系BCKβηで証明できるときαが直観主義論理で証明できるかどうかはかなり難しい未解決であることが分かってきた。この問題の解決は研究課題終了年までに解決すべき問題として残された。
直観主義論理,古典論理と極小論理式に関連した興味深い問題を提出した。直観主義論理で証明できない極小論理式は古典論理の公理になっているかというものである。現在知られている中間(implicational fragment)論理の公理は極小論理式ではない。この問題については今年度本科研費で招いたAgata Ciabattoni氏と共同研究を進めている。
|
Research Products
(6 results)
