| 研究概要 |
PLS(Polynomial Local Search)を拡張したnested PLSというクラスを導入し、nested PLSが有界算術$T^{2}_{2}$での証明つき計算可能関数のクラスと一致することを示した。PLSはS, Bussらにより$T^{1}_{2}$に対応することが示されていた。
またepsilon processesの長さの限界を正確に超限帰納法による計算($\alpha$-recursion)によって与えた。
次にintuitionistic logicでのstrictly positive formulasのcut消去は指数関数による証明の長さの増大しかもたらさないことを示し、これによりstrictly positive operatorsによるintuitionistic logicに基づく不動点理論がintuitionistic arithmeticの保存拡大であることを証明した。Intuitionistic logicに基づく不動点理論に関する従来知られていた証明論的諸結果すべてを包含するものである。
さらに$\Delta∧{0}_{2}$でああることが証明できる集合をErshov hierarchyのどこに位置するかを、その証明が形式化できる公理系によって分類した。これは関数の収束性がある順序数からの下降列の非存在から導かれるということである。
また、その多くの部分が未だ出版されていない順序数論の証明論の概略と近況を述べた。
|
