6
$\begingroup$

A recursive ordinal is an ordinal that is the order-type for some recursive relation (i.e. a recursive well-ordering). We can represent recursive ordinals as natural numbers using Kleene's $O$, an ordinal notation system. Unfortunately, the set of natural numbers which are in Kleene's $O$ is not recursive, or even recursively enumerable. And it is not effectively decidable whether two numbers represent the same ordinal or not.

But suppose you had an oracle $M$ which could tell what precisely numbers are notations in Kleene's $O$, and whether two numbers represent the same ordinal. Let $O'$ be the set of equivalence classes of elements of Kleene's $O$, under the equivalence relation of two numbers representing the same ordinal. Let us enumerate (or code) all recursively axiomatized theories with natural numbers, so that $T_n$ represents the $n^{th}$ such theory. Then let us define a function $f$ from the set of natural numbers to $O'$ as follows: $f(n)$ is the element of $O'$ corresponding to the proof-theoretic ordinal of the theory $T_n$. (The proof-theoretic ordinal of a theory is the least ordinal that the theory cannot prove the well-foundedness of.)

My question is, does there exist a Turing machine which, given access to the oracle $M$, can compute the function $f$? To put it another way, if a computer program knew exactly what recursive ordinals there were, could it find the proof-theoretical ordinal of all recursively axiomatizable theories? If the answer is no, as I suspect it may be, what other oracle do you require to do this?

Any help would be greatly appreciated.

Thank You in Advance.

$\endgroup$

1 Answer 1

Reset to default
3
$\begingroup$

I think that the answer you want is "yes, once you make it rigorous". For example, if we are talking about theories of second-order arithmetic then it is clear what "T proves that index $e$ computes a well ordering" will mean. For theories of first-order arithmetic, the definition is more subtle, but for example it might mean that $T$ proves a certain axiom scheme that represents transfinite induction up to $e$, or $T$ proves some other axiom scheme.

In any case, the following will apply as long as "T proves that index $e$ computes a well ordering" means that $T$ proves some (possibly infinite) set of sentences that is uniformly r.e. given the index $e$; we will call the set $S(e)$.

There is another caveat that I am more nervous about. You are talking about arbitrary indices for computable well orderings. Usually, when we do ordinal analysis, we look at particular "nice" indices, which compute the well order in a nice way. It is known that there are various tricks that one can do with indices to hide what they are doing. For example, there is an index $e$ that really computes an order of type $\omega$, but Peano Arithmetic does not prove that the order computed by $e$ has a least element. So does that mean, in your setup, that the least ordinal that PA cannot prove to be well founded is $\omega$?

So, really, statements that claim to identify the proof-theoretic ordinal have to be understood as informal interpretations of particular results, rather than being statements about a formal definition of "proof theoretic ordinal". See https://mathoverflow.net/questions/52926/proof-theoretic-ordinal/52927#52927

I am going to ignore that temporarily, and give an answer in the spirit of the question, because it shows a key fact about $\mathcal{O}$. But I am not convinced that the thing that is being found is really "the proof theoretic ordinal of $T$".

Now I will proceed to the construction. Given an index $t$ for $T$, the statement "For every $i \in S(e)$, $T$ proves the sentence with Goedel number $i$" can be written as an arithmetical formula $\phi(t,e)$, where the same formula $\phi$ works for all $t$ and $e$. Basically, $\phi$ says: whenever $e$ enumerates a formula $i$, there is a formal proof of that formula from the set of axioms enumerated by $t$.

Thus there is also an arithmetical formula $\psi(t,e)$ which says that $e$ computes a linear order of $\omega$, and $\phi(t,e)$ does not hold but, for every $e' <_e e$, $\phi(t,e')$ does not hold. The last part quantifies over every proper initial segment of the ordering computed by $e$. Note that if $e$ actually computes a well ordering, then $\psi(t,e)$ holds if and only if the order type of $e$ is (in some imprecise sense, but I think the one you mean) the "proof theoretic ordinal of $T$."

The index $\mathcal{O}$ is very strong. In particular, given any arithmetical formula, we can use $\mathcal{O}$ to tell whether that formula is true or false. Formally, this is the fact that $\emptyset^{(\omega)} <_T \text{HJ}(\emptyset) = \mathcal{O}$. Now, given $t$, we can do the following: enumerate all values of $e$. For each one, first ask whether $e \in \mathcal{O}$. If not, move on to the next value of $e$. If $e \in \mathcal{O}$, ask whether $\psi(e,t)$ holds. If so, we have found the ordinal for $t$. Otherwise, move on to the next value of $e$. This will find some sort of "proof theoretic ordinal" $e$, subject to my caveat above.

$\endgroup$
5
  • $\begingroup$ What if you defined the proof-theoretic ordinal as follows: the least ordinal $\alpha$ such that $PRA$ + quantifier-free transfinite induction up to $\alpha$ proves $Con(T)$? $\endgroup$
    – Keshav Srinivasan
    Commented Oct 6, 2013 at 19:23
  • $\begingroup$ That is still an arithmetical property of an index of $\alpha$, so the same method would apply, with the same caveat. The real situation with proof theoretical ordinals is that "you know it when you see it", but trying to make a very precise definition is difficult because of strange counterexamples. So it is still an informal notion. $\endgroup$
    – Carl Mummert
    Commented Oct 6, 2013 at 20:00
  • $\begingroup$ Why would the same caveat apply? For instance, is there a set of indices for the ordinals less than $\epsilon_0$ such that $PRA$ + quantifier-free transfinite induction using those indices does NOT prove $Con(PA)$? $\endgroup$
    – Keshav Srinivasan
    Commented Oct 6, 2013 at 22:25
  • 1
    $\begingroup$ You could make an index $e$ so that $|e|$ is really $\omega$, but the induction scheme for induction on $e$ implies Con(PA) over PRA. The issue is that the computation of the ordinal may ask, at each step, whether it has seen a counterexample to Con(PA), and can then do something different (like become non-well-founded) if it sees one. If it becomes non-well-founded in a simple predictable way models where Con(PA) fails, then PRA should be able to disprove a specific instance of the induction scheme under the assumption that Con(PA) fails. $\endgroup$
    – Carl Mummert
    Commented Oct 6, 2013 at 23:32
  • $\begingroup$ IN particular, the order I have in mind is $0 < 1 < 2 < \cdots < n < \cdots < n+3 < n+2 < n+1$ if $n+1$ is the first number that is a counterexample to Con(PA). So under Con(PA) this order is just $\omega$ and when Con(PA) fails with minimal witness $n+1$ the order is $n + \omega^*$. So transfinite induction should not hold for this order unless Con(PA) holds; the instance that should fail is $\phi(m)$ that says "for all $n < m$, $n$ is not a counterexample to Con(PA)". It is the case for this order that $(\forall b)[(\forall a <_e b)[\phi(a)] \to \phi(b)]$. $\endgroup$
    – Carl Mummert
    Commented Oct 6, 2013 at 23:34

You must log in to answer this question.

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