According to [The Art of Ordinal Analysis](https://www1.maths.leeds.ac.uk/%7Erathjen/ICMend.pdf), the proof theoretic ordinal of a theory $T$ is the least ordinal $\alpha$ such that:


$${\bf ERA}+TI(\alpha,ECP)\vdash Con(T)$$


In above definition, $ECP$ stands for Elementary computable predicates and $TI(\alpha, A)$ stands for transfinite induction up to $\alpha$ for predicates in complexity class $A$.



> 
> Q. Is it possible to reduce the complexity of predicates for transfinite induction in above definition to a smaller complexity class?
> 
> 
> For example, Is $Con(T)$ provable from ${\bf ERA}+TI(\beta,P)$ for some ordinal $\beta$ ?($P$ stands for polynomial time predicates.)
> 
> 
> 



Complexity of induction formulas in proof theoretic ordinals
By a padding argument, for reasonable notation systems, an elementary time computable predicate $P$ in $\mathrm{TI}(β,ECP)$ can be chosen to be polynomial time computable.


For example, for limit $α<β$, set $P'(α+(2^n+1) 2^{\mathrm{code}(α)}) ⇔ P(α+n)$ with $P'$ true for ordinals that are not in that form ('+' refers to ordinal addition; n∈ℕ). With this padding, we get an order preserving bijection between counterexamples to $P$ and counterexamples to $P'$. We have $\mathrm{ERA}⊢\mathrm{TI}(β,P')⇔\mathrm{TI}(β,P)$, and if $P$ is exponential time computable, then $P'$ is polynomial time computable (as a predicate on codes for ordinals using the notation system in the $\mathrm{TI}$).


A caveat is that we require the coding of $α+n$ to be well-behaved in relation to the coding of $α$, but this is satisfied by reasonable notation systems. Note, however, that there are recursive ordinal notation systems where, for example, $α→α+1$ is not recursive. Also, the reason elementary time computability was used over polynomial time computability is that reasonable representations of ordinals appear to be elementary time isomorphic (at least for ordinals for which ordinal analysis is well-understood), but polynomial time reducibility distinguishes between, for example, unary and binary numbers.


Also, the form in the question is just one of a number of different ways to define the proof ordinal of a theory. Since your definition uses Con(T), it is a form of $Π^0\_1$ ordinals, but like $Π^0\_2$ ordinals and unlike a more fine-grained notion of $Π^0\_1$ ordinals, it does not distinguish between say PA and PA+Con(PA). For 'natural' theories (and reasonable ordinal representations), the different definitions lead to the same ordinal, but that is not the case in general.


*An Extension*


There are 'pathological' representations of $ε\_0$ such that (1) ordinal comparison is exponential time computable, (2) ERA constructively proves that the representation is elementary time equivalent to Cantor Normal Form, and (3) ERA proves transfinite induction for polynomial time predicates. Essentially, given a polynomial time $P$ that holds for some $n > 2 \, \mathrm{code}(P)$, make sure that the least such $n$ codes a finite ordinal, with comparison of finite ordinals agreeing with comparison of their codes.


However, if ERA constructively proves that $ωβ=β$ (using an order-preserving computable injection $β×ω→β$) and that ordinal comparison is polynomial time computable, then $\mathrm{ERA}⊢\mathrm{TI}(β,Π^0\_1) ⇔ \mathrm{TI}(β,\mathrm{P})$ (P (without italics) means polynomial time). Essentially (using a slightly stronger assumption), given a $Π^0\_1$ $P$, if $¬P(α)$, then set $¬P'(α')$ for every $α'$ with $ωα≤α'<ω(α+1)$ with $\mathrm{code}(α')$ sufficiently large for us to have time to refute $P(α)$ (and to compute $ωα$ and $ω(α+1)$).


