This is probably better known here under the name of implicit type conversions. Strictly speaking, the rational number 1 is not the same as the integer 1; we just have a conversion map that preserves all the relevant properties. It's all fun and games until there are 1000 types and 10000 conversion maps involved and the relevant diagrams no longer commute (i.e., it depends what order you go).
At the risk of utterly derailing this with irrelevant discussion: path-dependent systems are particularly tricky for some people IMHO. I think in a more state-based way, and my first rigorous dive into path-dependent calculation was during my chemical engineering degree -- I learned to be extremely vigilant about memorizing what was path-dependent and triple-checking if that affected the situation I was calculating.
I do wish there was more rigorous exposure to them at lower levels of education and younger age. Because while I'm perfectly capable of handling path-dependent systems with proper focus and effort, my brain doesn't feel "native" when deriving solutions around those spaces - it feels similar to being "fluent enough" in another language. I feel this way about a lot of things -- I really feel I'd have been happier and more fulfilled if I'd been immersed in super rigorous first-principles education beginning around age 8-9. I didn't do well with things like "memorize this procedure for doing long division" and did much better with conceptual derivations of physics/math/science/historical arcs, etc.
The problem is that no one thinks of type conversions as taking any explicit paths! It's one thing to view the actual process of long division as path-dependent (something everyone who learns about Gröbner bases is familiar with, as at the right level of generality even the result is path-dependent); it's another thing to apply the same intuition to the way the inputs are parsed. (You said divide 3 by 2 with remainder? Sure, the quotient is 3/2 and the remainder is 0. Problem?)
> The problem is that no one thinks of type conversions as taking any explicit paths!
Indeed. This is super surprising to me and I’m adding the topic to my “study” list. I had no idea until today - I easily could imagine it’s possible if some of the type conversions are “lossy” (e.g. maps to lists), but I have a strong feeling that simpified lossy conversions are not what is being referenced.
Most of Buzzard's examples are indeed lossless (even bijective) conversions, but the notation mathematicians use (and programming languages often support) makes it look like they are completely absent, which comes back to bite you. In mathematics, it bites you when you want to actually compute your function and realize you don't remember how all those canonical arrows go. In programming, it bites you when the default conversions the compiler inserts aren't the ones you meant.
Or when your formulas on Google sheets start failing because you do 1-1 and the result is not 0, and then you spend 30 minutes creating new sheets, searching the web and double checking everything, until you realize that the value on the cell wasn’t 1, but 1.
Now I noticed that the period at the end of the paragraph is a bit unfortunate
The value was 1. which I guess is shorthand for 1.0 and it’s technically not the same value as 1
On top of that, sometimes values like 0.961727 will be shown as 1, so sometimes you think that the value in the cell you are referring to is a 1 but instead it’s something close to it
In particular I was making a list of array positions from 1 to 32 and calculating x,y coordinates from the position using the formulas (x = (i-1) % width, y = (i-1)/width)
Some of the coordinates were wrong, and it was because the i values were not integers, which I couldn’t tell just by looking at the sheet, and only realized it when double clicked on the cells
It's frustrating that there isn't an easy way to see the "canonical" value and format of a cell (in Sheets or Excel).
Just looking at a cell, it's not trivial to see if it's the number 1 or the string 1 (you can enter text by using a leading apostrophe, but that's not the only way to get text in a cell!). Numbers and strings have different alignments by default, but that can be overridden. The numeric value of the string 1 is 0 if you're using the SUM formula, but it's 1 if you use +. In other words, =A1+A2 does not necessarily equal =SUM(A1:A2)
Then you can format numbers however you like. For example, dates are stored in spreadsheets as days since an epoch (not the Unix epoch). So you can have the number 2 in a spreadsheet cell, then format it as a date, but just the day of the month, and it can appear as 1.
There's rounding, which bit you. 0.95 can appear as 1 if you display fewer decimal places.
Finally, there's the fact that the calculation is done like IEEE 754. Programmers are used to floating point numbers and the fact that properties like associativity don't apply, but that's not obvious to everyone.
You definitely know a lot about mangling data with spreadsheets!
> Programmers are used to floating point numbers and the fact that properties like associativity don't apply, but that's not obvious to everyone
One of my first programming assignments in college was to simulate a pool table. I had to go ask the TA what the hell was wrong with my code, the balls would never bounce because their distances to anything were never 0… fun times
In other areas, one might compare code jurisdictions, where presumably all the legislative clauses share a common vocabulary (and probably even conceptual framework), with common law jurisdictions, where all the legislative clauses occur in different centuries and thus one adds "picking a parallel transport" between the legal languages of the times (and jurisdictions) to the difficulties of adjudication.
I was thinking in much more abstract terms. You have information from a webflow, at some point converted to an XML message, converted to database entry, again to a JSON document, combined with an Azure workitem, then sent to Salesforce.
At any one point the data can interact with other systems, travel through codebases each seeing the data through their types, legacy APIs, the same-(ish) new-(ish) RPC API and in each service the data is represented in its own internal quirky way.
Sure, throw Go in that mix, hell at this point the more merrier! :)
This doesn’t sound right to me. The rational numbers are a superset of the integers. We know that there’s only one 1 in the rational numbers, then it must be the same 1 object as the 1 in the integers.
The statement “3/3 is in Z” is true. There’s no conversion happening: 3/3 is a notation for 1, just like 0.999… is a notation for 1. Many notations, but only one 1 object.
The case of R x R^2 = R^3 is different because the Cartesian product is defined to produce a set of ordered pairs. So it cannot give rise to a set of triples any more than a dog can give birth to a cat. So either x is not a Cartesian product or = is isomorphism not equality.
> We know that there’s only one 1 in the rational numbers, then it must be the same 1 object as the 1 in the integers.
> The statement “3/3 is in Z” is true.
make it sound very trivial while in reality it is not. I do not quite understand your example with R^3 but the defined applies equally to your statements. There are many ways to define and think about the objects you mentioned -- there is not one single truth. Unless you are a devoted platonist, in which case, it's still like your opinion, man.
How do you "extend" Z (what are you adding to it)? How do you prove there is a field containing Z? Assuming you are working in ZFC, what is an example of an element of Q? What is an example of an element of Z?
One way to do things is to define N as von Neumann ordinals:
Then you define Z as an equivalence relation of NxN by the equivalence (a,b) ~ (c,d) iff a+d=c+b. This means each integer is itself an infinite set of pairs of natural numbers.
Then you define Q as an equivalence relation of ZxZ\{0} by (a,b) ~ (c,d) iff ad = cb. Again, each rational is now an infinite set of pairs of integers.
The point of the OP post is that we want to define things by their properties, but then we are defining what a set of rational numbers is, not what the set of rational numbers is, and we need to make sure we do all proofs in terms of the properties we picked (e.g. that Q is a field, there is a unique injective ring homomorphism i_ZQ: Z->Q, and if F is a field such that there is an injective ring homomorphism i_ZF: Z->F, then there is a unique field homomorphism i_QF: Q->F such that i_ZF = i_QF after i_ZQ) rather than relying on some specific encoding and handwaving that the proof translates to other encodings too. This might be easier or harder to do depending on which properties we use to characterize the thing, and the OP paper gives adding inverses to a ring as one of its examples in section 5 ("localization" is a generalization of the process of constructing Q from Z. For example, you could just add inverses for powers of 2 without adding inverses of other primes), proposing a different set of properties that they assert is easier to work with in Lean.
0.999… always reminds me of my favorite definition of the real numbers:
“A real number is a quantity x that has a decimal expansion
x = n + 0.d₁d₂d₃…, (1)
where n is an integer, each dᵢ is a digit between 0 and 9, and the sequence of digits doesn't end with infinitely many 9s. The representation (1) means that
n + d₁/10 + d₂/100 + ⋯ + dₖ/10^k ≤ x < n + d₁/10 + d₂/100 + ⋯ + dₖ/10^k + 1/10^k
for all positive integers k.”[1]
Defining the reals in terms of binary expansion is left as an exercise for the reader[2].
[1] Knuth, The Art of Computer Programming, Volume 1, Third Edition, p. 21.
In the formalization of mathematics, things are built up structurally. Zero is the empty set. Natural numbers are sets that contain smaller natural numbers. Integers are pairs of natural numbers under an equivalence relation (a,b) ~ (c,d) if a + d = c + b. Rationals are pairs of integers under the equivalence relationship as above but if a * d = c * b. Reals are bounded sets of rationals (e.g. all the rationals q such that q * q < 2). Complex numbers are pairs of reals with addition and multiplication defined with i^2 = -1. Functions are really large sets with ordered pair (x,y) in the set f means f(x) = y. Etc.
Inclusions are a form of isomorphism. In the more common developments of elementary arithmetic, Q is constructed from Z, and in particular the subset of integral rational numbers are technically a different ring from Z. The conversion Z \to Q in particular is an isomorphism from Z to that subset.
Type conversions in every day programming languages though sometimes not only fail to be surjective, they can also fail to be injective, for example int32 -> float32.
type-conversions and "implicit isomorphisms" differ because the former does not need to be invertible, but they agree in that they are implicit maps, that are often performed without thought by the user. So I think that the type-conversions analogy is pretty good in that it captures the idea that implicit conversions, when composed in different ways from A to B, can arrive at various values, even if each stage along the way the choices seemed natural.
Even there, it would help to not apply the zero numerator equivalence class too early.
I.e. 2/3, 2/5, 2/7 are the numbers that divide 2 to get 3, 5 and 7 respectively.
Likewise, with full consistency, 0/1, 0/2, 0/3 cannot be reduced using common factors (the core equivalence for ratios), so have different ratio normal forms, and are the numbers that when they divide 0 produce 1, 2, and 3 respectively. All consistently.
The advantage of not applying zero numerator equivalence too early, is that you get reversibility, associativity and commutivity consistency in intermediate calculations even when zeros appear in ratios.
You can still apply zero numerator ratio equivalence to final values, but avoid a lot of reordering of intermediate calculations required to avoid errors if you had applied it earlier.
Of course, if you are coding it doesn't help that you are unlikely to find any numerical libraries, functions or numeric data types, that don't assume division by zero is an error, inf, or NaN, and that all zeros divided by non-zero numbers are equivalent to 0. So you simply can't get the benefits of holding off on that equivalence.
You have to do a lot of reasoning and reordering to ensure generally correct results, as apposed to "I am sure it will be fine" results.
I find it very surprising that this separate treatment of factor reduced equivalence, and zero numerator (and zero denominator) equivalences, on ratios, is not taught more explicitly. They are very different kinds of equivalence, with very different impacts on calculation paths.
I was actually toying with writing a rational number library going in the direction you sketch out. My inspiration was a trick in computational geometry for dealing with points at infinity. I think it's called homogeneous coordinates.
My point was to treat both p and q in p/q as symmetrically as possible.
Oh, I remember now: the motivating example was to write a nice implementation of an optimal player for the 'guessing game' for rational numbers.
One player, Alice, commits to a (rational) number. The other player, Bob, makes guesses, and Alice answers whether the guess was too high, too low or was correct. Bob can solve this in O(log p + log q). And the continued-fraction-based strategy Bob wants to use is generally symmetrical between p and q. So I was looking into expressing the code as symmetrically as possible, too.
If you start saying 0/x is 0 then of course 0/2 and 0/3 are zero. (Or equivalently that 0 x 2 = 0 x 3 = 0.) But that is an entirely different equivalence from factor reduction.
If you don’t start with that assumption and reduce 0/2 and 0/3 only according to shared factors, you find that all three numbers, 0, 2, and 3 can only be factored as a product of 1 and themselves.
(Thus a slightly generalized version of primes, for whole numbers instead of just natural numbers.)
So 0/2 and 0/3 are completely factor reduced.
The equivalence of 0/x = 0/2 = 0/3 = 0/1 = 0 is a separate equivalence. One which is not reversible, I.e. it erases information, and may break commutivity requiring special handling (exception generation, NaN representation, or calculation reordering, etc) if it is applied during intermediate calculations.
If you don’t apply the zero equivalence’s until a final value is calculated, you will always get the same answer, but will have avoided a need for special handling of intermediate calculations.
For instance, an intermediate division by zero followed by a multiplication of zero will cancel, avoiding any need to reorder calculations and yet resulting in the same final answer.
Note how your parent comment has specified "rational" 1 and "integer" 1. They use the symbol 1 for two similar concepts: We all "know" that 1 + 1 = 2 and 1.0 + 1.0 = 2.0. I have deliberately specified 1 for an int and 1.0 for a rational. Now we have two different representations for two very similar but not identical concepts.
At which point does 1 + a tiny amount cease to be an integer? By definition that tiny amount can have any magnitude and 1 plus anything will cease to be an integer. That is the property that defines an integer. Integers have subsequent "behaviours" that other types of numbers might lack.
You have picked zero/0. Now that is a sodding complicated concept 8) There are lots of things called zero but no more nor less than any other.
Zero might be defined by: 1 - 1 = 0. I have £1 in my bank account and I pay out £1 for a very small flower, my bank balance is now £0. Lovely model, all good except that interest calcs intervened and I actually have a balance of £0.00031. Blast. My pretty integer has morphed into a bloody complicated ... well is it a rational thingie or a ... what is it?
Now I want to withdraw my balance. I put a shiny £1 in, bought something and I have some change. What on earth does a 0.031p coin look like? Obviously, it doesn't exist. My lovely integer account has gone rational.
Symbols mean what we agree on with some carefully and well chosen language. Mathematicians seem to think they are the ultimate aces at using spoken and written language to make formal definitions, derivations and so on. That is a bit unfair, obviously. We all believe that what we think is communicable in some way. Perhaps it is but I suspect that it isn't always.
Have a jolly good think about what zero, nothing, 0 and so on really mean. Concepts and their description to others is a really hard problem, that some funky symbols sort of helps with.
Yes there are loads of things called zero. If I had to guess: infinitely things are zero! Which infinity I could not say.
It's also a complex number, a Unicode character, an ASCII character, an Extended ASCII character, a glyph, the multiplicative identity element, a raster image, ...
The GP point is correct; we implicitly convert between all these representations naturally and quickly, but there are interesting branches of mathematics that consider those conversions explicitly and find nuances (eg, category theory).
All the examples of shadows mentioned by Douglas in the video [0]:
Traditional Shadow from Sunlight: A tree casting a shadow in bright sunlight during the summer, characterized by the typical darkening on the ground.
Snow Shadow: Occurs in winter when a tree intercepts snowflakes, resulting in an absence of snow under the tree despite being surrounded by snow. This is likened to a shadow because it mimics the visual absence typical of shadows, even though caused by a different kind of blockage.
Rain Shadow: Explained with the example of the Cascade Mountains, where the mountains block rain clouds leading to dry conditions on the leeward side, effectively creating a "shadow" where rain is absent due to the geographical barrier.
Car Shadow by a Truck: Described during highway driving, where a large truck casts a "shadow" by preventing cars behind it from passing. This "shadow" is the area in front of the truck where cars tend to stay clear due to the difficulty in passing the truck.
Shadow Cast by England Due to the Gulf Stream: This is a metaphorical shadow, where England blocks the warm Gulf Stream from reaching certain areas, resulting in colder temperatures on one side, while allowing it to pass above to northern Norway, warming it. This is referred to as the "shadow of England" on the coast of Norway, influenced by the flow of water rather than light.
These examples use the concept of "shadow" in various physical and metaphorical contexts, showing disruptions in different types of flows (light, snow, rain, traffic, and ocean currents) caused by obstructions.
For example, the "2" in "2π" is not the same type of "2" as in x^2 or 2x generally. Yet, physicists (to pick a random group) will blend in these factors, resulting in nonsense. As a random example, one of the Einstein field equations has "8π" in it. Eight what!? What aspect of the universe is this counting out eight of -- a weirdly large integer constant? This actually ought to be "4(2pi)", and then "4" is the number of spacetime dimensions, which makes a lot more sense.
Similarly, in at least one place the square of the pseudoscalar (I^2) was treated as a plain -1 integer constant and accidentally "folded" into other unrelated integer constants. This causes issues when moving from 2D to 3D to 4D.
These examples miss the mark somewhat. The "2" in "2π" can mean several things (the nonnegative integer 2, the integer 2, the rational 2, the real 2) that are all commonly identified but are different. The "2" in "x^2" usually means the nonnegative integer 2. The "2" in "2x" can usually mean the nonnegative integer or the integer 2, but also the other 2's depending on what x is. The problem is not that the meaning of 2 varies across different expressions, but that it can vary within each single expression.
The best example is perhaps the polynomial ring R[x][y], which consists of polynomials in the variable y over the ring of polynomials in the variable x over the real numbers. Any algebraist would tell you that it is obviously just the two-variable polynomial ring R[x, y] in disguise, because you can factor out all the y-powers and then the coefficients will be polynomials in x. But the rings are very much not the same at the level of implementation, and every time you use their "equality" (canonical isomorphy), you need to keep the actual conversion map (the isomorphism) in the back of your mind.
Haskell shows (one way of) how you can have numerical literals like 2 that can be used with many different types, but still be strongly statically typed.
That by itself isn't a problem. But making all the other confusions you mention is a problem.
Saying 1 is both an integer and a rational number is wildly different from saying it is both an integer and an ASCII character. Z is a subset of Q. ASCII characters don’t overlap with either.
When you construct numbers using sets under ZFC axioms or inside lambda calculus what you get is representation. But 1 is just 1.
Your keyboard has a button with ‘1’ printed on it. When you push that, you don’t always get an integer or a rational number. You can convert what you get to either. So there must be overlap with ASCII somehow?
By any common set-theoretic construction of Q (e.g., equivalence classes of integer pairs under cross-multiplication), 1 as an element of Z is not literally an element of Q: 1 ∈ Q merely corresponds to 1 ∈ Z, and this correspondence is carefully designed to preserve the ring operations of Z within a certain subset of Q. In this case, the distinction is so negligible that eliding it is harmless, but the whole point of the article is that such elisions can become harmful in more complex constructions.
1 ∈ Z and ASCII '1' can similarly be seen as corresponding in terms of having the same glyph when displayed. But of course, there are far fewer meaningful operations common to the two.
I am not sure I understand what you mean by “literally” here. For sure, if you use Zermelo–Fraenkel set theory as the foundation of mathematics, as is commonly done, every mathematical object is a set. The first definition of 1 encountered in that setting is the singleton set {0}, where 0 is the empty set. (And 2={0,1}, 3={0,1,2} and so forth – you get the picture.)
This is precisely the sort of thing this is all about: The natural numbers are uniquely described up to unique isomorphism by some variant of the Peano axioms after all.
Ah, that depends what the meaning of “is” is, does it not?
On a more serious note, if you are of a certain philosophical bent you may believe that the natural numbers have an existence independent of and outside of the minds of humans. If so, 1 is presumably not a set, even if we don’t fully understand what it is. I certainly don’t think of it as a set on a day to day basis!
But others may deny that the territory even exists, that all we have are the maps. So in this one map, 1 is a set containing zero, but in that other map, it is something different. The fact that all the different maps correspond one-to-one is what counts in this worldview, and is what leads to the belief – whether an illusion or not – that the terrain does indeed exist. (And even the most hard nosed formalist will usually talk about the terrain as if it exists!)
But this is perhaps taking us a bit too far afield. It is fortunate that we can do mathematics without a clear understanding of what we talk about!
If there are many different ways to represent what something 'literally is', then how do we know for sure that ASCII '1' isn't a true representation of the literal number 1, just considered under different operations? We can say that 1 + 1 + 1 ≠ 1 (in Z), and we can also say that 1 + 1 + 1 = 1 (in Z/2Z): the discrepancy comes from two different "+" operations.
For that matter, how do we know what infinite sets like Z and Q 'literally are', without appealing to a system of axioms? The naive conception of sets runs headlong into Russell's paradox.
But the integers are a subset of the rationals, which are a subset of the reals, which are a subset of the complex numbers. Looking only at the objects and not their operations 1 (integer) = 1 (rational) = 1 (real) = 1 (complex). Moreover, when we do account for the operations, we also see that 1 + 1 = 2 and 1 * 1 = 1 in every one of those systems. This isn't just a coincidence, of course; it's by design.
However, the way you arrive at 1 + 1 = 2 is not the same (though I suppose you could short-circuit the algorithm). Rational addition requires finding a common denominator, while integer addition doesn't. They achieve the same result when the inputs are integers, and again this is by design, but the process isn't the same. Ditto real addition vs. rational and complex addition vs. real.
In higher-level mathematics, the operations on the objects become definitional. We don't look at just a set of things, we look at a set of things and the set of operations upon those things. Thus "1 with integer addition and integer multiplication" becomes the object under consideration (even if it's just contextually understood) instead of simply 1. This is why they don't satisfy higher-level notions of equivalence, even if they intentionally do satisfy simple equality as taught in grade school.
Of course, the entire point of the submitted paper is to examine this in detail.
> But the integers are a subset of the rationals, which are a subset of the reals, which are a subset of the complex numbers.
It depends on definitions, and, in some sense, the point of the common approach to mathematics is not just that one does not, but that one cannot, ask such questions. One approach is to look at natural numbers set theoretically, starting with 0 = ∅; to define integers as equivalence classes of pairs of natural numbers; to define rational numbers as equivalence classes of certain pairs of integers; and to define real numbers as equivalence classes of Cauchy sequences of rational numbers. In each of these cases there is an obvious injection which we are used to regarding as inclusion, but most of mathematics is set up to make it meaningless even to ask whether the natural number 1 is the same as the integer 1 is the same as ….
That is to say, if you're working on an application where encoding details are important, then you can and will ask such questions; but if I am writing a paper about natural numbers, I do not have to worry about the fact that, for some choice of encoding, the number 2 = {∅, {∅}} is the same as the ordered pair (0, 0) = {0, {0, 0}} = {∅, {∅}}, and in fact it is meaningless to test whether 2 "equals" (0, 0). The philosophy of studiously avoiding such meaningless questions leads some to avoid even testing for equality, as opposed to isomorphism; failing to do so used to be referred to in category-theoretic circles as "evil", although, as the nLab points out if you try to go to https://ncatlab.org/nlab/show/evil , it seems common nowadays to avoid such language.
This is not the point of the article. Even at the level of the objects themselves, 1 : integer is not 1 : rational. The latter is an ordered pair (1, 1) of two coprime positive integers, or an equivalence class of ordered pairs up to cancelling. Some ugly hackery is required to really make the integers equal to their respective rationals, and its consequences aren't great either (just imagine that some rationals are pairs while others are not -- that's what you get if you forcibly replace the rational k/1 by the integer k), and no one wants to do that.
There are multiple things that we denote using a particular symbol: 1. 1 in and of itself is not a single concept. You could replace the symbol 1 with any other, even the sound of a fart and the concepts still remain the same. Given that we somehow agree that a fart sound shall be the way that we refer to a concept/object/thing.
It's a largely useful conceit to use 1 for all of those objects and more besides. It makes talking about them easier but we do have to be careful to use the correct rule-set for their manipulation.
I would personally prefer to see 1.0 for "rational 1" or perhaps 1. but that would require a convoluted sentence to avoid 1. being at the end of the sentence, unless we allow for: 1.! Well, that would work but what about 1.? Oh for ffs, I mean: 1..
One notes that one's own ones may not be the same as one's other ones.
If only I could spin "won", "own" and perhaps "wan" into that last sentence! ... Right, I've wedged in own. Needs some work 8)
Well, you give give 1.0 for the rational one. But what about the real or complex one? Or what about the Gaussian Integer? What about the 2-adic one, or the 3-adic one, or any other p-adic one? What about the different kinds of floating point numbers?
I don't think the rational one is special enough that we need to different notation just for her and for her alone. (Though that specific distinction can make sense in some contexts. Just not universally.)
I'm typing this after reading their section on page 6 about the "pentagon axiom". They write that RxR^2, R^2xR, and R^3 are isomorphic, but not literally equal under different constructions, because (a,(b,c)) is different from ((a,b), c), and that this is a problem. I feel like math kinda gets this wrong by treating sets as meaningful objects on their own. Physics gets it closer to correct because it tries to be "covariant", where the meaningful answers to questions have to either have units on them or be totally unitless e.g. irrespective of coordinate system.
The two spaces Rx(RxR) and (RxR)xR have many isomorphisms between them (every possible coordinate change, for instance). But what matters, what makes them "canonically isomorphic", is not isomorphisms in how they are _constructed_ but in how they are _used_. When you write an element as (a,b,c), what you mean is that when you are asked for the values of three possible projections you will answer with the values a, b, and c. Regardless of how you define your product spaces, the product of (a), (b), and (c) are going to produce three projections that give the same answers when they are used (if not, you built them wrong). Hence they are indistinguishable, hence canonically isomorphic.
This is exactly the way that physics always treats coordinates: sure, you can write down a function like V(x), but it's really a function from "points" in x to "points" in V, which happens to be temporarily written in terms of a coordinate system on x and a coordinate system on V. We just write it as V(x) because we're usually going to use it that way later. Any unitless predictions you get to any actual question are necessarily unchanged by those choices of coordinate systems (whereas if they have units then they are measured in one of the coordinate systems).
So I would say that (a,(b,c)) and ((a,b), c) are just two different coordinate systems for R^3. But necessarily any math you do with R^3 can't depend on the choice of coordinates. There is probably a way to write that by putting something like "units" on every term and then expecting the results of any calculation to be unitless.
This is exactly the "specification by universal property" that the author is talking about. In your case, it's saying "a 3-dimensional vector space is a vector space with three chosen vectors e, f, g and three linear maps x, y, z such that each vector v equals x(v) e + y(v) f + z(v) g". But as the author points out, not everything follows from universal properties, and when it does, there is often several universal properties defining the same object, and that sameness itself needs to be shown.
Yes, I know it's the meaning of it, but I'm saying that the presence of "units" allows you to sort of... operationalize it? In a way that removes the ambiguity about what's going on. Or like, in theory. I dunno it's a comment on the internet lol.
I think that is due to insufficient imaginativeness. For example, energy and work are the same units but energy is an absolute quantity while work is a delta. So arguably work should be a sort of tangent element of the energy, rather than the same thing. There's no distinction in flat space but if you e.g. changed coordinates such that energy was on the surface of a sphere, then work is a spherical displacement instead, which is a totally different class of objects.
Likewise, torque is only in the same units because we don't regard radians as a unit, but we should. They are distinctly different.
Radians can be seen as a ratio of two lengths, the length of your arc and the length of the circumference of the unit circle. All units cancel in such ratios.
> There's no distinction in flat space but if you e.g. changed units such that energy was on the surface of a sphere, then work is a spherical displacement instead, which is a totally different class of objects.
Basically, how much you _want_ to encode in your type system depends on the needs of your application. (Approximately all type systems can be made to work for all applications. But they differ in the degree of convenience and error proneness.)
You use R^3 in your example of why coordinates don't matter. R^3 can be covered by one chart. Maybe your argument would be more convincing if you pick a different manifold. I have no idea what your complaint is otherwise.
I'm not talking about charts of R^3; I'm talking about the different isomorphic constructions of products like ((a, b), c) and (a, (b, c)) as being a sort of 'choice of coordinate system' on the isomorphic class of objects.
For this particular question we have a great answer in the form of homotopy type theory. It handles all the complications that the author mentions. This is one of the reasons type theorists were excited about HoTT in the first place.
The only problem is that the author is working in Lean and apparently* dismissive of non-classical type theory. So now we're back to lamenting that equality in type theory is broken...
*) I'm going by second hand accounts here, please correct me if you think this statement is too strong.
> For this particular question we have a great answer in the form of homotopy type theory. It handles all the complications that the author mentions. This is one of the reasons type theorists were excited about HoTT in the first place.
Arguably, Homotopy type theory still doesn't solve the problem, because while it strengthens the consequences of isomorphism it doesn't distinguish between "isomorphism" and "canonical isomorphism", whereas (some?) mathematicians informally seem to think that there's a meaningful difference.
> The only problem is that the author is working in Lean and apparently* dismissive of non-classical type theory. So now we're back to lamenting that equality in type theory is broken...
In my opinion, Lean made a number pragmatic choices (impredicative Prop, non-classical logic including the axiom of global choice, uniqueness of identity proofs, etc.) that enable the practical formalization of mathematics as actually done by the vast majority of mathematicians who don't research logic, type theory, or category theory.
It's far from established that this is possible at all with homotopy type theory, yet alone whether it would actually be easier or more economical to do so. And even if this state of affairs is permanent, homotopy type theory itself would still be an interesting topic of study like any other field of mathematics.
"Canonical" refers largely to the names we give to things, so that we maximize the extent to which an isomorphism maps the object named A in X to the object named A in Y. And also to choosing an isomorphism that embeds in a different isomorphism (of superstructures) that isn't strictly the topic of the current question.
I don't think anyone thinks canonical isomorphisms are mathematically controversial (except some people having fun with studying scenarios where more than one isomorphism is equally canonical, and other meta studies), they are a convenient communication shorthand for avoiding boring details.
I think the original author makes a good case that a) the shorthand approach isn’t going to fly as we formalise b) different mathematicians mean different things by canonical and these details matter when trying to combining results and that therefore 3) it would be better to provide a proper definition of what you’re talking about and give it an unambiguous name.
> Please don't comment on whether someone read an article. "Did you even read the article? It mentions that" can be shortened to "The article mentions that".
> it doesn't distinguish between "isomorphism" and "canonical isomorphism"
You can distinguish these concepts in (higher )category theory, where isomorphisms are morphisms in groupoids and canonical isomorphisms are contractible spaces of morphisms. These sound like complicated concepts, but in HoTT you can discover the same phenomena as paths in types (i.e., equality) and a simple definition of contractibility which looks and works almost exactly like unique existence.
> In my opinion, Lean made a number pragmatic choices (impredicative Prop, non-classical logic including the axiom of global choice, uniqueness of identity proofs, etc.) that enable the practical formalization of mathematics as actually done by the vast majority of mathematicians who don't research logic, type theory, or category theory.
The authors of Lean are brilliant and I'm extremely happy that more mathematicians are looking into formalisations and recognizing the additional challenges that this brings. At the same time, it's a little bit depressing that we had finally gotten a good answer to many (not all!) of these additional challenges only to then retreat back to familiar ground.
Anyway, there were several responses to my original comment and instead of answering each individually, I'm just going to point to the article itself. The big example from section 5 is that of localisations of R-algebras. Here is how this whole discussion changes in HoTT:
1) We have a path R[1/f][1/g] = R[1/fg], therefore the original theorem is applicable in the case that the paper mentions.
2) The statements in terms of "an arbitrary localisation" and "for all particular localisations" are equivalent.
3) ...and this is essentially because in HoTT there is a way to define the localisation of an R-algebra at a multiplicative subset. This is a higher-inductive type and the problematic aspects of the definition in classical mathematics stem from the fact that this is not (automatically) a Set. A higher-inductive definition is a definition by a universal property, yet you can work with this in the same way as you would with a concrete construction and the theorems that the article mentions are provable.
---
There is much more that can be said here and it's not all positive. The only point I want to make is that everybody who ever formalised anything substantial is well aware of the problem the article talks about: you need to pick the correct definitions to formalise, you can't just translate a random math textbook and expect it to work. Usually, you need to pick the correct generalisation of a statement which actually applies in all the cases where you need to use it.
Type theory is actually especially difficult here, because equality in type theory lacks many of the nice properties that you would expect it to have, on top of issues around isomorphisms and equality that are left vague in many textbooks/papers/etc. HoTT really does solve this issue. It presents a host of new questions and it's almost certain that we haven't found the best presentation of these ideas yet, but even the presentation we have solves the problems that the author talks about in this article.
I'd also like to know more about that. My comment points out some things about HoTT that might be described as "downsides" by some but are more like things that people might expect from HoTT given that it 'handles' type equality in a rigorous yet flexible way, but aren't actually feasible in a rigorous treatment, i.e. the system is not going to pick up all the issues that are "brushed aside" in an informal treatment and resolve them on its own. Its behavior will point out to you that these issues exist, but you'll still have to do a lot of work dotting the i's and crossing the t's, as with any formalization.
> It handles all the complications that the author mentions. This is one of the reasons type theorists were excited about HoTT in the first place.
It's not that simple, Buzzard actually seems to be quite familiar with HoTT. The HoTT schtick of defining equality between types as isomorphism does 'handle' these issues for you in the sense that they are treated rigorously, but there's no free lunch in that. You still need to do all the usual work establishing compatibility of values, functions etc. with the relevant isomorphisms, so other than the presentation being somewhat more straightforward there is not much of a gain in usability.
Can you elaborate more on how you think HoTT can solve the issue Buzzard mentions that when formalizing informal mathematics, the author frequently has a model (or, a particular construction) in mind and requires properties present in the model, and then claims that this is true for all "canonically equivalent" objects without actually spending time explicating the abstract nonsense required to properly specify the properties that canonically equivalent objects preserve, for their developement? (see: a product vs. the product)
Edit: and furthermore, the situation where the obvious choice of universal property (read: level of isomorphism) was a poor one, in their attempt to formalize localizations.
I think 99.9% of the people talking about HoTT haven't used HoTT in practice. They just see isomorphism is equivalent to equivalence(or something similar), comes up with a mental model and think this is the main contribution of HoTT, whereas isomorphism is a well studied thing even before formal set theory was a thing. HoTT gets weird and anyone who has tried any tool to prove anything in HoTT knows this, and this is the reason why it didn't got adopted even though many leading tools like lean worked hard to implement it.
[1] is the only video which I would say I found any bit accessible. But to be honest even after spending days, I couldn't grok it. And in my observation, different implementations of HoTT are quite different from each other.
For reference, the paper mentions the term "homotopy" exactly once, in this sentence:
> The set-theoretic definition is too strong (Cauchy reals and Dedekind reals are certainly not equal as sets) and the homotopy type theoretic definition is too weak (things can be equal in more than one way, in contrast to Grothendieck’s usage of the term).
Classical versus non-classical has nothing to do with it. HoTT does not work to capture what a mathematician means by "unique isomorphism" because witnesses of equality in HoTT are very much not unique.
I think HOTT helps remove a lot of the footguns and computational hairiness around using type-theoretic mathematics. But the issues Buzzard is talking about are really more profound than that.
This relates to a much deeper (but familiar and nontechnical) philosophical problem: you assign a symbol to a thing, and read two sentences that refer to the same symbol ("up to isomorphism"), but not necessarily the same thing. If the sentences contradict each other, is it because they disagree on the meaning of the symbol, or do they disagree on the essence of the thing? There is a strong argument that most debates about free will and consciousness are really about what poorly-understood thing(s) we are assigning to the symbol. Worse, this makes such debates ripe for bad faith, where flaws in an argument are defended by implicitly changing the meaning of the symbol.
In the context of """simple""" mathematics, preverbal toddlers and chimpanzees clearly have an innate understanding of quantity and order. It's only after children fully develop this innate understanding that there's any point in teaching them "one," "two," "three," and thereby giving them the tools for handling larger numbers. I don't think it makes sense to say that toddlers understand the Peano axioms. Rather, Peano formulated the axioms based on his own (highly sophisticated) innate understanding of number. But given he spent decades of pondering the topic, it seems like Peano's abstract conception of "number" became different from (say) Kronecker's, or other constructivists/etc. Simply slapping the word "integer" on two different concepts and pointing out that they coincide for quantities we can comprehend doesn't actually do anything by itself to address the discrepancy in concept revealed by Peano allowing unbounded integers and Kronecker's skepticism. (The best argument against constructivism is essentially sociological and pragmatic, not "mathematically rational.")
Zooming out a bit, I suspect we (scientifically-informed laypeople + many scientists) badly misunderstand the link between language and human cognition. It seems more likely to me that we have extremely advanced chimpanzee brains that make all sorts of sophisticated chimpanzee deductions, including the extremely difficult question of "what is a number?", but to be shared (and critically investigated) these deductions have to be squished into language, as a woefully insufficient compromise. And I think a lot of philosophical - and metamathematical - confusion can be understood as a discrepancy between our chimpanzee brains having a largely rigorous understanding of something, but running into limits with our Broca's and Wernicke's areas, limits which may or may not be fixed by "technological development" in human language. (Don't even get me started on GPT...)
The level of insights and clearness in your message, and most comments in this thread actually, is surprising great compared to what I often read on HN.
The fact that Buzzard is writing this paper at all to me shows a much higher degree of respect than before --- see how humble the overview is. I think this is great progress!
If you want to frame a 'universal defining property', you have to frame it in some language. The definition, therefore, is inevitably idiosyncratic to that language, and, if you specify the same property using a different language, the definition is going to change. What's more, the two definitions can be incommensurable.
And---all you have done is translate from the object language to the meet language--leaving the definitions of the terms of the meta language completely unexplicated.
The solution to this is as old too---like "point", "line", etc, these terms can--and arguably should--remain completely un-defined.
whence did you learn this idiom of "the meet language"???
i have working definitions of line, point, etc.. in terms of dimensions. but I have some issues with the precise definition of "dimension" due to having picked up the concept of "density". I cannot say what's the difference between density and dimension
sigh I really hate autocorrect. It was supposed to be "meta", not "meet".
It's bad enough that most of the content I read these days is being generated by LLMs. Slowly and inexorably, even the content I write is being written and overwritten by LLMs.
How can you frame a paper from 1965 as "very old" when the linked article is about Grothendieck, who started his math PhD in 1950 (and presumably studied math before that)?
The very very old solution I'm adverting to is Euclid's axioms. They don't define what "point" or "line" means, they just specify some axioms about them.
I haven't actually dug up the source, so I'm not sure if the gaps here are related, but GC Rota apparently claimed that one reason the umbral calculus remained mysterious for as long as it did was about ambiguities with `=`.
> Rota later stated that much confusion resulted from the failure to distinguish between three equivalence relations that occur frequently in this topic, all of which were denoted by "=".
There's so much ambiguous context that goes into your average '=', even when just talking about your standard functions on real numbers. You'll see it being used for anything from:
- We've found these to be equal
- We're hypothesizing this to be equal
- These are approximately equal
- These are defined to be equal
- This is a way to calculate something else, whether it's equal is up to your philosophy (a^2+b^2=c^2)
- I'm transforming my function into something else that looks different but is exactly the same
- I'm transforming my function into something else that is the same for some of the stuff I care about (but for example does not work anymore for negative numbers, complex nrs, etc.)
- I'm transforming my function into something else, but it's actually a trapdoor, and you can't convert it back.
- This is kind of on average true within an extremely simplified context or we know it's not true at all, but we'll pretend for simplification (looking at you physics)
- We are trying to check if these two are equal
- This is equal, but only within a context where these variables follow some constraints mentioned somewhere else entirely
- This is equal, but, we're not going to say whether you can or can't replace the variables with functions or whether it supports complex nrs, negative nrs, non-integers, etc.
A lot of this is usually kind of clear from context, but some of these differences are a nightmare if you want to code it out
Equality can be philosophically troubling, but as a practical matter, what you care about is the indiscernibility of identicals, and if every property you use follows from a universal property, then equal up to isomorphism is just equal. So every Rubik's cube is equal considered as a group of face rotations, and there's only one Rubik's cube, but if you care about chemical properties of sticker glue, they're no longer equal.
Something the author points out: sometimes theorems directly rely on specific constructions of mathematical objects, which are then used to establish things that do not mention the construction.
I have now read the paper and it alone is enough to make me seriously consider devoting significant amount of my time to the author's project. Here's why:
In my introductory statistics class, I learned that a independent and identically distributed sample is a sequence of random variables X[1], ..., X[n], all of the same signature Omega -> (usually) R. All of them are pairwise independent, and all of them have the same distribution, e.g. the same density function. Elsewhere in probability I have learned that two random variables that have the same density function are, for all intents and purposes, the same.
For all, really? Let's take X[i] and X[j] from some i.i.d. random sample, i != j. They have the same density, which leads us to write X[i] = X[j]. They are also independent, hence
P(X[i] in A, X[j] in A) = P(X[i] in A)*P(X[j] in A),
but X[i] = X[j], so
P(X[i] in A, X[j] in A) = P(X[i] in A, X[i] in A) = P(X[i] in A), so
P(X[i] in A) in {0, 1}.
This was a real problem for me, and I believe I had worse results in that statistics class than I would have if the concept was introduced properly. It took me a while to work out a solution for this. Of course, you can now see that the strict equality X[i] = X[j] is indefensible, in the sense that in general X[i](omega) != X[j](omega) for some atom omega. If you think about what needs to be true about Omega in order for it to have two different variables, X[i] and X[j]:Omega -> R, that are i.i.d, then it will turn out that you need Omega to be a categorical product of two probability spaces:
Omega = Omega[i] x Omega[j]
and X[i] (resp. X[j]) to be the same variable X composed with projection onto first (resp. second) factor. This definition of "sampling with replacement" is able to withstand all scrutiny.
Of course, just like in Buzzard's example of ring localization, it was all caused by someone being careless about using equality.
I was just thinking about something adjacent to this the other day. I had this half-baked idea that you could classify all the "types" built out of, say (R, ×, →) by algebraically replacing each copy of R with a finite set of cardinality a and then counting the cardinality of the entire type expression. So you'd formally associate, say, R^3 with the algebraic term a^3, and that holds regardless of how you rearrange R^3 = R^2 × R or R × R^2 or whatever. I liked the idea because it seemed (?) to derive non-obvious set theoretic equivalences, for free: such as
R -> (R -> R) ~ (a^a)^a = a^(a^2)
R^2 -> R ~ a^(a^2)
(R -> R)^2 ~ (a^a)^2 = a^(2a)
R -> R^2 ~ a^(2a)
The first equivalence is between a "curried", partial-application, function form of a function of two arguments, and the "uncurried" form which takes a tuple argument. The second equivalence is between a pair of real functions and a path in the plane R^2—the two functions getting identified with the coordinate paths x(t) and y(t). (Remember the cardinality of distinct functions over finite sets S -> T is |T|^|S|).
And I think you can take this further, I'm not sure how far, for example by associating different formal parameters a,b,c... for different abstract types S,T,U... Is this a trick that's already known, in type theory?
(My motivation was to try to classify the "complexity", "size", of higher-ordered functions over the reals. The inspiration's that you're imagining a numerical approximation on a grid of size a for (a finite subinterval in) each copy of R: then that cardinality relates to the memory size of the numerical algorithm, working inside that space. And you could interpret the asymptotic growth of the formal function, as a complexity measure of the space. If you think of R^n -> R as a "larger" function space than R -> R^n, that observation maps to a^(a^n) being an asymptotically faster-growing function (of 'a') than (a^n)^a = a^(na). And similarly the functionals, (R -> R) -> R, and function operators (like differential operators) (R -> R) -> (R -> R), form a hierarchy of increasing "size").
The connection between type isomorphisms and algebraic equalities is known and explored in a variety of interesting ways.
I don't know the precise history of the development of the notation and vocabulary, but there's a reason types like A+B are notated with a plus symbol and called "sums". Similarly for products. And it may surprise you (or not) to learn that people sometimes call A -> B an exponential type, and even notate it with superscript notation.
One of my favorites is the result that the binary tree type is isomorphic to septuples of binary trees, which you can arrive at by using the definition of binary trees as the fixed point solution of T = 1 + T*T and deriving T = T^7 with some algebra. [0]
I really like this. I remember my first serious math book, which was this old-school set theory and topology book, and being all excited about learning set theory up until I encountered iterated Cartesian product, and was forced to accept that ((x, y), z) and (x, (y, z)) are supposed to be indistinguishable to me. An answer on StackExchange said that "you will never, ever, ever need to worry about the details of set theory", but I still did.
This is an excellent text to understand mathematical structuralism.
But it feels anticlimactic.
At the beginning there are fundamental problems with mathematical equality.
In the end, there is no great new idea but only the observation that in algebraic geometry some proofs have holes (two kinds), but they can be filled (quite) schematically.
"Some proofs" are the proof used to verify that the definition of an affine scheme makes sense, and the author motions in the direction that every single proof in algebraic geometry uses identically wrong arguments when using the language of "canonical" maps.
Thus the replication crisis of mathematics is revealed. In the words of John Conway: a map is canonical if you and your office neighbor write down the same map.
When this subject comes up I always think that the equality sign is loaded. It can mean, definition, equality, identity, and proportionality. How come this state of the equality sign is not mentioned in the paper?
As a mathematician, I have never, ever seen the equal sign used to denote proportionality. I cannot tell what you mean by "identity" that wouldn't be equality. And a definition in the sense you seem to mean is, indeed, also an equality. I guess this issue not mentioned in the paper because it doesn't exist.
I agree it’s not really used symbolically, but isn’t it referring to the difference between, say:
(x + y)(x - y) = x^2 - y^2
(an identity, since it’s true for every x and every y) and something more arbitrary like
3x^2 + 2x - 7 = 0
(an equation certainly not valid for all x and whose solutions are sought).
Of course, really, the first one is a straightforward equality missing some universal quantification at the front… so maybe that’s just what the triple equals sign would be short for in this case.
It's not symbol soup, it's projective coordinates. Did you claim to be a mathematician? I merely have a PhD in Mathematics and a few papers in peer-review journals, so, unlike you, not a real mathematician, and I immediately understood the point.
Uh... I have a PhD, I'm a tenured professor, and I even supervise a couple of PhD students. How about you? Given your snarky tone, it sounds like you'd have mentioned something like this. Not sure why you'd try to flex when you don't know much about me ;)
With my font, the letter l looked like a vertical bar |. Hence why this looked like symbol soup. But okay, let's say it's about projective spaces. Then surely, you realize that the equal sign still denotes equality. The point [1:2] is literally equal to [2:4] in P^2, not "proportional". Perhaps you need a refresher: https://en.wikipedia.org/wiki/Equivalence_class#quotient_set
I used l instead of \lambda, my bad I guess. My point was that the equality sign = is used to denote equality between projective points [x:y] = [ax:ay] and also proportionality between the ordered pairs [x:y] = [ax:ay], just depending on how you read and understand it.
I later remembered fractions a/b = ac/bc work this way too!
Big-O notation is a famous example where = is some flavor of (asymptotic) proportionality, and it catches a lot of people out when they first learn about it.
The story of Grothendieck is really fascinating. He was a superstar in algebraic geometry, only to suddenly reject the endeavor of mathematics and going off to grow vegetables in the Pyrenees. He also demanded that all notes from his lectures be destroyed. But those notes existed in so many hands, I don’t think many people (if any) complied.
