Well-foundedness of Cauchy construction of ℝ

Stream: new members

[Lars Ericson]

I watched a video in which Norman Wildberger expresses some anxiety about construction of real numbers as equivalence classes as Cauchy sequences. He says it's shaky ground but he doesn't seem to get down to brass tacks in the video, just some bullet points.

nLab on the other hand seems to be comfortable that the construction can be defined from first principles without assuming ℝ to begin with, just ℕ and ℚ. That is, the construction is not tautological.

Lean uses Cauchy sequences.

This is not an urgent how-do-I-do-this-in-Lean topic, but if it is a standard controversy with a standard answer, I'd be curious to know.

[Kevin Lacker]

that PDF link doesn't appear to express any anxiety, it's just doing standard real number construction stuff

[Kevin Lacker]

i don't really want to watch a half hour video to figure out the claim though. I don't think there's a standard controversy here, I think this is pretty well accepted. can you summarize what seems shaky to him or to you?

[Johan Commelin]

Lars Ericson said:

This is not an urgent how-do-I-do-this-in-Lean topic, but if it is a standard controversy with a standard answer, I'd be curious to know.

There is no controversy.

[Johan Commelin]

What does happen, is that may universities don't define the reals at all, but just start their Calculus and Analysis courses with an axiomatic approach to the reals.
A construction of the reals may then appear as an appendix, or maybe in a later course that introduces metric spaces etc...

[Mario Carneiro]

NJ Wildberger is an ultrafinitist, he doesn't believe in infinite sets (or even very large finite sets/numbers), so cauchy sequences look a little magic and philosophically unjustified from that perspective. The constructivist solution is to talk only about computable sets and sequences, which are enumerable and hence easier to make "tangible"

[Mario Carneiro]

Alternatively, there is the formalist response (here formalist is referring to the philosophical position, although I think it accords well with formalized mathematics), in which all we are doing is playing a game with symbols, in which case we can use whatever infinite sets we like because they are just notations and we aren't asserting any "real" "existence" of infinite sets, whatever that means.

[Kevin Lacker]

formalism is the best philosophy here. -1 doesn't "really exist", it's just sooo convenient for like, accounting when someone owes me a dollar, life is better when we just go along with it

[Mario Carneiro]

I'm a formalist who pretends to be platonist when I want to get things done

[Johan Commelin]

I'm a platonist who pretends to be a formalist when I want to get things done (say in Lean)

[Johan Commelin]

I know that the type real in mathlib is not the real "real numbers" (you know, the ideal one... whose shadow you can see in some cave), but I just pretend that it is.

[Patrick Massot]

Lars Ericson said:

Lean uses Cauchy sequences.

mathlib has two independent constructions of real numbers (and an isomorphism between those constructions). Of course none of them is circular. The key point for Cauchy sequences is that you get to choose the target of the absolute value. While constructing real numbers you need to use an absolute value on rational numbers with rational values.

[Riccardo Brasca]

Which is the second construction?

[Riccardo Brasca]

Found it! topology.uniform_space.compare_reals

[Patrick Massot]

Yes, the other construction is Bourbaki reals (which are the real ones of course). I avoids the psychological hurdle of doing Cauchy sequences twice, one before constructing reals and one after. I also places real numbers in the broad context of completions of topological rings.

[Lars Ericson]

Thanks for discussing this and thank you @Mario Carneiro for putting a name to it. Ultrafinitism it is. I guess it was popular from 1959 to 1961.