| 研究概要 |
0.TRDBと略記される構成的数字の体系(一階算術HAにVf,transfinite recursionで定義される速語H、bar inductionを加えたもの)と、transfinitely defined typesを持つ.bar recursionをベ-スにした汎関数の体系TRMの相互関係を明らかにし、TRDBのformulaをtype,proofをtermと考えたときのTRDBの計算性の意味を明確にすることが目標であった。その目標はすべて達成され、現在論文作製中である。龍谷大学の林晋氏との共同研究である。なお他に広い意味の研究協力者たちもあり、その成果も発表論文の項目に記す。以下研究内容を詳細する。
1.TRMのtypeの集合論的モデルを構成。(typeのdegrllに関する超限帰納法による。また、それがtermの構成と整合的であることを示した。
2.TRMの有限のtypeのtermの特徴づけ。
3.TRDBをCurryーHoward型の写像でTRMに写し、TRDBの正規化がTRMの正規化に写されること、および、過去に行った、modified realizability interpretationと同じtermが得られることを示した。なお、このTRDBは、前年度までの体系よりは一般化されているが、それでも同様の結果が得られることが分った。
4.既存の還元法による無予盾性証明との関連は、還元のプロセスをtermの還元と考えて、証明図のdegreeに関する超限帰納法とbar inductionによってTRMへの埋め込みを考える。この点はまだ研究続行中である。
なお中間報告の意味でLogic Colloquium '90(Helsinki)に演題を出し、また平成3年4月の日本数学会において(林晋氏と共同で)講演を行った。
|
