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.