The Veblen functions for computability theorists

Abstract

We study the computability-theoretic complexity and proof-theoretic strength of the following statements: (1) "If X is a well-ordering, then so is epsilon_X", and (2) "If X is a well-ordering, then so is phi(alpha,X)", where alpha is a fixed computable ordinal and phi the two-placed Veblen function. For the former statement, we show that omega iterations of the Turing jump are necessary in the proof and that the statement is equivalent to ACA_0^+ over RCA_0. To prove the latter statement we need to use omega^alpha iterations of the Turing jump, and we show that the statement is equivalent to Pi^0_{omega^alpha}-CA_0. 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 phi(X,0)" is equivalent to ATR_0 over RCA_0.

arXiv comment26 pages, 3 figures, to appear in Journal of Symbolic Logic

Cited by in corpus (5)

• ${\Pi }_1^1$-Comprehension as a Well-Ordering Principle
• Computable Aspects of the Bachmann-Howard Principle
• Derivatives of normal functions in reverse mathematics
• A note on ordinal exponentiation and derivatives of normal functions
• Iterated Priority Arguments in Descriptive Set Theory