| 研究概要 |
本年度は、先ず、証明の長さについての研究を行った。ひとつには、計算量理論での並列計算での時間量が入力の長さの対数で抑えられるクラスである$NC^{1}$、およびそれに対応する新井による限定算術AID、そして命題論理の体系Frege systemの関係がS.Cook, S.Buss,新井らにより知られていた。集合のtraceに関するBollob\'{a}sの定理がFrege systemで多項式の長さで証明できるかという未解決問題を野崎、新井紀子とともに肯定的に解決した。ふたつめは、述語論理での証明の長さに関するもので、カット消去による証明によりsuper-exponentialな上界が知られていたいくつかの結果について、その上界が本質的に下げることができないことを示した。具体的には、2階イプシロン計算、2階可述的論理計算、不動点論理によるそれぞれの1階述語論理上のspeed-upsである。これらの結果は、主に集合に関する定理の証明論的研究に属する。つぎに行った研究は、集合論の証明論的研究である。これは例えば、Zermelo-Fraenkelの集合論からベキ集合の公理を取り除いた公理系において証明できる$\Pi_{2}$-論理式の限界を決めるもので、手法としては、無限公理付きのKripke-Platek集合論の証明論にSkolem関数を導入して得られた。強い集合論の証明論的研究としては、初めての成果であり、当研究課題の本丸の一部が達成されたことになる。ひとつめの証明の長さに関する成果は、ふたつの論文にまとめて発表し、ふたつめの集合論の証明論的研究は、金沢で行われた国際研究集会において講演により発表し、現在、論文を準備中である。
|
