10
$\begingroup$

According to The Art of Ordinal Analysis, 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.)

Improve this question
$\endgroup$
4
  • $\begingroup$ I don't know enough proof theory to say anything really helpful here, but I should point out that, when the complexity of the class $X$ in $TI(\alpha,X)$ gets low enough, you need to worry, more the usual, about the details of the notation system used for $\alpha$. $\endgroup$
    – Andreas Blass
    Commented Aug 14, 2017 at 2:00
  • $\begingroup$ @AndreasBlass: At least for ordinals below $\epsilon_0$, a notation system is introduced in Ordinal Notations and Well-Orderings in Bounded Arithmetic (cs.swan.ac.uk/~csarnold/publ/show-paper.php?10) with low complexity. $\endgroup$
    – Erfan Khaniki
    Commented Aug 14, 2017 at 2:28
  • $\begingroup$ I agree that, below $\varepsilon_0$ (and in fact for some distance beyond that), all the notation systems I've seen are rather obviously equivalent, so I'd expect their equivalence to be provable in rather weak theories. The problems begin either at higher ordinals or at extremely weak theories. $\endgroup$
    – Andreas Blass
    Commented Aug 14, 2017 at 2:32
  • $\begingroup$ @AndreasBlass: Actually, my main concern is about $PA$ and weaker systems. $\endgroup$
    – Erfan Khaniki
    Commented Aug 14, 2017 at 2:37

1 Answer 1

Reset to default
3
$\begingroup$

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

Improve this answer
$\endgroup$
5
  • $\begingroup$ It's not trivial for me why a padding argument works. Actually I don't think it's true that $\forall n,m\left(n\prec_\alpha m \rightarrow \left<n,2^n \right > \prec_\alpha \left <m,2^m \right >\right )$. Could you clarify your answer more? $\endgroup$
    – Erfan Khaniki
    Commented Sep 30, 2017 at 12:20
  • $\begingroup$ @ErfanKhaniki I clarified the answer: In the definition of $P'$, '+' refers to ordinal addition rather than addition of the natural numbers coding the ordinals. Let me know if something else is unclear. $\endgroup$
    – Dmytro Taranovsky
    Commented Sep 30, 2017 at 16:28
  • $\begingroup$ You use ordinals in the inputs of your functions, but my question is in the language of arithmetic, so the only objects are numbers. Therefore for a fix good definable wellordering $\alpha$, by formula $\prec_\alpha$, you should show there exists a good function $f$ such that: $ERA\vdash \forall n(P(n) \leftrightarrow P'(f(n)))$ and also $ERA\vdash\forall n,m\left(n\prec_\alpha m\rightarrow f(n)\prec_\alpha f(m)\right)$.Your answer does not clarify these things. Could you please clarify why your answer provide these things? Also please write your answer in the notation of the question, please. $\endgroup$
    – Erfan Khaniki
    Commented Sep 30, 2017 at 20:17
  • $\begingroup$ @ErfanKhaniki Formally, $P$ and $P'$ are predicates on codes (i.e. natural numbers), but once one fixes an ordinal notation system, they are naturally viewed as predicates on ordinals. Here is an equivalent description that emphasizes codes rather than ordinals. Define Succ(n) as the '≺'-successor of $n$, and Fin and Inf such that $n = \mathrm{Succ}^{\mathrm{Fin}(n)}(\mathrm{Inf}(n))$ with rng(Inf)∩rng(Succ)=∅. Set $f(n) = \mathrm{Succ}^{(2^{\mathrm{Fin}(n)}+1) 2^{\mathrm{Inf}(n)}}(\mathrm{Inf}(n))$. [...] $\endgroup$
    – Dmytro Taranovsky
    Commented Sep 30, 2017 at 22:19
  • $\begingroup$ @ErfanKhaniki For ordinal representation systems that use (for example) Cantor Normal Form (with a reasonable coding of pairing and natural numbers), rng($f$) and $f^{-1}$ are polynomial time computable, with $f^{−1}$ growing logarithmically. $\endgroup$
    – Dmytro Taranovsky
    Commented Sep 30, 2017 at 22:19

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .