Undecidable Complexity Statements in a Hierarchy of Extensions of Primitive Recursive Arithmetic

Candidate: Sigal,Ron Mark


For each transfinite ordinal (alpha) (LESSTHEQ) (epsilon)(,0), we fix a unique well-ordering of the natural numbers which we call its canonical well-ordering. Let S((alpha)) be Primitive Recursive Arithmetic plus function definition by transfinite recursion on the canonical well-ordering of order type (alpha). For a hierarchy of theories S((alpha)), where (omega)('(omega)('(omega))) (LESSTHEQ) (alpha) < (epsilon)(,0), we define functions (phi)(,(alpha)) such that statements asserting extremely loose upper bounds on the computational complexity of (phi)(,(alpha)) are independent of S((alpha)). We quantify the gap between actual and provable complexity bounds in terms of the Lob-Wainer hierarchy of rapidly growing functions. A statement asserting a primitive recursive upper bound for the complexity of (phi)(,(alpha)) can be proven in a theory slightly higher in the hierarchy than S((alpha)).