限定算術と多項式時間計算量

点击翻译按钮获取中文摘要

限定算術(Bounded arithmetic)の超準モデルMと、そのgeneric拡大M[G]の中間にある構造の構造を調べその結果を弱い帰納法と最小値原理との関係等に応用した。Lを限定算術の言語、RをLに含まれない一変数の新しい述語とし、MIN(R)は"Rは最小元を持つ"を意味する命題とする。この時T_2^1(R)からMIN(R)は簡単に証明されるが、T_2^1(R)より弱い体系で証明可能かどうかは知られていなかった。MとM[G]の中間の構造であるsymmetricモデルがMIN(R)を満たさないようになる、すなわちRが最小元を持たないようにするための条件を調べた。この中間構造としてT_2^0(R)となるものがとれることから、T_2^0(R)からMIN(R)が証明されないことがわかる。あるΣ_0^b(R)-formulaψ(x,R)が存在してS_2^1(R)からMIN(ψ(x,R))が証明できないことは、竹内-Pudlak-Krajicekらの結果から導かれるが、ψ(x,R)がどのような命題になるかは具体的にはわかっていない。従ってS_2^1(R)からMIN(R)が証明できるかどうかは未解決であるが、symmetricモデルがS_2^1(R)のモデルになるための条件について調べた。symmetricモデルを使うことによって、弱い算術と数え上げ原理との関係についても、調べた。有限数え上げの場合を除いて、数え上げ原理はT_2^0(R)と独立であることが示された。この場合も最小値原理と同様にS_2^1(R)に対して独立になるかはわからず、そうなるための条件などについて調べた。