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

はしがき


本研究は, 「チャーチのラムダ計算の BCK 論理による再生」の表題のもとに, 平成15年度から平成18年度にかけての4年間にわたり, 文部科学省科学研究費補 助金の交付を受けて行われた。 本研究の目的は, チャーチがラムダ計算を考えた当初の目論見を再生することであった。 チャーチがラムダ計算を考えた当初は論理を含んでいて, その体系で数学を構築するのが目 的であった。しかし, Kleene とRosser が1935 年にそれが矛盾を含むことを発見してからは, 主 に論理を除いた体系(も非常に豊富な内容を含むので) が型なしラムダ計算として研究されてき た。古森は1987 年のWhite の結果からラムダ計算にBCK 論理を入れても(この体系をBCKβη と名づけた) 無矛盾であることに気が付き, さらに論理を含む型なしラムダ計算の模型を考案し それらを合わせて1989 年に論文にした。このような模型の考案は世界でもはじめてのことで あった。 この「はしがき」の末尾の「研究発表」にあるように, 研究分担者たちの活発 な研究活動により, 体系BCKβηと古典命題論理の証明図の性質は明らかになりつつある。 ここでは, 研究代表者の古森による２つの成果について述べる。

第一のものは体系BCKβηに関するものである。体系BCKβηを用いてチャーチの当初の目論 見を再生するためには, 体系BCKβηで古典論理のシミュレーションが論理的にできる必要が ある。直観主義論理で古典論理のシミュレーションができることは知られているので, 体系 BCKβηで直観主義論理のシミュレーションが論理的にできることが分かればよい。これにつ いて古森は二つの方法を提示し, そのどちらについても次もことを示した:
変換 * が存在し, 任意の直観主義論理の論理式 A にたいして, A* は体系BCKβηの論理式で A が直観主義論理で証明できるならば A* は体系BCKβηで証明できる。
この逆A* が体系BCKβηで証明できるならば, A が直観主義論理で証明できるが 示せれば, 体系BCKβηで直観主義論理のシミュレーションが論理的にできることが示された ことになる。しかし, 逆はまだ未解決である。二つの方法のうちの一つは, 変換 * が単純な ものであり, もう一つは変換は少し複雑になるが逆の証明のことを考えたものである。後者 について, 逆が成立することを示すことは残された大きな課題である。

第二のものは 1998-1999年度の科学研究費補助金で行った研究「部分構造論理の研究」の 研究成果報告書で述べた第二の成果と関係している。そこで述 べた体系を更に改良した体系λρという古典論理の体系を作り, その体系の Church-Rosser 性を証明した。その証明は全く新しいものであり, その方法で他の体系の Church-Rosser 性 の新たな証明が得られることも判明した。

また, 本科学研究費で招聘した Agata Ciabattoni と共同研究する予定で 2005 年 3 月に作 成した 3 つの問題がある。これらの問題は理解するのが容易で，解くのもそれほど困難では ないと考えられたが, どの問題も解決には至っていない。研究が進むにつれて 3 つの問題と も非常によい問題であるということが分かってきた。数学の研究において未解決な良問を作る ということは, 時として問題を解くことと同じように重要なことである。そのような重要な役 割を果たしたと考えている。

2007 年 5 月 31 日
古森 雄一
研究組織
交付決定額(配分額)(金額単位: 円)
直接経費 間接経費 合計
平成15年度 1,200,000 0 1,200,000
平成16年度 1,100,000 0 1,100,000
平成17年度 600,000 0 600,000
平成18年度 600,000 0 600,000
総計 3,500,000 0 3,500,000
研究発表
(1)学会誌等
(2)口頭発表
(3)出版物
inserted by FC2 system