|
存在定理「条件を満たす全てのXに対して，条件を満たす解Yが存在する」の解の一様計算可能性の一つの形式化として「XからYを計算する原始再帰的な一様計算手続きが存在し，それが解を与えることが算術的内包公理を含む古典高階算術体系で証明できる」という概念を考え，比較的単純な論理式として形式化される全ての存在定理に対して，上記の意味での解の一様計算可能性は，直観主義高階算術体系にシグマ02二重否定シフト原理と可算選択公理を加えて得られる準直観主義高階算術体系における証明可能性によって特徴づけられることを示した．
さらに，この準直観主義高階算術体系と構成的逆数学における既存の体系の関係性を解明した．
|
