Hacker News Reader

Comment by gizmo686 | Hacker News Reader

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.

View on HN

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

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?

Could you provide an example? I'm not seeing it.

Is there some integer that is not also a rational number?

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.

Isn’t the empty set a subset of all sets?

A quick look at Wikipedia indicates that there exist other constructions.

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.

I see where I have gone wrong. Element vs subset. Classic error when thinking fast. Thank you for the thought provoking comments.

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.

Yes, {} is a subset(⊂) of all sets, but it is not a member(∊) of all sets. For instance, {} is not a member of {{{}}}. In the Von-Neumann definition, 1:={0}={{}}. So, 0∊1, but 0 is not a member of {1} which is the above set. https://en.wikipedia.org/wiki/Set-theoretic_definition_of_na...

Ah, thank you. It does actually make some sense, having looked into it some more now (:

It looks like the approach of defining ℤ in terms of ℕ is much more tedious to deal with overall, so can see the advantages.

Conceptually, yes, every integer is also a rational number. But they are represented as different objects.

It's a bit like saying every int32 is also a double. Yes, every value of int32 fits into a double, but the bit pattern is different.

The canonical construction for rational numbers is pairs (a, b) which we interpret as a/b. An integer k "is the same as" (k, 1).

So it might be more correct to say every integer has the same value as some rational number. Of course this distinction is pointless most of the time, so we don't worry about it.

This is not unique to integers and rationals. It also applies to naturals and integers, rationals and reals, etc.

But an int32 1 isn’t the same as a mathematic object 1. So of course your analogy doesn’t work

By definition, analogies are between things that aren’t the “same thing”.

And a double 1.0 isn't the same as a rational 1/1. But I also didn't claim either of these things.

I understand that this might be a problem in a programming language, even if you decide to ignore that mathematical sets have infinitively many elements. When I programmed an RPN calculator supporting quotients and complex numbers, I had to grapple with the fact that 1 (one) is a quotient (with denominator 1) and a complex number (with imaginary part 0). I solved it by defining the functions and operators taking a certain type and coercing the arguments to that type. One example, the logarithm can take complex numbers. If I had a quotient argument, I coerce it to a complex number before passing it to the logarithm.

However I assumed that this is only a problem in programming languages. I am a bit surprised that mathematics also seems to be affected. I am going to study it a bit.

Practical mathematics mostly isn't affected. That's what the earlier commenter was referring to with Tao's stages of maturity.

In the pre-rigorous stage, you don't know it's an issue. In the rigorous stage, you know it's an issue. In the post-rigorous stage, you know it's not an issue (i.e. you know you know how to write down all the details if you needed to, and you know it will all work how you might hope it would, and so you don't need to).

I think the magic word is: isomorphism!

An isomorphism is a way to relate two different sets such that each element is paired with exactly one in the other set such that it does not matter if you do operations before or after.

In my calculator the set of reals is isomorph to the set of complex numbers with imaginary part zero:

    ℝ ⬄ { c | c ∈ ℂ and im(c) = 0 }

So I can coerce to complex numbers without impunity because of that isomporphism! And I know it is an isomorphism because if adding two reals then coercing to complex is the same as coercing first then adding.

TIL: In a way mathematics has types like programming languages.

I hope I am not too far off here. I didn't look up anything, this all went into my head this morning.

This is sort of true, but there are isomorphisms which aren't "good enough" in some sense. E.g. if you're familiar with linear algebra, there's a thing called a dual space, which (for finite dimensions) is isomorphic to your space, but when you change coordinates, dual spaces change their coordinates backwards. Or for complex numbers, when you extend R by adding `i` (sometimes written C=R[i]), if you look carefully, you'll see that you could have instead added an element α = -i, and you'll notice that R[α] is isomorphic to R[i] in a way where the isomorphism maps R to itself; in a sense you can't tell whether you added i or -i, and this degree of freedom is important when studying field extensions.

The closest thing I'm aware of to "pretty much equal" is "unique up to unique isomorphism", so they may not be equal, but they're isomorphic, and there's no flexibility to make any choices of which isomorphism to use. But "isomorphism" also implies you have a particular context/structure in mind that you want to preserve, e.g. a set isomorphism (a bijection) may not be a linear isomorphism (~an invertible matrix). In practice, you may be working in multiple contexts at once, so you invent Functors which map one type of morphism to another, and now you care about Categories.

To expand: they're "equivalence classes". The digit 1 represents a value, in the same equivalence class as 1/1, 2/2, 1.0, 1+0i, {0|}, 1.0+0i+0j+0k, etc. ad infinitum.

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.

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.

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

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.

I have the naive feeling that early counting may have included 0 as a primitive right from the get-go. The need to say "nothing" seems pretty primal.

Zero entered western writing systems through India, with limited usage in math before that. It seems like it was invented/borrowed as part of switching from additive numbers (such as Roman numerals) to positional numbers.

"Nothing" as a concept always existed of course. But it wasn't considered a number, generally. Certainly no one counted "nothing, one, two", and even today natural language doesn't include "nothing" or some equivalent as a numeral noun.

You need to be careful about the phrase “considered a number” since I believe one, or unity, was also not considered a number by some ancient civilisation - i.e. a number was only multiple copies of unity.

[I believe this YouTube video goes into more detail in its discussion of why 1 was not considered Prime in the ancient world: https://youtu.be/R33RoMO6xeA]

That's where I'm quite skeptical. Imagine you are in charge of trade or rationing important village resources in the winter. It just seems to me almost necessary that people would have a way to symbolically indicate that all the sheep are gone. As opposed to just not having any symbol for that at all.

> There is an infinite chain of supersets of the rational numbers, real numbers, etc.

No you only do it for all the sets (of numbers) that you are currently working with.

You can work with infinitely many such sets at a time.

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

Exactly what we did in the Analysis I course I attended during my bachelor: defined the reals axiomatically, and the N as smallest inductive(?) subset containing 0.

Satisfactory or not, it worked well for the purpose. And I actually liked this definition, if anything because it was original. Mathematical definitions don't need to have some absolute philosophical value, as long as you prove that yours is equivalent to everyone else's it's fine.

> as long as you prove that yours is equivalent to everyone else's it's fine

That’s exactly the point I was making in the first place.

“Unsatisfactory” just means “unsatisfactory” in the sense that some mathematicians out there won’t be able to use your definitions and still get the subset property. This means that you are, in all realities, forced to deal with the separate notions of “equivalence” and “equality”. Which is what the article is talking about—all I’m really saying here is that you can’t sidestep equivalence by being clever.

You're not redefining anything; you're adding a relationship.

Another way to see it is to prepend every mathematical text involving ℤ with "for every ℤ such that [essential properties omitted]", so that you can apply it to several definitions of ℤ, rather than awkwardly redefining it after the fact. This is the mathematical equivalent of "programming to the interface", and is actually how mathematics are often formalized in modern proof assistants: as huge functors that abstract these details away.

This means similar to duck typing?

You can't do this in general, and everywhere, so it's still not rigorous. Consider the embedding of the nats into the reals, where the reals are defined as a subset of the binary sequences (e.g. as the usual infinite binary expansion for (0,1] choosing those that do not terminate in the zeros sequence, but prefix with a Elias-gamma-coded, zigzag-encoded integer). But the usual definition of sequence is as a function from the nats; so are you again going to redefine your reals in terms of that?

In the end you still need to maintain a correspondence between the embedding and the original set as in the typical way where you do that and consider the subset notation as a shorthand that requires you to "lift" or "wrap" through the correspondence wherever necessary.

I don't think you can define the reals as a mapping from natural numbers, reals are famously not countable.

You can't map the natural numbers to the set of real numbers, but you can map the natural numbers to the fractional part of a single real number.

How would this work when mapping them to the fractional part of the real number 2 ?

Collapsing a countably infinite set to 0 doesn't seem useful or reversable.

The integer part is easy, since we already have the integers. Once you have D=[0,1), then you can define R=ZxD. That is to say, this definition of R seperates out the integral and fractional components of every real number.

fun n => 0

I'm not sure what you're trying to disagree with here.

Fortunately functions from the natural numbers are not countable either. This is Cantor's theorem.

I'm not a set-theorist, but a set-theorist friend of mine once taught me that you can turn a countably-infinite set (such as the integers) into an uncountably-infinite one (like the reals) by applying the 'power set' operation (the set of all subsets).

Not heaps sure what this really means with respect to whether 1 the integer is really completely related (as in, equal, or the-exact same-thing) to 1.0 the real though. Kinda seems like it might still need a bit more information to fully identify a real, even when it happens to be infinitely-close to an integer?

More generally, Cantor's diagonal argument shows that there is no surjective map of a set onto its powerset.

I think you misunderstood the parent comment. They're not talking about defining the reals by setting up a mapping where each real number corresponds to a unique natural number. They're talking about defining the reals by setting up a mapping where each real number corresponds to a unique mapping from the natural numbers to {0, 1} (i.e. a unique binary sequence). The set of all binary sequences is isomorphic to the power set of the natural numbers, which is uncountable.

It makes more sense to define it the other way around:

Q = Z u Q’, where Q’ is the set of all rational numbers that aren’t integers.

Redefining the smaller set can’t work because there may be more than one larger set, e.g. split complex numbers vs regular complex numbers. But you can define a larger set to strictly extend a smaller set.

What the fuck is silently redefined? That's very self-referential reasoning.

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

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_num...

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

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”

This is a construction. The notion is the same. Not all math need be constructive. This is an implicit bias in most theorem provers.

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.

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.

> up to isomorphism

Which is exactly the sort of more sophisticated notion of equivalence you end up needing in these cases.

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.

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?

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

Isn't that a bit metaphysical and open to interpretation? I would say R only meaningfully exists as defined. A mathematical "truth" is either an axiom or it has a proof?

(Not that I think that makes a difference for the original argument about 1)

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.

> You have to use a very funny notion of ⊂ for that to make sense

Are you claiming that ℤ ⊄ ℚ

This thread is wild.

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?

> 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."

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.

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.

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.

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.)

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.

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.

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.

What do you mean by "subtype"? Lean defines a thing calles `Subtype`, members of which are constructed from a value and a property.

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.

why would you say that this is a bad thing

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.

Cumbersome compared to what? Ignoring the issue entirely?

Cumbersome compared to just having ℕ ⊂ ℤ, instead of having a coercion c from ℕ to ℤ, with complicated algorithms of where to insert c automatically, and then hiding the result from you, because otherwise you would see with your own eyes what a mess you are in.

But with coercions you do have {↑n | n ∈ ℕ} ⊂ ℤ, which is the subtype that you really want!

The issue is that not all properties of subsets can be lifted to supersets. As an example from analysis, you can coerce the reals ℝ to the extended reals ℝ∞, but you lose some of your rewrite rules because you need to choose how to define edge cases like (∞ - ∞) in ℝ∞. Making these choices is common in mathematics (at least in analysis) and in pencil and paper proofs it's usually just handwaved away.

Using subtypes, a proof checker would have to be explicitly given which ambient superset you're going to rewrite something like ((a : ℝ) - (b : ℝ)) in... this is more or less the same as using coercions to distinguish between ℝ and {↑r | r ∈ ℝ} ⊂ ℝ∞ except with subsets type inference is way harder.

I'll admit that coercions are annoying, but subsets don't let you get around it: here there's an essential step up in complexity between sloppy pencil and paper proofs and verified code. Personally, I'm really interested in seeing how much of mathematical handwaving can be rigorously automated away. There's a lot of cool work in this area by I don't think the FM community has a definitive answer for it yet.

Let's be clear, I am not arguing for subtypes. Subtypes are a mess, that is why no type system supports them. I am arguing against any types at all. So type inference being harder is not a problem, because there won't be any type inference. I know, that is a tough pill to swallow, type inference is like a hard drug for computer scientists.

Subsets or subcollections, on the other hand, are fine. Of course you will have proof obligations, but that is not a problem, and automation can take care of most of this (note that automation is much more flexibel than hardcoded type inference).

Fair enough, I haven't used many proof assistants without dependent types, and I probably should.

Absolutely right. If you keep worrying about whether 1 is actually 1, you’ll never get any math done.

> 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_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, 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-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. )

You ellipsed ([...]) the "can assume" part of my statement. Every mathematician knows the different ways of constructing numbers. It really is a simple YES.

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.

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.

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.

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).

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.

"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").

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

I think every mathematician are aware of both of those perspectives, and uses whichever is more convenient at the moment.

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.

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

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_num...

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.

These are all constructions though. They don't say what the natural numbers are.

The natural numbers is a set with a starting element and that has, for each element, a thing immediately following.

Things like 0 in 3 make no sense since 0 refers to the first thing in whatever representation you have, not a particular one.

I love formal theorem proving and provers, but this shouldnt lead us to believe that the natural numbers are fundamentally any particular representation

N is defined by its properties not its representation.

> These are all constructions though. They don't say what the natural numbers are.

A construction is exactly what would tell you what they are.

> The natural numbers is a set with a starting element and that has, for each element, a thing immediately following.

OK, but, like, which one? There are lots of sets that this describes.

> Things like 0 in 3 make no sense since 0 refers to the first thing in whatever representation you have, not a particular one.

If 0 and 3 are sets then we can legitimately ask whether 0 is a member of 3 or not. If 0 and 3 aren't sets then what are they? If the natural numbers are a set then 0 and 3 should also be sets, since set theory only talks about sets.

> N is defined by its properties not its representation.

Then what is it? If you say it's a set with those properties, then it should be a set and we can ask set questions about it. If you say it's somehow all of the sets with those properties, or some other concept that somehow encompasses them, then you still haven't explained what it actually is.

Not a direct reply to your question, but it seems to me that GP is describing a "structuralist" view (cf. https://en.wikipedia.org/wiki/Structuralism_(philosophy_of_m..., on which I'd guess much has been written over the years (both for and against).

I think so yes.

The article here espouses a constructivist view of mathematics

While I like that view personally, I think it's wrong to act as if it's the only one like this article does.

Many people have different views.

If I choose to wear a fedora, is a fedora an essential part of who I am? Or an arbitrary choice that be changed?

This question goes back to Plato.

You use Von Neuman naturals. I use Peano naturals. Which are the real naturals? Can they both be the naturals, even though they are clearly different? The natural numbers are not any one construction. They are the abstract idea of whose properties are what all the constructiona have in common.

Math is like God. We use feeble human language to approximately talk about something that is beyond our ability.

Right and this is my point the view espoused in the article is not universal

> Math is like God. We use feeble human language to approximately talk about something that is beyond our ability.

That sounds like giving up. The approach the article is describing is a lot more satisfying - forming this concept of equivalence, and then using it to give genuine, rigorous answers to questions like:

> You use Von Neuman naturals. I use Peano naturals. Which are the real naturals? Can they both be the naturals, even though they are clearly different?

> OK, but, like, which one? There are lots of sets that this describes.

Any, and all. One can do the thinking without specifying what. I believe this is the notion of a 'universal property' in category theory.

> If 0 and 3 aren't sets then what are they?

I mean, if you want to give me a construct I would use, I'd say the following

0 = \s -> \z -> z 3 = \s -> \z -> s s s z

If you say that these are akin to church numerals, that is correct if you look at it as a lambda calc term. However I'm saying something much stronger than just a lambda calculus term. That's just my notation.

I'm saying that zero is the concept of taking two things (one an initial thing and the other a method to take one thing and get the next thing) and then returning the initial thing. While three is the concept of taking the same two things and then doing the method three times on the first thing. I used lambda notation because that is an easy way to convey the idea, not because that is what three is.

> Then what is it? If you say it's a set with those properties, then it should be a set and we can ask set questions about it. If you say it's somehow all of the sets with those properties, or some other concept that somehow encompasses them, then you still haven't explained what it actually is.

It's a set in the colloquial sense, not in the ZFC sense.

There's an idea of a thing, and then the definition of the thing. Both are valid in my mind.

For example, heat is the movement of atoms. It's also the energy in a thing. But it's also the feeling of hot that I cannot describe. It's also an idea in its own right. Things can be many things. There's an infinite hierarchy of description that one may apply to concepts, and, in my philosophy, at some level the description becomes unable to be expressed.

> One can do the thinking without specifying what.

After one has figured out a rigorous approach, one can generally ignore it in day-to-day work. But you need to have that foundation there or you can go horribly wrong. (Analogy: we don't generally think about limits when doing day-to-day calculus. But when people tried to do calculus pre-Weierstrass, unless they were geniuses they "proved" all sorts of nonsense and got crazy results).

> I believe this is the notion of a 'universal property' in category theory.

That's one of the good answers to this problem. But you still need the constructions (if only to prove that an object with the required properties exists at all) and you need a lot of the kind of work the article is talking about, where you establish that these different constructions are equivalent and you can lift all your theorems along those equivalences.

> I'm saying that zero is the concept of taking two things (one an initial thing and the other a method to take one thing and get the next thing) and then returning the initial thing. While three is the concept of taking the same two things and then doing the method three times on the first thing. I used lambda notation because that is an easy way to convey the idea, not because that is what three is.

OK but then what kind of things are these "concepts"? What kind of questions can and can't we ask about them? If you care about "what the natural numbers are" then these kind of questions are worth asking.

We must remember that these constructions retcon the actual human experience with numbers, which is firmly rooted in counting and measurement, that always come after this experiential basis. Formal definitions appear driven by an aesthetic consensus, mostly about minimalism and axiom flavor. Individual human experience with numbers reflects human history and at both scales 'counting and measurement' is more fundamental in the sense that it always comes first, and therefore all constructions derive from it, must maintain consistency with it, and conflicts must be resolved within it, and it is safe to ignore inconsistencies that can't be expressed within it.

In those terms, the foundations (of any topic or field) are never fundamental. I think people in this thread are using a different meaning of "fundamental".

Without formal constructions, humans have a nasty habit of proving things that wrong or not even wrong. Our ancestors dealt with this problem in the 19th Century by creating tools to help distinguish truth from balderdash.

Your statement is consistent with my point which I mean to point out the psycho-social origin of such constructions and therefore the limits of their utility. I do not say they are not useful at all.

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

> ℤ ⊂ ℝ 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.

I think he literally just demonstrated the problem you were trying to illustrate about software provers

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

Reply on news.ycombinator.com