7 ms·

Terence Tao wrote a blog post years ago dividing math education into 3 stages: pre-rigourus, rigourus, and post-rigorous. That distinction seems relevent here.

Terence Tao wrote a blog post years ago dividing math education into 3 stages: pre-rigourus, rigourus, and post-rigorous. That distinction seems relevent here. Every mathamatician knows that the integer 1 and the real number 1 different objects [0]. We could make every invocation of a canonical isomorphism explicit, but that would make all of math far too unwieldy to do. This is the core problem with formal proof verification. Current provers need you to prove things at such a low level that they are simply unwieldy to use. That does not mean we need to reinvent all of math. It means we need to improve formal verification tooling. Maybe we also need to train mathamaticians in formal verification systems. In much the same way that they had to be trained to use computer algebra systems. We didn't reconstruct all of math. We just learned how to work within the limitations of tools when we use those tools. [0] Unless you go out of your way to construct them to be the same thing. There is not actually any official definition of, for example, what the integer 1 is. Since so many definitions of it are equivalent, that is a fundamentally pointless conversation to have. A few textbook authors need to make a decision for pedalogical purposes. No one else cares.

auggierose 2y ago
I think pretty much every mathematician agrees that you can assume ℕ ⊂ ℤ ⊂ ℚ ⊂ ℝ ⊂ ℂ, and that 1 the integer is the same as 1 the real number.
- klodolph 2y ago
  You have to use a very funny notion of ⊂ for that to make sense. Mathematicians recognize that there is a lot of funny business going on behind the scenes… if you use the typical construction of these sets, then ℤ ⊂ ℚ is for sure false under the set-theoretic definition of what subsets are. So you are going to get a lot of funny explanations of why you can still say “ℤ ⊂ ℚ” and what that means. And what is “the same as” anyway?
  - hansvm 2y ago
    The typical construction is just to show that they _can_ be constructed. Once you have "primitive" integers, rationals, ..., you pick (for this finite example) the largest of them, and define the "integers" to be a subset with a certain property. That's also well-defined, and you find _exactly_ the same integers in the rationals and reals.
  - interroboink 2y ago
    Could you provide an example? I'm not seeing it. Is there some integer that is not also a rational number?
    - klodolph 2y ago
      How about this example: the natural number 0 is not a member of the integers, from a set theoretic perspective. In the natural numbers, 0 = {} However, {} is not an element of the integers. This is not something I expect to be easy to understand. This is the standard set theoretic definition of integers that mainstream mathematicians use. This is not some esoteric, fringe theory.
      - Affric 2y ago
        Isn’t the empty set a subset of all sets? A quick look at Wikipedia indicates that there exist other constructions.
        klodolph 2y ago
        Yes, the empty set is a subset of all sets. I think some wires got crossed somewhere because whether zero is a subset of some other set doesn’t fit into the questions we are trying to answer. You could pick a construction where the natural numbers are a subset of the integers. This is trivial, but this is a poor strategy overall, because you can always find a bigger set of numbers to work with. You can’t take the “biggest” set of numbers and then define all other sets of numbers as subsets of that. It would be kind of like trying to count down from infinity.
        Affric 2y ago
        I see where I have gone wrong. Element vs subset. Classic error when thinking fast. Thank you for the thought provoking comments.
        SAI_Peregrinus 2y ago
        The Surreal Numbers manage to be a sort of "biggest" ordered field, in NBG, though they're a proper class not a set. All other ordered fields are subfields of the Surreals. Of course "ordered" is doing a lot, since it excludes the complex numbers, vectors, bivectors, etc. Whether elements of some object that isn't an ordered field should be considered "nubmers" is related but different question.
  - deleted 2y ago
    [deleted]
  - sebtron 2y ago
    I don't think it is a "funny" notion of inclusion, but rather that once ℚ is defined, ℤ is silently redefined to be that one subset of ℚ that was used in the construction.
    - klodolph 2y ago
      There’s a very deep problem with that—every time you invent a “superset”, do you then have to redefine the subset to be a subset of that “superset”? There is an infinite chain of supersets of the rational numbers, real numbers, etc. Think of it like this… we can define 0, and then define 1 as the successor. Repeating this, we can have a definition for every finite number. But we cannot do this the other way around. We cannot start with ∞, define the predecessor to ∞, and then somehow get back to 0. In other words, if you want to work backwards and say that smaller sets (like the natural numbers) are a subset of the bigger sets (like complex numbers), then you have to pick a “biggest set” containing all numbers, which is unsatisfactory. Somebody always wants a bigger set.
      - ysofunny 2y ago
        > There’s a very deep problem with that—every time you invent a “superset”, do you then have to redefine the subset to be a subset of that “superset”? I have thought about this too, and I'd initially agree with you. but I thought at some point how mathematical history is not extremely dissimilar from this. put in very rough terms: at first humans discovered/invented numbers (i.e. the counting numbers); these started at number one — the first number. later on, at some point we had to go back and realize that there was a zero before number one which "silently" redefined the first number as zero and this created the natural numbers a the modern set-based N edit: adding this alternative rendering of my intended comment triggered by a condescending reply: "mathematics silently redefines stuff all the time. deal with it"
        klodolph 2y ago
        There is a different answer here which is more satisfactory… which is to use notions of equality other than set theoretic equality. Which is what the article is talking about.
  - ysofunny 2y ago
    I disagree but I'm being nitpicky I think the real funky business happens right between ℚ ⊂ ℝ but maybe all I'm really trying to say is "hey, look at me, I understand how all of ℕ ⊂ ℤ ⊂ ℚ" I'm very very sure that it's possible to give a fully ZF set-theoretic construction of the rationals using sets. in fact IMO the annoying thing is that there are in fact two trivially equivalent constructions that I can think of the top of my head, and I find that even worse than there being none at all
    - klodolph 2y ago
      What do you disagree with? Traditionally, you define ℚ as equivalence classes of pairs of integers. The integer 0 is an integer, it’s not an “equivalence class of pairs of integers” and therefore it’s not a rational, in the set-theoretic sense. Real numbers have lots more constructions. https://en.m.wikipedia.org/wiki/Construction_of_the_real_numbers https://en.m.wikipedia.org/wiki/Construction_of_the_real_num...
      - ysofunny 2y ago
        so yes, to answer one of my own questions. I was only really saying that I don't really know any of those constructions; but know all the "preceding" ones. I gotta figure out dedekind cuts or at least learn tarski's fixed point theorem which I'm sure that would allow me to much better understand tarski's construction all in the slow lifelong process of understanding and learning to draw post's lattice finally, to answer your question, I disagree with saying that there's funky business between ℤ ⊂ ℚ because of my alleged claim that there is at least one construction which avoids the problem you describe, but as I was trying to say, these would have a non-unique way to construct number zero which nobody likes
      - zeroonetwothree 2y ago
        You could construct the larger set and then define the smaller sets as specific subsets. For example Conway’s surreal numbers is a fun construction. If you do it that way then there is only one version of “1”
      - anon291 2y ago
  - auggierose 2y ago
    No funny notion of ⊂ at all, it is about how you construct ℚ, for example. You construct Q(ℤ), show that ℤ is embedded in Q(ℤ) via a monomorphism I, and then define ℚ as (Q(ℤ) \ I(ℤ)) ∪ ℤ. For example. You are right that nobody cares about how this works in detail. It does assume though some notion of ℚ and ℤ as collections, but not necessarily sets from ZFC.
  - anon291 2y ago
    Not at all. This is only a problem when doing formal verification due to how the theorem provers work (based on lambda calc). N is the set of zero and all its successors. Z is N extended with all additive inverses, which means it includes all of N. Q is Z with all multiplicative inverses, so it includes all Z. R is the set of Q plus all supremums and infinums of all bounded sets of Q. R is only not Q when you define R with dedekind cuts, which is a nice formal construction, but doesn't change what R is, up to isomorphism.
    - nyssos 2y ago
      > up to isomorphism Which is exactly the sort of more sophisticated notion of equivalence you end up needing in these cases.
      - auggierose 2y ago
        See my other comment. You can define R(ℚ) as Dedekind cuts, see that there is a monomorphism I from ℚ to R(ℚ), and then set ℝ = (R(ℚ) \ I(ℚ)) ∪ ℚ. Then you have ℚ ⊂ ℝ and ℝ ≅ R(ℚ). No problem. Except of course if you work in a theorem prover that doesn't support a construction like that.
      - anon291 2y ago
        Yeah, I'm very familiar. The 'up to isomorphism' applies to dedekind cuts et al. I'm pointing out that the nature of R is independent of its definition, and that any mathematical formal system you invent to construct R (up to isomorphism) is just a description. R exists independently on its own. The constructions of R are useful, because you can show things about them that could be applicable to R. However, the article gives a rhetorical question of whether you should be able to say 0 is in 3. No you should not, because while there are many constructions of the natural numbers, the universal property they all share (that there is a zero and a successor) does not permit any notion of inclusion. The construction of the naturals as sets would permit such notions, but these are not relevant to any discussion of the natural numbers. Put in homotopy type theory terms, the natural numbers are the equivalence class of all representations of the natural numbers, and all propositions over the natural numbers are the equivalence classes of all propositions over all representations of the natural numbers. Since one cannot draw an equivalence between '0 \in 3' and any proposition from another construction of the natural numbers (I believe), then the term '0 \in 3' is not a proposition over the natural numbers. Put another way, I posit that there are constructions isomorphic to the natural numbers whose propositions cannot be mapped onto the space of all propositions over the construction of the natural numbers as sets. Whereas, all constructions of the natural numbers will permit a proof of the associativity of addition, or the infinity of primes. So these proofs are what should be accepted as 'proofs' over the natural numbers, but '0 \in 3' would not, because it's missing in many systems. '0 \in 3' could be used in the set representation to be the definition of less than, but it is not a statement that applies to all representations. Is that clearer?
  - deleted 2y ago
    [deleted]
  - diffeomorphism 2y ago
    You would usually use something like \hookrightarrow instead. The set is isomorphic to a subset. In the same way the real line is "included" in the plane (\R \times \{0\}) or the sphere is not only a subset of the whole space but a submanifold. Math uses lots of polymorphism and overloaded notation, but that is also part of the beauty, where "A=A" can actually be a deep result about concepts being compatible.
  - paulddraper 2y ago
    > You have to use a very funny notion of ⊂ for that to make sense ?? Are you claiming that ℤ ⊄ ℚ This thread is wild.
    - gus_massa 2y ago
      There is a subset of Q that is canonicaly isomorph to Z. Probably the distiction is too technical unless you want to do some weird advanced algebra. (Note that in most weird advanced math the distiction doen't matter.) So in most case, mathematicians and non mathematicians just write Z ⊂ Q and live happily ever after. But if you get supertechnical you should use scare quotes Z "⊂" Q or to look more proffesional Z ↪ Q (because tha inclusion is an injective funcion, and sometimes it's useful to think aboout it as a function.). --- To add some confussion: Imagine that you buy in the supermarket a copy of Z that is green and another copy of Z that is red. 1(red) + 2 (red) = 3(red) 1(green) + 2(green) = 3(green) (If I get super technical, I have to define a +(red) operation and a +(green) operation. And probably also a =(red) and =(green) as the article discuss.) Are they the same Z or just canonicaly isomorph or it doen't matter? --- To add even more confussion: You have a copy of abstract Z and a copy inside the rational written as n/1: 1 + 2 = 3 1/1 + 2/1 = 3/1 Are they the same Z or just canonicaly isomorph or it doen't matter?
      - paulddraper 2y ago
        > There is a subset of Q that is canonicaly isomorph to Z. Actually, the statement ℤ ⊂ ℚ reads "The set of integers is a proper subset of rationals."
- interroboink 2y ago
  Yeah I didn't get that comment, either. At least in my education, you first define the natural numbers (where 0 and 1 are special, and the rest are defined in terms of that (ie 2 = 1+1)), then you define negation, which gives you the negative numbers. Then you layer on multiplication and division, which gives you rational numbers, and so on. So, it's the same "0 and 1" definition all the way through, just with additional operations being added to the mix. Though maybe other approaches do it differently.
  - germanier 2y ago
    The usual formal definition for the rational numbers is equivalence classes of pairs of integers. The zero is then the equivalence class of (0, 1) which is not the same as the integer 0. You could certainly somehow get it to work by starting with the closure of the division operation but would introduce a lot of unnecessary headache along the way.
  - klodolph 2y ago
    I think you may have not gotten far enough to get a formal explanation of what 0 and 1 are. The definition taught to most mathematicians is that for the natural numbers, 0 = {} 1 = {{}} In general S(N) = N ∪ {N} But this is not how the real numbers are constructed. You either use Dedekind cuts, Cauchy sequences, or something else.
    - gus_massa 2y ago
      Complex numbers are just pairs (real and imaginary) of Cauchy sequences of pairs (numerator and denominator) of pairs (positive and negative) of nested versions of the empty set. (modulo al the necesary equivalence to make this work). So the natural number {{}} is canonical included in the complex numbers as [something]. Natural {{}} Integer ({{}},{}) Rational (({{}},{}),({{}},{})) Real (({{}},{}),({{}},{})), (({{}},{}),({{}},{})), (({{}},{}),({{}},{})), ... Complex ((({{}},{}),({{}},{})), (({{}},{}),({{}},{})), (({{}},{}),({{}},{})), ... , (({},{}),({{}},{})), (({},{}),({{}},{})), (({},{}),({{}},{})), ... ) (And there are a few alternative definition, but I think they are even more messy.)
- singularity2001 2y ago
  I came across this topic in lean, where you have different definitions of 0 and 1 within the same context and you can auto-convert using coercion. instance : One Hyper where one := ⟨1, 0, 0, 0⟩ scoped notation "1" => One.one -- doesn't work "invalid atom" and unnecessary instance : OfNat Bool 1 where ofNat := true instance : Coe ℤ Bool where coe z := z ≠ 0 instance : Coe ℝ ℝ⋆ where coe r := ⟨ r 0 0 0 ⟩ Basically all the fun of C++ casting just that you are always safe.
  - auggierose 2y ago
    It is a different story in Lean though, because Lean, as most other logics based on type systems, doesn't have subtypes. So all you have are coercions. That's actually a bad thing.
    - staunton 2y ago
      What do you mean by "subtype"? Lean defines a thing calles `Subtype`, members of which are constructed from a value and a property.
      - auggierose 2y ago
        That might be called Subtype, but is a disjoint type containing different values than the original type. If S is a subtype of T, and x : S, then also x : T.
    - singularity2001 2y ago
      why would you say that this is a bad thing
      - auggierose 2y ago
        Because coercions are just a work-around, and more machinery hidden from you, but still there causing problems (like types). If you are coming from C++, then yes, Lean coercions are a step up. If you are coming from mathematics, then Lean coercions are just a cumbersome work-around.
- math_dandy 2y ago
  Absolutely right. If you keep worrying about whether 1 is actually 1, you’ll never get any math done.
- Someone 2y ago
  > I think pretty much every mathematician agrees that […] 1 the integer is the same as 1 the real number Yes and no. NO: there already are multiple ways to construct “1 the natural number”, even if you restrict that to set-theoretic ones. See https://en.wikipedia.org/wiki/Set-theoretic_definition_of_natural_numbers https://en.wikipedia.org/wiki/Set-theoretic_definition_of_na.... Von Neumann defined the natural number 1 as {∅} (the set with as only element the empty set), Frege and Russell as the equivalence class of all sets with a single element (and that’s not a circular definition) Integers typically are constructed from those (See for example https://mathesis-online.com/integers https://mathesis-online.com/integers, which defines an integer i as the equivalence class of pairs (a,b) of natural numbers such that a = b + i) In this construction, “the integer 1” is the infinite set {(1,0},{2,1},{3,2},…}. That obviously (in the mathematical sense) is different from the one element set {∅} Rationals and reals are constructed on top of that (see for example https://www.quora.com/How-is-the-set-of-real-numbers-constructed-by-using-the-axiomatic-set-theory-ZFC-set-theory https://www.quora.com/How-is-the-set-of-real-numbers-constru... for a way to construct those) YES: when you decide to ignore the low-level stuff and just use the intuitive definition of reals and integers. (Alternatives: - don’t ignore it, but start at the basis, calling the integers something else, then prove equivalence between a well-defined subset of the reals and the integers and then give that subset the name “integers”. - directly construct the reals without first constructing the integers and then define the integers as a subset of them. I’m not aware of any way to define the reals without first defining integers, though. )
  - auggierose 2y ago
    You ellipsed ([...]) the "can assume" part of my statement. Every mathematician knows the different ways of constructing numbers. It really is a simple YES.
    - Someone 2y ago
      No, it isn’t. Whether it is depends on what level the mathematician operates, and will differ on what they’re working on. That’s precisely the subject of this article: there’s an intuitive idea that, upon close scrutiny, turns out to before complex than it appears to be. So, if you want to start from the basis in a proof assistant, you’ll have to discriminate between them and either give them different names or introduce context from which the computer can infer what you mean. If, for example, you want to prove that two definitions of integers are equivalent, you need two different names.
- dataflow 2y ago
  The (principle) cube root of the integer -1 is -1, but the (principle) cube root of the complex number -1 is (1 + sqrt 3) / 2. They sure seem like different objects. Though I guess whether you want to blame that on the operators vs. the objects themselves can be left to your taste, but I'm not sure what "these objects are equivalent" would mean if the behaviors are left unspecified as characteristics of the objects (which would be the former case).
  - auggierose 2y ago
    That is indeed a nice feature of types: You can overload notions. In this case you overload the notion "principal cube root" (PCR) to mean different things for ℤ and for ℂ. But really, "principal cube root" as you would like it to behave is not well-defined just for a number, you also need to provide the algebraic structure you consider it in, as in PCR(ℤ, -1) = -1, and PCR(ℂ, -1) = (1 + sqrt 3) / 2. Alternatively, just set PCR(-1) = (1 + sqrt 3) / 2. That makes probably the most sense, as there is not much value in a PCR notion for integers in the first place.
  - lupire 2y ago
    "Principal" root isn't an interesting mathematical object. It's just an arbitrary way to choose a preferred element from an equivalence class, when you're too lazy to consider the whole class and you want to pretend that 'implies" ("only if") is is the same as " biconditional" ('if and only if").
    - dataflow 2y ago
      > when you're too lazy to consider the whole class Well then consider the whole class? The whole classes are different too, I don't get your point.
- im3w1l 2y ago
  I think every mathematician are aware of both of those perspectives, and uses whichever is more convenient at the moment.
  - auggierose 2y ago
    Yes, but in a software like a theorem prover you must make the conscious decision whether you want your prover to be able to assume ℕ ⊂ ℤ or not. All the type theory based ones say "not". That is not very convenient.
vishnugupta 2y ago
> Every mathamatician knows that the integer 1 and the real number 1 different objects [0]. This is quite interesting to me as I'm trying to understand, recreationally, these concepts. From what you've written it looks like there are several ways to construct numbers. I'm aware of some of them but I don't know if they are connected or related e.g., Dedikend cut, Van Neumann numbers etc., It'd be great if you could list down all such constructions.
- klodolph 2y ago
  Wikipedia has a lot of resources. Naturally, it won’t all be accessible (some of these constructions sit at the top of a mountain, and you have to climb the mountain first). https://en.m.wikipedia.org/wiki/Construction_of_the_real_numbers https://en.m.wikipedia.org/wiki/Construction_of_the_real_num...
- gizmo686 2y ago
  All of the ways is quite the ask. There are 2 main main approaches: explicit constructions and axiomatic constructions. Dedikend cuts and Von Neuman numbers are both examples of explicit constructions. You can point to exactly what a given number "is", and then prove properties about you construction. The other approach is the axiomatic construction, where you define what properties you want your numbers to have. You then (hopefully) prove that such a system exists and is, in some sense unique. Taking the integers, the most common explicit construction is the set-theoretic Von Neumon construction, where 0={}, 1={0}, 2={0,1}, 3={0,1,2}... You can also imagine defing 0={}, 1={0}, 2={1}, 3={2} Note that while we say these are equivalent definitions, they produce different results in the sense that, for example, 0∈3 in the former, but not in the latter. [0]. You can also define natural numbers as a subset of the cardinals. In this construction, 3 represents the collection of all sets that can be put in a 1-to-1 correspondance to the set { {}, {{}}, {{{}}} }. Here, the exlusion of various infinities is a rather arbitrary part of the definition. You can also define integers as a subset of combinatorical games, given by 0={|}, 1={0|}, 2={1|}. This naturally leads to negative numbers, -1={|0}, and a zoo of "numbers" not seen outside of combinatorical game theory, such as ↑ = {0|{0|0}}. Still, if you restrict yourself to the integer looking numbers and follow the game theory rules of addition, you get something equivalent to the natural numbers. You can also define them as strings constructed from the alphabet of a single character, so 0="", 1="a", 2="aa". (This is the free monoid over a single set) Lambda Calculus gives us the church encoding, where: * 0 = λf.λx.x * 1 = λf.λx.f x * 2 = λf.λx.f (f x) Under the axiomatic definition of numbers, the classical definition is given by the 9 Peano axioms, which amount to assuming the existence of 0 and a "succesor" function S(n) informally corresponding to S(n) = n+1. All of the above examples are things I have actually seen and that arise naturally in their respective branch of mathametics. [0] This contradiction is not actually an issue, because no one ever actually says 0∈3, even though it is technically true in some constructions.
deleted 2y ago
[deleted]
ajsnigrutin 2y ago
Meh, php solves this with "$a === $b" :D
paulddraper 2y ago
> Every mathamatician knows that the integer 1 and the real number 1 different objects !!!!!! The integer 1 is the same as the real number 1 ,is the same as the odd number 1, is the same as the perfect square 1, etc. ℤ ⊂ ℝ That this is the top-voted comment on this thread.....
- r0uv3n 2y ago
  > ℤ ⊂ ℝ That is not at all obvious without some canonical isomorphism acting on ℤ, or at least is a behaviour strictly dependent on your particular set theoretic construction of the reals. E.g. for the cauchy sequence construction of the reals, the image of the integer 1 under this canonical isomorphism would be the equivalence class of the sequence (1,0,0,0,...), but these are of course not the same object in a set theoretic sense.
  - chiefjosh 2y ago
    I think he literally just demonstrated the problem you were trying to illustrate about software provers

auggierose 2y ago

I think pretty much every mathematician agrees that you can assume ℕ ⊂ ℤ ⊂ ℚ ⊂ ℝ ⊂ ℂ, and that 1 the integer is the same as 1 the real number.

klodolph 2y ago
You have to use a very funny notion of ⊂ for that to make sense. Mathematicians recognize that there is a lot of funny business going on behind the scenes… if you use the typical construction of these sets, then ℤ ⊂ ℚ is for sure false under the set-theoretic definition of what subsets are. So you are going to get a lot of funny explanations of why you can still say “ℤ ⊂ ℚ” and what that means. And what is “the same as” anyway?
- hansvm 2y ago
  The typical construction is just to show that they _can_ be constructed. Once you have "primitive" integers, rationals, ..., you pick (for this finite example) the largest of them, and define the "integers" to be a subset with a certain property. That's also well-defined, and you find _exactly_ the same integers in the rationals and reals.
- interroboink 2y ago
  Could you provide an example? I'm not seeing it. Is there some integer that is not also a rational number?
  - klodolph 2y ago
    How about this example: the natural number 0 is not a member of the integers, from a set theoretic perspective. In the natural numbers, 0 = {} However, {} is not an element of the integers. This is not something I expect to be easy to understand. This is the standard set theoretic definition of integers that mainstream mathematicians use. This is not some esoteric, fringe theory.
    - Affric 2y ago
      Isn’t the empty set a subset of all sets? A quick look at Wikipedia indicates that there exist other constructions.
      - klodolph 2y ago
        Yes, the empty set is a subset of all sets. I think some wires got crossed somewhere because whether zero is a subset of some other set doesn’t fit into the questions we are trying to answer. You could pick a construction where the natural numbers are a subset of the integers. This is trivial, but this is a poor strategy overall, because you can always find a bigger set of numbers to work with. You can’t take the “biggest” set of numbers and then define all other sets of numbers as subsets of that. It would be kind of like trying to count down from infinity.
        Affric 2y ago
        I see where I have gone wrong. Element vs subset. Classic error when thinking fast. Thank you for the thought provoking comments.
        SAI_Peregrinus 2y ago
        The Surreal Numbers manage to be a sort of "biggest" ordered field, in NBG, though they're a proper class not a set. All other ordered fields are subfields of the Surreals. Of course "ordered" is doing a lot, since it excludes the complex numbers, vectors, bivectors, etc. Whether elements of some object that isn't an ordered field should be considered "nubmers" is related but different question.
- deleted 2y ago
  [deleted]
- sebtron 2y ago
  I don't think it is a "funny" notion of inclusion, but rather that once ℚ is defined, ℤ is silently redefined to be that one subset of ℚ that was used in the construction.
  - klodolph 2y ago
    There’s a very deep problem with that—every time you invent a “superset”, do you then have to redefine the subset to be a subset of that “superset”? There is an infinite chain of supersets of the rational numbers, real numbers, etc. Think of it like this… we can define 0, and then define 1 as the successor. Repeating this, we can have a definition for every finite number. But we cannot do this the other way around. We cannot start with ∞, define the predecessor to ∞, and then somehow get back to 0. In other words, if you want to work backwards and say that smaller sets (like the natural numbers) are a subset of the bigger sets (like complex numbers), then you have to pick a “biggest set” containing all numbers, which is unsatisfactory. Somebody always wants a bigger set.
    - ysofunny 2y ago
      > There’s a very deep problem with that—every time you invent a “superset”, do you then have to redefine the subset to be a subset of that “superset”? I have thought about this too, and I'd initially agree with you. but I thought at some point how mathematical history is not extremely dissimilar from this. put in very rough terms: at first humans discovered/invented numbers (i.e. the counting numbers); these started at number one — the first number. later on, at some point we had to go back and realize that there was a zero before number one which "silently" redefined the first number as zero and this created the natural numbers a the modern set-based N edit: adding this alternative rendering of my intended comment triggered by a condescending reply: "mathematics silently redefines stuff all the time. deal with it"
      - klodolph 2y ago
        There is a different answer here which is more satisfactory… which is to use notions of equality other than set theoretic equality. Which is what the article is talking about.
- ysofunny 2y ago
  I disagree but I'm being nitpicky I think the real funky business happens right between ℚ ⊂ ℝ but maybe all I'm really trying to say is "hey, look at me, I understand how all of ℕ ⊂ ℤ ⊂ ℚ" I'm very very sure that it's possible to give a fully ZF set-theoretic construction of the rationals using sets. in fact IMO the annoying thing is that there are in fact two trivially equivalent constructions that I can think of the top of my head, and I find that even worse than there being none at all
  - klodolph 2y ago
    What do you disagree with? Traditionally, you define ℚ as equivalence classes of pairs of integers. The integer 0 is an integer, it’s not an “equivalence class of pairs of integers” and therefore it’s not a rational, in the set-theoretic sense. Real numbers have lots more constructions. https://en.m.wikipedia.org/wiki/Construction_of_the_real_numbers https://en.m.wikipedia.org/wiki/Construction_of_the_real_num...
    - ysofunny 2y ago
      so yes, to answer one of my own questions. I was only really saying that I don't really know any of those constructions; but know all the "preceding" ones. I gotta figure out dedekind cuts or at least learn tarski's fixed point theorem which I'm sure that would allow me to much better understand tarski's construction all in the slow lifelong process of understanding and learning to draw post's lattice finally, to answer your question, I disagree with saying that there's funky business between ℤ ⊂ ℚ because of my alleged claim that there is at least one construction which avoids the problem you describe, but as I was trying to say, these would have a non-unique way to construct number zero which nobody likes
    - zeroonetwothree 2y ago
      You could construct the larger set and then define the smaller sets as specific subsets. For example Conway’s surreal numbers is a fun construction. If you do it that way then there is only one version of “1”
    - anon291 2y ago
- auggierose 2y ago
  No funny notion of ⊂ at all, it is about how you construct ℚ, for example. You construct Q(ℤ), show that ℤ is embedded in Q(ℤ) via a monomorphism I, and then define ℚ as (Q(ℤ) \ I(ℤ)) ∪ ℤ. For example. You are right that nobody cares about how this works in detail. It does assume though some notion of ℚ and ℤ as collections, but not necessarily sets from ZFC.
- anon291 2y ago
  Not at all. This is only a problem when doing formal verification due to how the theorem provers work (based on lambda calc). N is the set of zero and all its successors. Z is N extended with all additive inverses, which means it includes all of N. Q is Z with all multiplicative inverses, so it includes all Z. R is the set of Q plus all supremums and infinums of all bounded sets of Q. R is only not Q when you define R with dedekind cuts, which is a nice formal construction, but doesn't change what R is, up to isomorphism.
  - nyssos 2y ago
    > up to isomorphism Which is exactly the sort of more sophisticated notion of equivalence you end up needing in these cases.
    - auggierose 2y ago
      See my other comment. You can define R(ℚ) as Dedekind cuts, see that there is a monomorphism I from ℚ to R(ℚ), and then set ℝ = (R(ℚ) \ I(ℚ)) ∪ ℚ. Then you have ℚ ⊂ ℝ and ℝ ≅ R(ℚ). No problem. Except of course if you work in a theorem prover that doesn't support a construction like that.
    - anon291 2y ago
      Yeah, I'm very familiar. The 'up to isomorphism' applies to dedekind cuts et al. I'm pointing out that the nature of R is independent of its definition, and that any mathematical formal system you invent to construct R (up to isomorphism) is just a description. R exists independently on its own. The constructions of R are useful, because you can show things about them that could be applicable to R. However, the article gives a rhetorical question of whether you should be able to say 0 is in 3. No you should not, because while there are many constructions of the natural numbers, the universal property they all share (that there is a zero and a successor) does not permit any notion of inclusion. The construction of the naturals as sets would permit such notions, but these are not relevant to any discussion of the natural numbers. Put in homotopy type theory terms, the natural numbers are the equivalence class of all representations of the natural numbers, and all propositions over the natural numbers are the equivalence classes of all propositions over all representations of the natural numbers. Since one cannot draw an equivalence between '0 \in 3' and any proposition from another construction of the natural numbers (I believe), then the term '0 \in 3' is not a proposition over the natural numbers. Put another way, I posit that there are constructions isomorphic to the natural numbers whose propositions cannot be mapped onto the space of all propositions over the construction of the natural numbers as sets. Whereas, all constructions of the natural numbers will permit a proof of the associativity of addition, or the infinity of primes. So these proofs are what should be accepted as 'proofs' over the natural numbers, but '0 \in 3' would not, because it's missing in many systems. '0 \in 3' could be used in the set representation to be the definition of less than, but it is not a statement that applies to all representations. Is that clearer?
- deleted 2y ago
  [deleted]
- diffeomorphism 2y ago
  You would usually use something like \hookrightarrow instead. The set is isomorphic to a subset. In the same way the real line is "included" in the plane (\R \times \{0\}) or the sphere is not only a subset of the whole space but a submanifold. Math uses lots of polymorphism and overloaded notation, but that is also part of the beauty, where "A=A" can actually be a deep result about concepts being compatible.
- paulddraper 2y ago
  > You have to use a very funny notion of ⊂ for that to make sense ?? Are you claiming that ℤ ⊄ ℚ This thread is wild.
  - gus_massa 2y ago
    There is a subset of Q that is canonicaly isomorph to Z. Probably the distiction is too technical unless you want to do some weird advanced algebra. (Note that in most weird advanced math the distiction doen't matter.) So in most case, mathematicians and non mathematicians just write Z ⊂ Q and live happily ever after. But if you get supertechnical you should use scare quotes Z "⊂" Q or to look more proffesional Z ↪ Q (because tha inclusion is an injective funcion, and sometimes it's useful to think aboout it as a function.). --- To add some confussion: Imagine that you buy in the supermarket a copy of Z that is green and another copy of Z that is red. 1(red) + 2 (red) = 3(red) 1(green) + 2(green) = 3(green) (If I get super technical, I have to define a +(red) operation and a +(green) operation. And probably also a =(red) and =(green) as the article discuss.) Are they the same Z or just canonicaly isomorph or it doen't matter? --- To add even more confussion: You have a copy of abstract Z and a copy inside the rational written as n/1: 1 + 2 = 3 1/1 + 2/1 = 3/1 Are they the same Z or just canonicaly isomorph or it doen't matter?
    - paulddraper 2y ago
      > There is a subset of Q that is canonicaly isomorph to Z. Actually, the statement ℤ ⊂ ℚ reads "The set of integers is a proper subset of rationals."
interroboink 2y ago
Yeah I didn't get that comment, either. At least in my education, you first define the natural numbers (where 0 and 1 are special, and the rest are defined in terms of that (ie 2 = 1+1)), then you define negation, which gives you the negative numbers. Then you layer on multiplication and division, which gives you rational numbers, and so on. So, it's the same "0 and 1" definition all the way through, just with additional operations being added to the mix. Though maybe other approaches do it differently.
- germanier 2y ago
  The usual formal definition for the rational numbers is equivalence classes of pairs of integers. The zero is then the equivalence class of (0, 1) which is not the same as the integer 0. You could certainly somehow get it to work by starting with the closure of the division operation but would introduce a lot of unnecessary headache along the way.
- klodolph 2y ago
  I think you may have not gotten far enough to get a formal explanation of what 0 and 1 are. The definition taught to most mathematicians is that for the natural numbers, 0 = {} 1 = {{}} In general S(N) = N ∪ {N} But this is not how the real numbers are constructed. You either use Dedekind cuts, Cauchy sequences, or something else.
  - gus_massa 2y ago
    Complex numbers are just pairs (real and imaginary) of Cauchy sequences of pairs (numerator and denominator) of pairs (positive and negative) of nested versions of the empty set. (modulo al the necesary equivalence to make this work). So the natural number {{}} is canonical included in the complex numbers as [something]. Natural {{}} Integer ({{}},{}) Rational (({{}},{}),({{}},{})) Real (({{}},{}),({{}},{})), (({{}},{}),({{}},{})), (({{}},{}),({{}},{})), ... Complex ((({{}},{}),({{}},{})), (({{}},{}),({{}},{})), (({{}},{}),({{}},{})), ... , (({},{}),({{}},{})), (({},{}),({{}},{})), (({},{}),({{}},{})), ... ) (And there are a few alternative definition, but I think they are even more messy.)
singularity2001 2y ago
I came across this topic in lean, where you have different definitions of 0 and 1 within the same context and you can auto-convert using coercion. instance : One Hyper where one := ⟨1, 0, 0, 0⟩ scoped notation "1" => One.one -- doesn't work "invalid atom" and unnecessary instance : OfNat Bool 1 where ofNat := true instance : Coe ℤ Bool where coe z := z ≠ 0 instance : Coe ℝ ℝ⋆ where coe r := ⟨ r 0 0 0 ⟩ Basically all the fun of C++ casting just that you are always safe.
- auggierose 2y ago
  It is a different story in Lean though, because Lean, as most other logics based on type systems, doesn't have subtypes. So all you have are coercions. That's actually a bad thing.
  - staunton 2y ago
    What do you mean by "subtype"? Lean defines a thing calles `Subtype`, members of which are constructed from a value and a property.
    - auggierose 2y ago
      That might be called Subtype, but is a disjoint type containing different values than the original type. If S is a subtype of T, and x : S, then also x : T.
  - singularity2001 2y ago
    why would you say that this is a bad thing
    - auggierose 2y ago
      Because coercions are just a work-around, and more machinery hidden from you, but still there causing problems (like types). If you are coming from C++, then yes, Lean coercions are a step up. If you are coming from mathematics, then Lean coercions are just a cumbersome work-around.
math_dandy 2y ago
Absolutely right. If you keep worrying about whether 1 is actually 1, you’ll never get any math done.
Someone 2y ago
> I think pretty much every mathematician agrees that […] 1 the integer is the same as 1 the real number Yes and no. NO: there already are multiple ways to construct “1 the natural number”, even if you restrict that to set-theoretic ones. See https://en.wikipedia.org/wiki/Set-theoretic_definition_of_natural_numbers https://en.wikipedia.org/wiki/Set-theoretic_definition_of_na.... Von Neumann defined the natural number 1 as {∅} (the set with as only element the empty set), Frege and Russell as the equivalence class of all sets with a single element (and that’s not a circular definition) Integers typically are constructed from those (See for example https://mathesis-online.com/integers https://mathesis-online.com/integers, which defines an integer i as the equivalence class of pairs (a,b) of natural numbers such that a = b + i) In this construction, “the integer 1” is the infinite set {(1,0},{2,1},{3,2},…}. That obviously (in the mathematical sense) is different from the one element set {∅} Rationals and reals are constructed on top of that (see for example https://www.quora.com/How-is-the-set-of-real-numbers-constructed-by-using-the-axiomatic-set-theory-ZFC-set-theory https://www.quora.com/How-is-the-set-of-real-numbers-constru... for a way to construct those) YES: when you decide to ignore the low-level stuff and just use the intuitive definition of reals and integers. (Alternatives: - don’t ignore it, but start at the basis, calling the integers something else, then prove equivalence between a well-defined subset of the reals and the integers and then give that subset the name “integers”. - directly construct the reals without first constructing the integers and then define the integers as a subset of them. I’m not aware of any way to define the reals without first defining integers, though. )
- auggierose 2y ago
  You ellipsed ([...]) the "can assume" part of my statement. Every mathematician knows the different ways of constructing numbers. It really is a simple YES.
  - Someone 2y ago
    No, it isn’t. Whether it is depends on what level the mathematician operates, and will differ on what they’re working on. That’s precisely the subject of this article: there’s an intuitive idea that, upon close scrutiny, turns out to before complex than it appears to be. So, if you want to start from the basis in a proof assistant, you’ll have to discriminate between them and either give them different names or introduce context from which the computer can infer what you mean. If, for example, you want to prove that two definitions of integers are equivalent, you need two different names.
dataflow 2y ago
The (principle) cube root of the integer -1 is -1, but the (principle) cube root of the complex number -1 is (1 + sqrt 3) / 2. They sure seem like different objects. Though I guess whether you want to blame that on the operators vs. the objects themselves can be left to your taste, but I'm not sure what "these objects are equivalent" would mean if the behaviors are left unspecified as characteristics of the objects (which would be the former case).
- auggierose 2y ago
  That is indeed a nice feature of types: You can overload notions. In this case you overload the notion "principal cube root" (PCR) to mean different things for ℤ and for ℂ. But really, "principal cube root" as you would like it to behave is not well-defined just for a number, you also need to provide the algebraic structure you consider it in, as in PCR(ℤ, -1) = -1, and PCR(ℂ, -1) = (1 + sqrt 3) / 2. Alternatively, just set PCR(-1) = (1 + sqrt 3) / 2. That makes probably the most sense, as there is not much value in a PCR notion for integers in the first place.
- lupire 2y ago
  "Principal" root isn't an interesting mathematical object. It's just an arbitrary way to choose a preferred element from an equivalence class, when you're too lazy to consider the whole class and you want to pretend that 'implies" ("only if") is is the same as " biconditional" ('if and only if").
  - dataflow 2y ago
    > when you're too lazy to consider the whole class Well then consider the whole class? The whole classes are different too, I don't get your point.
im3w1l 2y ago
I think every mathematician are aware of both of those perspectives, and uses whichever is more convenient at the moment.
- auggierose 2y ago
  Yes, but in a software like a theorem prover you must make the conscious decision whether you want your prover to be able to assume ℕ ⊂ ℤ or not. All the type theory based ones say "not". That is not very convenient.

vishnugupta 2y ago

> Every mathamatician knows that the integer 1 and the real number 1 different objects [0]. This is quite interesting to me as I'm trying to understand, recreationally, these concepts. From what you've written it looks like there are several ways to construct numbers. I'm aware of some of them but I don't know if they are connected or related e.g., Dedikend cut, Van Neumann numbers etc., It'd be great if you could list down all such constructions.

klodolph 2y ago
Wikipedia has a lot of resources. Naturally, it won’t all be accessible (some of these constructions sit at the top of a mountain, and you have to climb the mountain first). https://en.m.wikipedia.org/wiki/Construction_of_the_real_numbers https://en.m.wikipedia.org/wiki/Construction_of_the_real_num...
gizmo686 2y ago
All of the ways is quite the ask. There are 2 main main approaches: explicit constructions and axiomatic constructions. Dedikend cuts and Von Neuman numbers are both examples of explicit constructions. You can point to exactly what a given number "is", and then prove properties about you construction. The other approach is the axiomatic construction, where you define what properties you want your numbers to have. You then (hopefully) prove that such a system exists and is, in some sense unique. Taking the integers, the most common explicit construction is the set-theoretic Von Neumon construction, where 0={}, 1={0}, 2={0,1}, 3={0,1,2}... You can also imagine defing 0={}, 1={0}, 2={1}, 3={2} Note that while we say these are equivalent definitions, they produce different results in the sense that, for example, 0∈3 in the former, but not in the latter. [0]. You can also define natural numbers as a subset of the cardinals. In this construction, 3 represents the collection of all sets that can be put in a 1-to-1 correspondance to the set { {}, {{}}, {{{}}} }. Here, the exlusion of various infinities is a rather arbitrary part of the definition. You can also define integers as a subset of combinatorical games, given by 0={|}, 1={0|}, 2={1|}. This naturally leads to negative numbers, -1={|0}, and a zoo of "numbers" not seen outside of combinatorical game theory, such as ↑ = {0|{0|0}}. Still, if you restrict yourself to the integer looking numbers and follow the game theory rules of addition, you get something equivalent to the natural numbers. You can also define them as strings constructed from the alphabet of a single character, so 0="", 1="a", 2="aa". (This is the free monoid over a single set) Lambda Calculus gives us the church encoding, where: * 0 = λf.λx.x * 1 = λf.λx.f x * 2 = λf.λx.f (f x) Under the axiomatic definition of numbers, the classical definition is given by the 9 Peano axioms, which amount to assuming the existence of 0 and a "succesor" function S(n) informally corresponding to S(n) = n+1. All of the above examples are things I have actually seen and that arise naturally in their respective branch of mathametics. [0] This contradiction is not actually an issue, because no one ever actually says 0∈3, even though it is technically true in some constructions.

deleted 2y ago

[deleted]

ajsnigrutin 2y ago

Meh, php solves this with "$a === $b" :D

paulddraper 2y ago

> Every mathamatician knows that the integer 1 and the real number 1 different objects !!!!!! The integer 1 is the same as the real number 1 ,is the same as the odd number 1, is the same as the perfect square 1, etc. ℤ ⊂ ℝ That this is the top-voted comment on this thread.....

r0uv3n 2y ago
> ℤ ⊂ ℝ That is not at all obvious without some canonical isomorphism acting on ℤ, or at least is a behaviour strictly dependent on your particular set theoretic construction of the reals. E.g. for the cauchy sequence construction of the reals, the image of the integer 1 under this canonical isomorphism would be the equivalence class of the sequence (1,0,0,0,...), but these are of course not the same object in a set theoretic sense.
- chiefjosh 2y ago
  I think he literally just demonstrated the problem you were trying to illustrate about software provers