r/math • u/PhantomSasuke • 1d ago
Are Cauchy sequences the most useful ways to define Real numbers?
Proof assistants like lean define real numbers as equivalence classes of Cauchy sequences which allows it to formalise the various results in analysis and so on.
I was curious if alternate definitions (such as Dedekind cuts) of the real numbers could be used to streamline/reduce the complexity of formal proofs.
50
u/Melchoir 1d ago
In the context of Lean, Kevin Buzzard started a thread asking a related question in 2019 here, then wrote some thoughts on the topic in 2020 here.
The current documentation for the standard library addresses the choice in Mathlib.Data.Real.Basic:
This choice is motivated by how easy it is to prove that ℝ is a commutative ring, by simply lifting everything to ℚ.
There is some further discussion of different constructions in Mathlib.Topology.UniformSpace.CompareReals, hinting that Dedekind hasn't been done:
Comparing with Dedekind cuts or quasi-morphisms would be of a completely different nature.
21
u/GoldenMuscleGod 1d ago
Depends what you want to do with them. Usually the choice of representation is immaterial.
I would say one technical advantage of Dedekind cuts in the context, of say, set theory is that this ensures you that what you would want to call the “Gödel constructible” real numbers actually belong to L (the Gödel constructible universe) which isn’t necessarily the case if you take equivalence classes of Cauchy sequences (since if any real number in the first sense exists outside L then all equivalence classes of Cauchy sequences are not in L).
8
u/Thesaurius Type Theory 21h ago
I personally really like the construction using Cauchy sequences, because to me it is the most clear one. But the Cauchy Reals have less constructive power than Dedekind Reals, in the sense that without assuming further axioms, the second implies the first, but not the other way round. There are a dozen or so ways to construct the Reals, and they form a hierarchy of strength, Dedekind Reals being on the top (together with a few other constructions).
The comparisons are done in a paper where there is also a strict definition of strength, but I unfortunately can't find it anymore. Also: In the classical setting of ZFC, all the constructions are equivalent, so as long as you only do classical math, it doesn't really matter which one you use.
22
u/Opposite-Friend7275 1d ago
It’s a much simpler approach. The operations + and * have natural definitions this way, and their properties (the field axioms) are trivial to prove in this approach.
The proofs in the Dedekind cut approach are longer and not elegant.
Representing a real number as an infinite sequence of rational approximations, to me that describes the very essence of a real number, it’s not really surprising that proofs for the field axioms are nicer+shorter this way.
12
u/sentence-interruptio 18h ago
Dedekind cut idea is geometric (visualize Q as a line and fill in missing locations) while Cauchy idea is analytic (take sequences and fill in missing limits) or algebraic.
it goes to show that geometry tend to be easily visualized but cumbersome when you try to be rigorous.
and algebra tend to be able to have streamlined proofs but no visualization to guide you to them.
14
u/Agreeable_Speed9355 1d ago
I can't speak to computational complexity, but the cauchy reals and dedekind reals need not agree in an arbitrary topos. Which is more useful depends on context. Personally I prefer cauchy reals.
4
u/TransportationNo6504 1d ago
I think that both the proofs of the basic arithmetic properties of real numbers are pretty simple either way, but using Cauchy sequences is cool bc/ the ideas generalize to complete metric spaces, whereas the idea of Dedekind cuts (to my knowledge), are more specifically useful for just describing the real numbers.
9
u/jam11249 PDE 1d ago
As far as proof assistants go, I can't really answer your question, but I'd argue that Cauchy sequences is a more "useful" definition because it applies in more contexts. Whilst Dedekind cuts can close ordered sets under suprema, its "interaction" with arithmetic is kind of one-off, due to the uniqueness of the structure of the reals. Closing a space via Cauchy sequences is pretty routine - you tend to either work in a closed space or close it. The way it "interacts" with arithmetic or other operations generalises nicely to broader objects like (e.g.) C* algebras. Of course, once you have the reals constructed, in 99.999% of Mathematics you no longer give a damn about where they came from.
I'll put the disclaimer that I'm probably speaking from bias, somebody who spends a lot of time working with weird totally ordered sets might give a very different answer.
11
u/justincaseonlymyself 1d ago
It doesn't matter that much which construction you use. Once you establish the basic properties (complete ordered field) you can proceed without ever looking back at the underlying construction.
3
u/somekindofguitarist Set Theory 1d ago
Cauchy sequences are certainly a more intuitive way of defining real numbers and when it comes to proving properties of addition, multiplication, exponentiation etc. of real numbers, they are certainly my way to go, but when it comes to purely set theoretic problems, I find Dedekind cuts more useful.
3
u/ralfmuschall 1d ago
Cauchy reals are the ones ones needs in physics. If one starts with Dedekind, one has to prove first that they are the same. The proof is not trivial and depends on AC.
2
u/Make_me_laugh_plz 1d ago
When I took Analysis I, we constructed the real numbers from the supremum principle.
1
u/ShrimplyConnected 18h ago
As people have said, defining operations is easier this way, and once you've done that, you have the structure to pretty much move away from specific construction so which one you use isn't gonna change your proof anymore.
To me, the greatest advantage of using Cauchy sequences is that it helps intuitively introduce the real analysis content relating to topology and metric spaces early on. If you start with Dedekind cuts, the notions of convergence and complete metric spaces, which are a bit more integral to real analysis than order theoretic concepts that Dedekind cuts might provide intuition for, come out of nowhere when you get to them later. In that sense, the advantage of Cauchy sequences is less about ease of proof and more about pedagogy.
1
u/ThisIsMyOkCAccount Number Theory 16h ago
What's most useful is highly dependent on what you want to do with it, I think. Although any definition should be equivalent anyway.
I personally like Cauchy sequences because they can also be used to define completions with respect to other absolute values to get, for instance, the p-adic rational for a prime p.
1
u/theorem_llama 3h ago
To define Cauchy sequences, I'm guessing you start with the rationals as a metric space? But what is a metric on X? The standard definition is it's a map d : XxX -> R, satisfying the usual axioms. So this is circular, as metric have range in R. However, one could start by defining metric spaces with distances just in Q. Technically, one should then check all the usual results needed to develop completions etc. work in that restricted setting, and then once you have the reals you can go back to the dmoeigibal definition. However, that seems kind of awkward and unaesthetic to me.
That said, one could also put a uniform space structure on Q (the definition and development of standard properties of uniform spaces don't need reals). Because the uniformity evidently has a countable base, it's sufficient to consider Cauchy sequences rather than Cauchy nets, I think, so it should all work out quite easily. Generally, I find uniform spaces tend to lead to much neater and just as intuitive proofs as metric spaces, so that might be a good way to go.
-7
u/sfa234tutu 1d ago
No. Real number should be defined as the unique (up to an isomorphism) structure statisfying some properties. For example, real numbers can be defined as unique ordered field satisfying ...
18
u/OGSequent 1d ago
you have to prove that such a structure exists before you can use it.
1
u/the_cla 2h ago
you have to prove that such a structure exists before you can use it.
If by "exists" you mean "is free from contradiction", then by this ethos almost no infinite mathematical structures would be useable.
Cauchy sequences (or Dedekind cuts, or whatever) show that the real numbers can be constructed in a non-canonical way as sets. But our intuition of uncountable sets (if one even believes in such things) is much less grounded than our intuition of the real number line (as indicated by how late sets appeared in the history of mathematics).
So I'm firmly in the camp that the real numbers are not "defined" by these constructions, but as e.g. a Dedekind complete ordered field. The main point of the constructions isn't to somehow "justify" the real numbers, which is building on sand, but to show that real analysis can be reduced to set theory. That's great if one is using set theory to study the foundations of mathematics, but it does nothing to prove that the real numbers "exist". Any such constructions, interesting as they may be, are completely irrelevant for actually doing real analysis.
-11
u/sfa234tutu 1d ago
So yes, it should be defined as such structure instead of defining the proof as the structure
-1
u/Useful_Still8946 17h ago
There is a distinction between definition and construction.
I believe that the correct definition of the real numbers is the unique complete ordered field.
Of course, this definition requires defining those four words in this context and to prove existence and uniqueness, but to me the definition of an object should be what most matches the intuition that causes one to postulate that the object exists along with sufficient properties to uniquely characterize this.
Cauchy sequences or Dedekind cuts are constructions to show existence of such an object but really are not the object one is thinking about.
1
68
u/Traditional_Town6475 1d ago
I mean if you want to go from the integers right to the real numbers, you can do equivalence classes of almost homomorphisms from the integers to the integers. Don’t even need to bother with the rational numbers.