Author: RupertRupert
Date: May 4, 2008 23:02
In SOSOA, pp. 74-6, we have
"Definition II.4.4 (the real number system). A real number is defined
in RCA_0 to be a sequence of rational numbers such that
AkAi(|q_k-q_(k+i)|<=2^(-k))... Remark: Note that we are taking
equality between real numbers (the = of definition II.4.4) to be an
equivalence relation other than true identity... One might consider
alternative definitions under which a real number would be an
equivalence class or a representative of an equivalence class. Both
alternatives turn out to be inappropriate. Equivalence classes would
require the language of third order arithmetic, and the use of
representatives would demand a strong form of the axiom of choice
which is not available even in full second order arithmetic, Z_2."
I'm having trouble seeing the last part of the last sentence. Surely I
can define a pi^0_1 relation "X is the representative of the
equivalence class of Y", where, if Y is a real number, then X is a
real number which is an increasing sequence of dyadic rationals. It
may be more convenient to use the definition given in the text for the
statement of theorems, but how could using the other definition
require any form of the axiom of choice?
| 
