https://commons.lib.jmu.edu/cgi/viewcontent.cgi This is a neat attempt without assuming infinity a priori, but I think it falls flat in 2 (?) places. 1. the way they define a sequence as a static function between Z+ and Q means that they cannot ever arrive at any arbitrary real number. One example of a real number that they cannot converge to is any non-computable number, since that computable number would be representable as the computer program that iterated in a loop successive outputs, and there are an infinite number of reals that are not computable. They also contradict themselves in Example 10.1 by hand-waving what they mean by a sequence as the successive rational expansions of the square-root (sqrt) of 2. First, they never define sqrt, and second they don’t offer an explanation of the function that maps Z+ to expansions of sqrt(2) (or if one exists at all). This specific example is solvable, in that they could get a sequence that “diverges in Q” but is still cauchy by defining a power law, and using (1 + 1/n)^n) (a.k.e. e) but alas they didn’t do this. They still have no fundamental way of describing (let alone producing) non-computable numbers. 2. The completeness theorem in the appendix just says that any value can have a Cauchy sequence (I call them “Cauchies” bc I’m lazy) from above and below, and they are the “same” using their definition of a real number = cauchy sequence in rationals. This doesn’t show all reals are present, in the way they want to[^1], because it doesn’t show how any real could be arrived at, only that Cauchies can arrive at any number we know it can already arrive at either from above or below. To solve #1, I think we can do something slightly more clever in our definition of sequences. They can be “recursive” rather than just a static mapping from Z+->Q. If we want to get fancy we can add some computational concepts, but looking forward to discussing with folks about my criticisms before fleshing this out too far. [^1] To quote one part on page 51: “There are just “too many” reals to construct in this fashion. We need, essentially, to use equivalence classes on Q×Q×Q×. . . , which is what sequences of rationals really are, in order to get a set large enough to cover the reals”