| 研究概要 |
本研究は1. 部分構造論理の代数的証明論、および2. ルディクス理論への余代数的アプローチの二点を主眼としている。
1. については、独自の考案による部分構造階層の中で、証明論の限界を示す境界線を画定することを目標としている。証明論のポテンシャルをより高めるため、これまでの(代数的に自然な)直観主義枠組みを(より多くの論理を捉えうる)古典的枠組みに拡張する研究を行った。これは単なる自明な拡張にとどまらず、アーベル論理、ウカシェヴィッチ無限多値論理など、さまざまな具体的論理に統一的観点を与えるものとなった。成果は国際学会CSL'09に投稿し受理された。また第一回非古典数学会議、国際学会TACL'09における招待講演の際にも発表した(Ciabattoni, Strassburger,照井の共同研究)。
さらに、代数的証明論は非古典論理の代数的意味論と証明論を両輪として展開されるが、そのうち純代数的に説明可能な部分を論文の形にまとめ上げ、雑誌に投稿した(Ciabattoni, Galatos,照井の共同研究)。
2. については、論理的完全性の対話的理解を求めて、古典的なゲーデルの完全性定理をゲーム意味論・ルディクスの枠組みで再解釈する研究を行った。まずは通常の有限的・帰納的観点の中でゲーデルの完全性定理の対話版を証明し、成果を国際学会TACL'09で発表した。次に無限的・余帰納法的観点からゲーデルの定理の再検討を行った。これは前研究を補完するものであり、数理論理学におけるラッセル・パラドックス、プログラミング理論における一般再起型の解釈、実現可能性理論における直交性の概念など、多くの重要概念を統合するものとなった。成果は論理・理論計算機科学分野において最も権威のある学会の一つであるLICS'10に投稿し、受理された(Basaldella,照井の共同研究)。
|
