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