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.
Thank You in Advance.
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.
Separately, remember that the real line is o-minimal: any definable subset is actually a finite union of points and intervals. This is regardless of the complexity of the defining formula, so long as the formula is in the language of real closed fields with parameters. So the least upper bound principle does not do much for us in that language.