# What is the proof-theoretic ordinal of the first-order theory of real closed fields?

I recently asked a question on MathOverflow, concerning a predicative second-order theory of real numbers. Now the standard way of developing predicativity in the case of second-order arithmetic is by using comprehension schemes indexed by certainn transfinite ordinals, starting with the set of ordinals less than $\varepsilon_0$, which is the proof-theoretical ordinal of first-order $PA$. So in order to carry out the same procedure for the real numbers, I would need to know the proof-theoretic ordinal of the first-order theory of real numbers, i.e. the theory of real closed fields.

In other words, I want to find out what transfinite ordinals can proven to be well-founded by the theory of real closed fields. It's possible the answer may be "none of them", because you can't even define "natural number" in the theory of real closed fields, so you may not be able to define any countable well-orderings. If that is the answer, then what if we go to a second-order theory of real numbers, but a very weak one: the axioms for ordered fields, plus the least upper bound axiom (AKA Dedekind completeness), plus a comprehension schema for only first-order formulas (i.e. formulas with no quantification over sets of real numbers)? This would be a theory similar to $ACA_0$, which has the full second-order induction axiom, but comprehension for only formulas that don't involve quantification over sets of natural numbers.

This theory may still be too weak to define any countable well-orderings, because the standard definition of natural number in the second-order theory of real numbers involves quantification over sets of real numbers: a natural number is defined to be a real number which belongs to all the hereditary sets that $0$ belongs to (or $1$ depending on where you start the natural numbers), where a hereditary set is a set which contains $n+1$ whenever it contains $n$.

Any help would be greatly appreciated.

EDIT: In the comments, @RobArthan pointed out that the sets definable in the first-order theory of real-closed fields are the semialgebraic sets, and semialgebraic sets have to be finite unions of points and intervals, so we can't really construct any countable sets, let alone countable well-orderings. So we can conclude that the first-order theory of real closed field can't prove the well-ordering of any transfinite ordinals, so its proof theoretic ordinal would simply be $\omega$.

So now my only remaining question is, what if we took the second-order theory of real numbers, i.e. the axioms for ordered fields along with the least upper bound or (Dedekind) completeness axiom, but we restrict comprehension to formulas without quantification over sets of real numbers? (This is analogous to restricting second-order $PA$ to $ACA_0$.) In that case, what transfinite ordinals, if any, could we prove to be well-founded?

• I don't know if it's relevant, but it may be worth noting that real closed fields are Dedekind complete, if you only allow cuts that can be defined in the language of real closed fields.
– user14972
Oct 2, 2013 at 20:46
• Yes, that's just another way of saying that the theory of real closed field consists of first-order consequences of the second-order theory of real numbers. Oct 2, 2013 at 22:24
• In the usual model-theoretic sense of the term "definable", the sets definable in the theory of real closed fields comprise precisely the semi-algebraic sets. Do you have some other notion of how the theory might "define" a countable well-ordering? Oct 6, 2013 at 13:42
• @RobArthan Is your definition of definability the same as being definable using a formula in the language of the first-order theory of real closed field? That's the definition that I would think makes sense. In any case, the question now becomes, how would you show that there are no countable well-ordered semialgebraic sets? Oct 6, 2013 at 18:25
• @KeshavSrinivasan: O-minimality: a 1-dimensional semi-algebraic set is a finite union of points and intervals, so (over an uncountable real closed field like $\mathbb{R}$) the only definable sets of field elements are either finite or uncountable. Oct 6, 2013 at 21:34