The Veblen functions for computability theorists

TL;DR

This paper analyzes the proof-theoretic strength of statements involving Veblen functions and well-orderings, establishing their equivalence to certain subsystems of second-order arithmetic through computability-theoretic methods.

Contribution

It provides new computability-theoretic proofs linking Veblen function statements to subsystems like ACA_0^+ and Pi^0_{omega^alpha}-CA_0, clarifying their proof-theoretic strength.

Findings

Omega iterations of the Turing jump are needed for the first statement.

The first statement is equivalent to ACA_0^+ over RCA_0.

The second statement is equivalent to Pi^0_{omega^alpha}-CA_0.

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.