4 ms·

There are various ways to construct real numbers and complex numbers. One approach is given in Landau's Foundations of Analysis (a.k.a. Grundlagen der Analysis)

There are various ways to construct real numbers and complex numbers. One approach is given in Landau's Foundations of Analysis (a.k.a. Grundlagen der Analysis). You might want to look at the Metamath Proof Explorer materials on constructing numbers, a good starting point is here: http://us.metamath.org/mpeuni/mmcomplex.html http://us.metamath.org/mpeuni/mmcomplex.html Metamath is a general tool that lets you specify axioms and proofs, and verifies that the proofs only depend on axioms and previously proved proofs. The Metamath Proof Explorer (MPE) is a particular application of it that uses classical logic and the ZFC set theory axioms. MPE shows how to construct numbers using these axioms, then proves a set of number axioms, and from then on uses only those axioms so that the details of any particular construction are not important. What's usually more important is showing that you can construct them.

andi999 5y ago
Cool link. I know some construction of the real and complex numbers, I was asking about the construction of the hyperreals used in the textbook. I couldnt find info about that on the page.
- Smaug123 5y ago
  The construction is fairly easy but requires some fairly hefty background knowledge to make formal. In brief, though: an ordinary real number can be implemented as a sequence of rational numbers, with two sequences considered to be "the same" if they eventually get, and stay, arbitrarily near to each other. A hyperreal can be implemented as a sequence of real numbers, with two sequences considered to be "the same" if they are equal at "very many places", for a certain strict and formal definition of "very many places". (Formally, fix a nonprincipal ultrafilter on the naturals; then the requirement is that the sequences be equal on a set of indices which is a member of that ultrafilter.) A standard real z can be viewed as a hyperreal, by taking that sequence to be z, z, z, …. Another equivalent representation of that same hyperreal would be the sequence 0, z, z, z, … because that's equal to the first sequence in "very many places". There's an infinite hyperreal, implemented by the sequence 1, 2, 3, …. (In fact there are tons and tons of infinite hyperreals.) You can prove that the space of hyperreals is a field, and moreover with some model theory you can show that actually a lot of structure (in fact, all first-order structure) transfers directly over to the hyperreals from the reals.
  - andi999 5y ago
    Very cool, thank you. Do you know what happens to measure theory in the hyperreals? Or integration in general?
    - Smaug123 5y ago
      I don't know much about it, I'm afraid. But there is the very cool fact that the usual Riemann integral can be written as basically just a sum in nonstandard analysis; it's covered very neatly in André Pétry, "Analyse Infinit́esimale: une présentation non standard" which is very readable. There's a lot more advanced stuff, including Brownian motion and (I think) some integration, in Hurd and Loeb, "An Introduction to Nonstandard Real Analysis". For the foundations of nonstandard analysis, and a wide-ranging overview, I strongly recommend Robert Goldblatt, "Lectures on the Hyperreals: an Introduction to Nonstandard Analysis", one of the Graduate Texts in Mathematics.
    - ska 5y ago
      I'm rusty, but did think about this a bit at one point. I recall you can't really do the usual constructions on hyperreals (problems with completeness?) but you can do something like approximate any real-valued measure closely.

andi999 5y ago

Cool link. I know some construction of the real and complex numbers, I was asking about the construction of the hyperreals used in the textbook. I couldnt find info about that on the page.

Smaug123 5y ago
The construction is fairly easy but requires some fairly hefty background knowledge to make formal. In brief, though: an ordinary real number can be implemented as a sequence of rational numbers, with two sequences considered to be "the same" if they eventually get, and stay, arbitrarily near to each other. A hyperreal can be implemented as a sequence of real numbers, with two sequences considered to be "the same" if they are equal at "very many places", for a certain strict and formal definition of "very many places". (Formally, fix a nonprincipal ultrafilter on the naturals; then the requirement is that the sequences be equal on a set of indices which is a member of that ultrafilter.) A standard real z can be viewed as a hyperreal, by taking that sequence to be z, z, z, …. Another equivalent representation of that same hyperreal would be the sequence 0, z, z, z, … because that's equal to the first sequence in "very many places". There's an infinite hyperreal, implemented by the sequence 1, 2, 3, …. (In fact there are tons and tons of infinite hyperreals.) You can prove that the space of hyperreals is a field, and moreover with some model theory you can show that actually a lot of structure (in fact, all first-order structure) transfers directly over to the hyperreals from the reals.
- andi999 5y ago
  Very cool, thank you. Do you know what happens to measure theory in the hyperreals? Or integration in general?
  - Smaug123 5y ago
    I don't know much about it, I'm afraid. But there is the very cool fact that the usual Riemann integral can be written as basically just a sum in nonstandard analysis; it's covered very neatly in André Pétry, "Analyse Infinit́esimale: une présentation non standard" which is very readable. There's a lot more advanced stuff, including Brownian motion and (I think) some integration, in Hurd and Loeb, "An Introduction to Nonstandard Real Analysis". For the foundations of nonstandard analysis, and a wide-ranging overview, I strongly recommend Robert Goldblatt, "Lectures on the Hyperreals: an Introduction to Nonstandard Analysis", one of the Graduate Texts in Mathematics.
  - ska 5y ago
    I'm rusty, but did think about this a bit at one point. I recall you can't really do the usual constructions on hyperreals (problems with completeness?) but you can do something like approximate any real-valued measure closely.