3 ms·

> 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 co

> 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.
  - auggierose 2y ago
    It helps to state carefully what you are trying to achieve. I want a theorem prover where constructing numbers such that ℕ ⊂ ℤ is easy. Doing this in a theorem prover is not trivial, for example none of the type based theorem provers allow that (although, Isabelle/ZF might qualify; it is based on set theory on top of a weak intuitionistic type theory; but here ℕ and ℤ are not types, but sets of the same type). It is trivial though if you are a mathematician, no matter what you are working on. You know that these constructions can be done, and that as a result you can assume ℕ ⊂ ℤ (if you want to). So as long as your theorem prover doesn't support something as trivial as that, it is lacking. And yes, that is exactly what Buzzard is talking about. For the case I am talking about here though, that is just table stakes: make sure your prover can do ℕ ⊂ ℤ ⊂ ℝ ⊂ ℂ. If you can do that, you can start worrying about more advanced issues of equality, and you might find that you have already solved a significant amount of them.
    - robinzfc 2y ago
      I can confirm that in Isabelle/ZF one can set up a context (locale) with the meaning of the ℕ ℤ ℝ ℂ symbols defined so that ℕ ⊂ ℤ ⊂ ℝ ⊂ ℂ. However ℕ for example will not be equal in such case to the canonical set of ZF natural numbers where 1 = {0}, 2 = {0,1} etc.

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.
- auggierose 2y ago
  It helps to state carefully what you are trying to achieve. I want a theorem prover where constructing numbers such that ℕ ⊂ ℤ is easy. Doing this in a theorem prover is not trivial, for example none of the type based theorem provers allow that (although, Isabelle/ZF might qualify; it is based on set theory on top of a weak intuitionistic type theory; but here ℕ and ℤ are not types, but sets of the same type). It is trivial though if you are a mathematician, no matter what you are working on. You know that these constructions can be done, and that as a result you can assume ℕ ⊂ ℤ (if you want to). So as long as your theorem prover doesn't support something as trivial as that, it is lacking. And yes, that is exactly what Buzzard is talking about. For the case I am talking about here though, that is just table stakes: make sure your prover can do ℕ ⊂ ℤ ⊂ ℝ ⊂ ℂ. If you can do that, you can start worrying about more advanced issues of equality, and you might find that you have already solved a significant amount of them.
  - robinzfc 2y ago
    I can confirm that in Isabelle/ZF one can set up a context (locale) with the meaning of the ℕ ℤ ℝ ℂ symbols defined so that ℕ ⊂ ℤ ⊂ ℝ ⊂ ℂ. However ℕ for example will not be equal in such case to the canonical set of ZF natural numbers where 1 = {0}, 2 = {0,1} etc.