3 ms·

> Real analysis, with heavy use of infinite sets, I never dove all the way into this, but I always found one detail unsatisfying: the natural numbers as define

by amluto 4y ago

> Real analysis, with heavy use of infinite sets, I never dove all the way into this, but I always found one detail unsatisfying: the natural numbers as defined by Peano arithmetic, and more generally the kind of sets described in the OP, are sets all the way down. Each element is itself a set consisting, recursively, of sets. The system has no types! But Cauchy sequences, and limit sequences, aren’t sets all the way down, nor are they things that grew out of untyped lambda calculus. They are sequences, not sets. And their elements are real numbers, not sets. Sure, a real number may well be describable as itself being a Dedekind cut over the rational numbers, which are themselves describable using Peano arithmetic. But you can do calculus using the axioms of the real numbers and treat the real numbers as their own type of object. The result seems much cleaner to me - a real number is equivalent to a Dedekind cut, but this does not mean that a real number is a Dedekind cut. A set of reals is not sets all the way down. An object of type Integer in most programming languages is not implicitly convertible to Set. Putting types into a model of mathematics seems to add a very welcome firewall between algebraic structures (like the reals) and the underlying formalism that was used to justify their existence and properties. In this context, of course infinite sets exist. The set of distinct real numbers in a sequence of reals converging to given irrational number is (countably) infinite. This infinity is firewalled off from the axiom of infinity, and it is infinite all by itself, which is amazing because I can take a limit or calculate a derivative without thinking about ZF at all! (The problems in the world are not all solved like this. Calculus certainly involves measures, and the Banach-Tarski paradox works on sets of reals, etc. But I don’t have to worry about Banach-Tarski when integrating a function.)

klodolph 4y ago
> They are sequences, not sets. I get what you are trying to say here. If we were talking only about calculus, it would be a reasonable thing to say. In this context, we are talking about calculus in connection with its set theory foundations, and so this statement, in context, is simply incorrect. Imagine I dropped a tomato on the floor and called you in to help me clean up a “chemical spill”. You’d say that’s not a chemical spill, that’s a tomato. On any other day of the year you would be correct, but today we are in chemistry class, talking about how ordinary matter is made of chemicals. Today you are wrong, because we are in chemistry class, talking about what tomatoes are made of. > Putting types into a model of mathematics seems to add a very welcome firewall between algebraic structures (like the reals) and the underlying formalism that was used to justify their existence and properties. The firewall only works if the underlying structure is sound. People have, historically, spent enormous amounts of time working with mathematical objects that turned out to be trivial, turned out not to exist at all, or had contradictions. For that reason, real mathematicians spend some time fussing about proving that the real numbers exist using set theory, before they turn around and work with exactly that firewall that you’re discussing. In upper-level undergrad courses, you’ll be expected to do this. (At least, I was asked to do this in undergrad.) Again, today, the topic of discussion is the axiom of infinity. If I ask, “how would we do calculus without infinite sets,” we need to revisit the set-theoretic construction of real numbers and calculus before we can put that firewall back into place. > But I don’t have to worry about Banach-Tarski when integrating a function. Unfortunately, the Banach-Tarski paradox is exactly the kind of paradox you must worry about when integrating functions. In a loose sense, what the paradox shows is that you cannot cut up a function you want to integrate, rearrange the pieces, and then integrate the result. For a long time, mathematicians had all sorts of incorrect beliefs about calculus. For example, “a continuos function defined on an open interval is differentiable at some point on the interval”. These incorrect beliefs didn’t disappear overnight. We created a rigorous foundation for calculus on a carefully-crafted list of set theory axioms (ZFC) and slowly rooted out the incorrect beliefs with proofs and counterexamples. It’s worth asking whether ZFC is the foundation we want for calculus. Maybe it’s time to adjust the foundations. Maybe you think—what if I had a version of calculus that didn’t have non-measurable sets? Working backwards from that idea, what axioms would I need in order to still get work done?

by amluto 4y ago

klodolph 4y ago

> They are sequences, not sets. I get what you are trying to say here. If we were talking only about calculus, it would be a reasonable thing to say. In this context, we are talking about calculus in connection with its set theory foundations, and so this statement, in context, is simply incorrect. Imagine I dropped a tomato on the floor and called you in to help me clean up a “chemical spill”. You’d say that’s not a chemical spill, that’s a tomato. On any other day of the year you would be correct, but today we are in chemistry class, talking about how ordinary matter is made of chemicals. Today you are wrong, because we are in chemistry class, talking about what tomatoes are made of. > Putting types into a model of mathematics seems to add a very welcome firewall between algebraic structures (like the reals) and the underlying formalism that was used to justify their existence and properties. The firewall only works if the underlying structure is sound. People have, historically, spent enormous amounts of time working with mathematical objects that turned out to be trivial, turned out not to exist at all, or had contradictions. For that reason, real mathematicians spend some time fussing about proving that the real numbers exist using set theory, before they turn around and work with exactly that firewall that you’re discussing. In upper-level undergrad courses, you’ll be expected to do this. (At least, I was asked to do this in undergrad.) Again, today, the topic of discussion is the axiom of infinity. If I ask, “how would we do calculus without infinite sets,” we need to revisit the set-theoretic construction of real numbers and calculus before we can put that firewall back into place. > But I don’t have to worry about Banach-Tarski when integrating a function. Unfortunately, the Banach-Tarski paradox is exactly the kind of paradox you must worry about when integrating functions. In a loose sense, what the paradox shows is that you cannot cut up a function you want to integrate, rearrange the pieces, and then integrate the result. For a long time, mathematicians had all sorts of incorrect beliefs about calculus. For example, “a continuos function defined on an open interval is differentiable at some point on the interval”. These incorrect beliefs didn’t disappear overnight. We created a rigorous foundation for calculus on a carefully-crafted list of set theory axioms (ZFC) and slowly rooted out the incorrect beliefs with proofs and counterexamples. It’s worth asking whether ZFC is the foundation we want for calculus. Maybe it’s time to adjust the foundations. Maybe you think—what if I had a version of calculus that didn’t have non-measurable sets? Working backwards from that idea, what axioms would I need in order to still get work done?