# What subsystem of second-order arithmetic can interpret the theory of real closed fields?

Real numbers can be encoded as sets of natural numbers, because they can be encoded as Dedekind cuts or Cauchy sequences of rational numbers, and a rational number can be encoded by a natural number. Thus any first-order statement about real numbers can be translated into a statement of second-order arithmetic.

So it's natural to ask, how much of second-order arithmetic do you need to interpret the standard first-order theory of real numbers, i.e. the theory of real closed fields? What is the subsystem of second-order arithmetic required to do this? I imagine it would be an impredicative subsystem, since a lot of instances of least upper bound schema would presumably not be predicatively justifiable. So perhaps we need something stronger than $ATR_0$?

Any help would be greatly appreciated.

• There are countable real closed ordered fields. For example, one can be obtained by taking any countable elementary submodel of the reals. The least upper bound property is not part of the axioms for a real closed field. Jan 16, 2014 at 21:52
• @CarlMummert Yes, I know that there are countable real closed fields (e.g. the algebraic reals); when did I say anything otherwise? And you're right that the second-order LUB axiom is not part of the theory of the real closed fields, but I was talking about the first-order LUB axiom schema, not the second-order LUB axiom: for any formula phi(x) in the first-order language of ordered fields, there is a least upper bound for the elements that satisfy phi(x). That's just another way of saying that we assume all the first-order consequences of the second-order LUB axiom. Jan 17, 2014 at 3:05

The weak subsystem $\mathsf{RCA}_0$ proves that the real numbers satisfy the axioms of a real-closed ordered field. These are simply the axioms of an ordered field and the intermediate value theorem for polynomials.
• Also, is $RCA_0$ the weakest subsystem that can prove the axioms of real closed fields? Can $RCA_0^*$ do it? Jan 17, 2014 at 4:25