| 研究概要 |
本年度は以下の2点について成果を得た.
1.深さの上限が入力の対数の繰り返しになるような回路で計算できる関数の族を定義し,これに対する弱い算術の体系が,弱い数学的帰納法を用いて公理化されることを示した.このような回路は,対数の繰り返しの回数によって階層を構成するが,計算量理論においてすでに得られているグラフ到達可能性問題の下界を用いて,この階層が分離されることがわかる.このことから上で定義した算術体系の証明能力が異なることが示される.またパリティ関数の下界性の証明を用いると,異なる部分における分離が導かれるので,このことからも体系の分離を示すことが可能である.
2.Cloteと竹内によって定義された二階算術の体系T^<pol>は多項式時間で決定可能な述語を定義できるが,同様の関数は定義できないことが知られている.竹内はこのような具体的な関数として,除算がとれることを証明している.この証明は証明論におけるカット除去定理を用いた複雑なものであるが,これに対して,ある種の1階算術のモデルはT^<pol>のモデルに拡張できることを示し,これを用いてT^<pol>では2の冪乗以外の自然数による除算が定義できないことを証明した.これは上述の竹内による定理の拡張になっており,また一階算術の独立性に関するJohannsenの定理の拡張にもなっている.
|
