| 研究分担者 |
櫻井 貴文 (桜井 貴文) 千葉大学, 理学部, 助教授 (60183373)
山本 光晴 千葉大学, 理学部, 助教授 (00291295)
廣川 左千男 (廣川 佐千男) 九州大学, 情報基盤センター, 教授 (40126785)
藤田 憲悦 群馬大学, 工学部, 助教授 (30228994)
鹿島 亮 東京工業大学, 情報理工学研究科, 助教授 (10240756)
多田 充 千葉大学, 総合メディア基盤センター, 助教授 (20303331)
|
|---|
| 研究概要 |
研究分担者たちの活発な研究活動により,体系BCKβηと古典命題論理の証明図の性質は明らかになりつつある。ここでは,研究代表者の古森による2つの成果について述べる。
第一のものは体系BCKβηに関するものである。体系BCKβηを用いてチャーチの当初の目論見を再生するためには,体系BCKβηで古典論理のシミュレーションが論理的にできる必要がある。直観主義論理で古典論理のシミュレーションができることは知られているので,体系BCKβηで直観主義論理のシミュレーションが論理的にできることが分かればよい。これについて古森は二つの方法を提示し,そのどちらについても次もことを示した:
変換*が存在し,任意の直観主義論理の論理式Aにたいして,A*は体系BCKβηの論理式でAが直観主義論理で証明できるならばA*は体系BCKβηで証明できる。
この逆A*が体系BCKβηで証明できるならば,Aが直観主義論理で証明できるが示せれば,体系BCKβηで直観主義論理のシミュレーションが論理的にできることが示されたことになる。しかし,逆はまだ未解決である。二つの方法のうちの一つは,変換*が単純なものであり,もう一つは変換は少し複雑になるが逆の証明のことを考えたものである。後者について,逆が成立することを示すことは残された大きな課題である。
第二のものは1998-1999年度の科学研究費補助金で行った研究「部分構造論理の研究」の研究成果報告書で述べた第二の成果と関係している。そこで述べた体系を更に改良した体系λρという古典論理の体系を作り,その体系のChurch-Rosser性を証明した。その証明は全く新しいものであり,その方法で他の体系のChurch-Rosser性の新たな証明が得られることも判明した。
|
