3 ms·
> the very definition of what the real numbers are I wonder what that was. (In my world it was just a bunch of axioms.)
by Koshkin 5y ago
> the very definition of what the real numbers are
I wonder what that was. (In my world it was just a bunch of axioms.)
- siraben 5y agoIt was given axiomatically, with classical set theory as the foundation. Define the reals as a complete, ordered field. In fact it can also be proven that any two complete ordered fields are isomorphic. From this you can prove various cancellative, associative and distributive laws and obvious things like 0 < 1. See[0] for a readable Coq formalization. [0] https://www.cs.umd.edu/~rrand/vqc/Real.html https://www.cs.umd.edu/~rrand/vqc/Real.html
- subset 5y agoThere are also set-theoretic constructions of the Reals that satisfy the axioms (e.g. Dedekind cuts)