THE VEBLEN FUNCTIONS FOR COMPUTABILITY THEORISTS
Alberto Marcone, Antonio Montalbán · 2010
We study the computability-theoretic complexity and proof-theoretic strength of the following statements: (1) “If X is a well-ordering, then so is εX”, and (2) “If X is a well-ordering, then so is ϕ(α, X)”, where α is a fixed computable ordinal and ϕ represents the two-placed Veblen function. For the former statement, we show that ω iterations of the Turing jump are necessary in the proof and that the statement is equivalent to ACA + 0 over RCA0. To prove the latter statement we need to use ωα iterations of the Turing jump, and we show that the statement is equivalent to Π0 ωα-CA0. Our proofs are purely computability-theoretic. We also give a new proof of a result of Friedman: the statement “if X is a well-ordering, then so is ϕ(X, 0)” is equivalent to ATR0 over RCA0.