2
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ 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. $\endgroup$ Jan 16, 2014 at 21:52
  • $\begingroup$ @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. $\endgroup$ Jan 17, 2014 at 3:05

1 Answer 1

1
$\begingroup$

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?

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.

$\endgroup$
2
  • $\begingroup$ What do you mean by "So the least upper bound principle does not do much for us in that language."? The LUB axiom schema is equivalent to the intermediate value theorem for polynomials. It's just different ways of axiomatizing the theory of real closed fields. $\endgroup$ Jan 17, 2014 at 4:15
  • 1
    $\begingroup$ Also, is $RCA_0$ the weakest subsystem that can prove the axioms of real closed fields? Can $RCA_0^*$ do it? $\endgroup$ Jan 17, 2014 at 4:25

You must log in to answer this question.

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