Hacker News Reader

Comment by auggierose | Hacker News Reader

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

View on HN

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?

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.

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)

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.

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.

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.

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.

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.

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.

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.

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

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.

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

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

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?

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.

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.

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.

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

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.

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.

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.

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.

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

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

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”

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.

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.

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

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.

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.

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.

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

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

Reply on news.ycombinator.com