5 ms·
Coming from the mathematics side of things, > In a math class, we typically tell students that ℕ is a set. I think the approach is a bit glib. There are some
by klodolph 5y ago
Coming from the mathematics side of things,
> In a math class, we typically tell students that ℕ is a set.
I think the approach is a bit glib. There are some caveats—a student with more mathematical experience would think of ℕ as a set, or a type, or as objects in various categories.
It’s also worth asking a student what 1∪2 is. Most people will look at that and just tilt their head, even though common foundations for mathematics treat 1 and 2 as sets. It turns out most people don’t want to work in foundations, and want to think of 1 and 2 as non-sets. The same applies in the other direction, upwards, when you think of ℕ as a type (even though it is also a set).
- vkazanov 5y agoMy math is shallow at best but... 1∪2 would become just 2 with integers represented as sets in certain foundational theories, right?
- hansvm 5y agoYes. One common definition is equivalent to each natural to being the set containing all preceding naturals. With that view 2={0,1} and 1={0}, so their union is just 2.
- Spivak 5y agoYep! But notation depends a lot on the author to some extent. You will find people who treat 1U2 as {1}U{2} because it’s less annoying to write. It’s the same reason languages have an .add method on sets so you don’t have to write. s = s.union(set(s))
- deleted 5y ago[deleted]
- alisonkisk 5y agowho writes 1U2 instead of {1,2} ? When would {1}U{2} ever appear in ant context except for the first day of Intro to Set Theory?
- jdmichal 5y agoI assume 1 and 2 are placeholders here... Not literally meant.
- lapinot 5y ago> It turns out most people don’t want to work in foundations, and want to think of 1 and 2 as non-sets Which is to say most mathematicians prefer type theory to set theory :). Perhaps we should stop saying "maths is usually done in ZFC", or that "ZFC is mainstream math". For one math is almost never formalized and second informal math is quite strongly typed (the basic object usually not a set but a structured set) where set theory is very untyped. At some point people (erm mathematicians) have to acknowledge that we computer sciency-math have brought far better foundations (being intuitionistic type theory) insofar that it has set theory as a subpart, but is much finer in what it can distinguish. It's newtonian mechanics vs general relativity. What set-foundationalists say is fine, but the frontier is elsewhere.
- creata 5y agoHow is intuitionistic type theory a "better" foundation? As a simple example, where can I find a statement of Brouwer's fixpoint theorem in an intuitionistic type theory, and how is it better stated than its classical counterpart?
- lapinot 5y ago:) i don't know about that theorem, don't remember having seen. Now i'm reading stuff about Brouwer! Since it seems to be about topology so i'd guess homotopy type theory folks would have written something about it. edit: You seem to know some stuff apparently?
- Tainnor 5y ago> For one math is almost never formalized and second informal math is quite strongly typed [...] I think you're correct about the first part, but not about the second. It is incredibly common in mathematics to silently "convert" objects between different types or to ignore certain things that will trip you up once you try to encode things super formally. For example, "the function x^2" (instead of x->x^2), basically all the common notational shorthands in differential equations, where functions are treated as variables, silently identifying isomorphic objects and so on. Plus, very few working mathematicians actually use constructivism and are quite happy with the existence of, for example, the whole set of real numbers.