Tangentially related question: how are real numbers formally defined?
I remember that integers are usually defined in terms of successors: Succ 1 = 2. But this doesn't help for real numbers because they can't really be enumerated?
I remember that integers are usually defined in terms of successors: Succ 1 = 2. But this doesn't help for real numbers because they can't really be enumerated?