RCA_0におけるハーリントンの定理とπ^1_ 1式の証明の長さの比較

• Date/Time: May 18, 2018 (Friday) / 16:00 - 17:00

• Speaker: 古川 大樹 氏 (東北大学大学院 理学研究科)

• Venue: Rm 1201, Science Complex A, Tohoku Univ.

• Abstract: ハーリントンの定理はWKL_0とRCA_0の間にπ^1_ 1保存拡大が成り立つことを主張する定理であるが、その証明は普通、モデル論的になされる。しかし、 この証明をRCA_0内で形式的に証明し直すことでWKL_ 0におけるπ^1_1式の証明をRCA_ 0における証明に変換する具体的な手続きが与えられる。これを考察することで、RCA_0における証明の長さがWKL_ 0における元の証明の長さの多項式で抑えられることがわかる。