チャーチのラムダ計算のBCK論理による再生
【研究分野】数学一般(含確率論・統計数学)
【研究キーワード】
ラムダ計算 / BCK論理 / チャーチ / 古典論理 / Curry-Howard対応 / 直観主義論理 / ラッセルの逆理 / 集合論 / 数理論理学 / P=NP問題 / 極小論理式 / 部分構造論理
【研究成果の概要】
研究分担者たちの活発な研究活動により,体系BCKβηと古典命題論理の証明図の性質は明らかになりつつある。ここでは,研究代表者の古森による2つの成果について述べる。
第一のものは体系BCKβηに関するものである。体系BCKβηを用いてチャーチの当初の目論見を再生するためには,体系BCKβηで古典論理のシミュレーションが論理的にできる必要がある。直観主義論理で古典論理のシミュレーションができることは知られているので,体系BCKβηで直観主義論理のシミュレーションが論理的にできることが分かればよい。これについて古森は二つの方法を提示し,そのどちらについても次もことを示した:
変換*が存在し,任意の直観主義論理の論理式Aにたいして,A*は体系BCKβηの論理式でAが直観主義論理で証明できるならばA*は体系BCKβηで証明できる。
この逆A*が体系BCKβηで証明できるならば,Aが直観主義論理で証明できるが示せれば,体系BCKβηで直観主義論理のシミュレーションが論理的にできることが示されたことになる。しかし,逆はまだ未解決である。二つの方法のうちの一つは,変換*が単純なものであり,もう一つは変換は少し複雑になるが逆の証明のことを考えたものである。後者について,逆が成立することを示すことは残された大きな課題である。
第二のものは1998-1999年度の科学研究費補助金で行った研究「部分構造論理の研究」の研究成果報告書で述べた第二の成果と関係している。そこで述べた体系を更に改良した体系λρという古典論理の体系を作り,その体系のChurch-Rosser性を証明した。その証明は全く新しいものであり,その方法で他の体系のChurch-Rosser性の新たな証明が得られることも判明した。
【研究代表者】