Return to Answer

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.

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, there are 'pathological' representations of $ε_0$ such that (1) ERA constructively proves that the representation is elementary time equivalent to Cantor Normal Form, and (2) 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.)

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.

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)$).

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.

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. I did not analyze whether it is possible to come up with an elementary time equivalent representation (of say Cantor Normal Form) that is pathological under polynomial time computability.

Also, the form in the question is just one of a number of different ways to define the proof ordinal of a theory. For 'reasonable' theories (and reasonable ordinal representations), the different definitions lead to the same ordinal, but that is not the case in general.

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.

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, there are 'pathological' representations of $ε_0$ such that (1) ERA constructively proves that the representation is elementary time equivalent to Cantor Normal Form, and (2) 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.)

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.

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. We have $\mathrm{ERA}⊢\mathrm{TI}(α,P')⇔\mathrm{TI}(α,P)$, and if $P$ is exponential time computable, then $P'$ is polynomial time computable.

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. I did not analyze whether it is possible to come up with an elementary time equivalent representation (of say Cantor Normal Form) that is pathological under polynomial time computability.

Also, the form in the question is just one of a number of different ways to define the proof ordinal of a theory. For 'reasonable' theories (and reasonable ordinal representations), the different definitions lead to the same ordinal, but that is not the case in general.

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.

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. I did not analyze whether it is possible to come up with an elementary time equivalent representation (of say Cantor Normal Form) that is pathological under polynomial time computability.

Also, the form in the question is just one of a number of different ways to define the proof ordinal of a theory. For 'reasonable' theories (and reasonable ordinal representations), the different definitions lead to the same ordinal, but that is not the case in general.