2007 Fiscal Year Annual Research Report
| Project/Area Number |
17540115
|
|---|
| Research Institution | Kobe University |
|---|
Principal Investigator |
新井 敏康 Kobe University, 工学研究科, 教授 (40193049)
|
|---|
| Keywords | 数学基礎論 / 数理論理学 / 証明論 / 順序数 |
|---|
| Research Abstract |
Cut eliminationヤイプシロン代入法による無矛盾性の研究において、そこで対象としていた巨大順序数の公理系がrecursively Mahlo operationで近似できることも示している、ということが分った。
ここでのrecursivelyをはずすと、集合論でいつも問題になる、巨大基数間の大小、一方が他方より大きい、というだけでなく、如何に大きいかを言い表すときにMahlo operationを用いる。これで一方が他方より「ずっと大きい」と結論できる。しかし、それではどれだけどう大きいか、あるいは逆に言えば小さいほうからMahlo operationsをどう繰り返せば大きいほうを近似できるのかは、いままで問われていなかった。
本年度の研究のひとつはこの問いに答えたものである。
次にふたつの論理計算で、ともに論理的に正しい論理式しか証明しない、しかしその証明の長さが一方が他方よりずっと短いことがある(speed-up)、という問題について考察した。これを示すには証明のサイズに関してnon-trivialな下界を示さなければならない。問題になる論理式が量化記号無しの命題論理の論理式である場合であると、このようなspeed-upの存在を示すのは、NP=?co-NPの解決に非常に近く、はなはだ困難である。
本年度の研究では、second order論理計算間でなら、不完全性定理の有限な形を用いてspeed-upが存在することを示した。
さらに多項式時間計算可能関数を特徴付けるsafe recursionから、safe nested recursionに移行すれば、指数時間計算可能関数が特徴付けることができることを示した。
また、無予盾性証明とはいかなる営為なのかについて論じた。
|
