| 研究分担者 |
赤間 陽二 東北大学, 大学院・理学研究科, 助教授 (30272454)
竹田 雅好 東北大学, 大学院・理学研究科, 教授 (30179650)
森田 康夫 東北大学, 大学院・理学研究科, 教授 (20011653)
山崎 武 大阪府立大学, 総合科学部, 助手 (30336812)
|
|---|
| 研究概要 |
解析学を基礎付ける土台としてHilbertが導入した2階算術には,様々な種類の形式化が存在する.なかでも計算可能な関数や集合を扱う体系RCA_0と,それにコンパクト性の議論を付加した体系WKL_0は,解析学の基礎として十分な強さを持ちながら,無矛盾性に関してはPRA(「有限の立場」の形式化)と同等になることから,Hilbertのプログラムに関連して重要な意義をもつ.田中と山崎は,S.Simpsonの協力の下で、WKL_0におけるある形の定理に対して,その証明からコンパクト性の議論を取り除けること,すなわちRCA_0における証明に変換できることを証明する一方,コンパクト性と類似する有界従属選択公理に対しては,その使用を一斉には消去できないことを示した.そこで,いくつかの定理について個別に有界従属選択の消去可能性を議論し,その背後にある一般的な原理を探った.たとえば,実数や複素数に関する命題の多くは,量化記号消去定理を用いて充足関係を導入することで有界従属選択の使用を避けることができることがわかった.Simpson-田中-山崎の結果は,WKL_0の高階算術化が難しいことを意味しており,この状況を厳密に調べる研究の一つが山崎と坂本伸幸によってなされた.すなわち,WKL_0等の高階一様版はWKL_0より真に強い原理になる.また,山崎は,多項式時間計算の体系における逆数学現象や,直観主義理論の完全性定理に必要となる公理についても調べた.赤間は,部分組合せ代数の中に極限操作を導入し,そこで表現できる関数とlimiting recursive functionとの関係を調べた.
最後に,田中は,超算術的選択公理HACに対して,13種類のバリエーションを定義し,それぞれと同値な公理を決定した.
|
