max and sup

[ncfavier]

Some people are complaining that the HoTT book uses $\mathsf{max}(x, y)$ to denote the $\mathsf{sup}$ operation in a lattice, and in particular the $\mathsf{sup}$ of two real numbers, whereas in traditional mathematical practice $\mathsf{max}\{x, y\}$ denotes the maximum of the set $\{x, y\}$, i.e. the $\mathsf{sup}$ with the added side condition that $\mathsf{max}\{x, y\} \in \{x, y\}$.

Is there a reason for this apparent departure from convention? Was it to avoid conflict with the $\mathsf{sup}$ constructor for $W$-types or the $\lor$ logical connective?

[mikeshulman]

"max" is only used for the real numbers or other ordered field, not for an arbitrary lattice, and these orders are linear. In classical mathematics, any supremum in a linear order is a maximum in the sense you mean, so the difference is only visible constructively. I was under the impression that "max" was standardly used this way for the real numbers by constructive mathematicians, where I believe it does have the property that $(\mathrm{max}(x,y) \# x) \to (\mathrm{max}(x,y) =y)$ which is equivalent, in classical mathematics, to being a maximum in your sense. I don't have access to my bookshelf at the moment, but I thought, for instance, that Bishop uses it this way. Are the people doing the complaining familiar with the literature on real numbers in constructive mathematics?

[ncfavier]

I'll just cut out the middleman: the discussion happened on X/Twitter https://nitter.privacydev.net/ncfavier/status/1812145889722413267.

[martinescardo]

I think Bishop uses max. I agree it is not an accurate notation. I think we should not change it, though, to avoid the mathematics looking too different. Perhaps a remark can be added to clarify that this function classically provides the maximum and constructively produces only a least upper bound in general.

[mikeshulman]

I think it's more than just a least upper bound. The classical condition $\mathrm{max}(x,y) \in \{x,y\}$ is equivalent to $(\mathrm{max}(x,y) = x) \vee (\mathrm{max}(x,y) = y)$, so when rephrasing this constructively we have multiple options for how to interpret the $\vee$. If we use the strong constructive (a.k.a. "additive") disjunction we get a strong notion that isn't satisfied by the real numbers. But we can also use the weak "multiplicative" disjunction $(\neg P \to Q) \wedge (\neg Q \to P)$, and then we get a property that I believe the max operation on real numbers does satisfy constructively, as long as we interpret "not equal to" as "apart from". So I would say it isn't that this operation isn't a maximum, rather it's that there is more than one constructive notion of maximum, just as there is more than one constructive notion of "field": the rationals are a field in the strong sense that every number is either zero or invertible, but the real numbers are a field in the weaker sense that every number apart from zero is invertible, and we still call them both fields. Similarly, I think it's justified to call this operation a (weak / multiplicative) maximum.

But I agree that adding a clarifying remark is a good idea.

[Gro-Tsen]

(I'm the one who pointed out this issue to Naïm.)

I think $\max(x,y)$ is a horrible notation. This requires to forego either the convention that $\max(x,y) = \max\{x,y\}$ or the idea that $\max(S) \in S$ for any set $S$ for which the notation is defined; both options are terribly bad: the first is horribly confusing, and the second is a complete break of mathematical tradition.

Yes, Bishop does write $\max\{x,y\}$, but Bishop is clearly trying to make constructive analysis look as similar to real analysis as possible, and this notation is part of his plan. (Also, Bishop uses Cauchy sequences, so it makes a bit more sense to use the notation for the termwise operation on Cauchy sequences: maybe in classical math you can get away with writing $\max$ for the pointwise max of two functions, but it's still in bad taste.) Troelstra and van Dalen use $\max(x,y)$, as presently done in the HoTT book, which is admittedly a bit less bad than $\max\{x,y\}$, but still horrible.

In either case, this still leaves open the question of how one is supposed to denote the max of a set in the standard definition of the max of a set, namely: $z = \max S$ means “we have $z\in S$ and for every $t\in S$ the relation $t\leq z$ holds”.

Doing constructive math is not a valid excuse for redefining one of the most basic and standard concepts in mathematics, at least not when this definition as it stands makes perfect and useful sense in constructive math. How else are we supposed to express the concept in quotes at the end of the last paragraph?

(So maybe there an alternative definition of $\max S$ that I missed, by sprinkling $\neg\neg$ in appropriate places, which reduces to the above in the classical setting and equals $\frac{1}{2}(x+y+|x-y|)$ when $S = \{x,y\}$, which could justify using “max” for the sup of two reals; but even then, the general rule for “constructivizing” classical math concepts is to go for the strongest notion that makes useful sense, not one obtained by adding $\neg\neg$ in various places, and the strongest notion that makes useful sense for $z = \max S$ is the one where $z\in S$ is required.)

Writing $\sup(x,y)$ will surprise nobody, it will confuse nobody, I'm pretty sure I've seen this notation used in classical math even for real numbers, and it makes perfect sense.

If for some reason you don't like “sup”, then maybe I can suggest something like “wmax” (or some small variation or decoration of “max” as long as it isn't exactly “max”)? Since the order on $\mathbb{R}$ is being called “weakly linear”, it probably makes sense to call the sup operation on reals a “weak max”. But please don't just call it “max” as this breaks long-established traditions and is guaranteed to confuse readers.

[awodey]

I think comparisons with previous authors, such as Bishop and Troelstra-vanDalen, are more persuasive than appeals to what someone thinks is “standard” or “horrible”.

[mikeshulman]

the general rule for “constructivizing” classical math concepts is to go for the strongest notion that makes useful sense.

I don't think that "strongest" is always quite the right adjective to use here, but it's a reasonable approximation, so let's accept it for the sake of argument.

The point is that the strong notion of max where $z\in S$ does not make useful sense for the real numbers, because they don't have maximums in that sense. Yes, some ordered sets like the rational numbers or integers do have maximums in that sense, but it's a well-known fact that when constructivizing math often a single classical concept splits into two or more constructively different ones. So I would argue that for the real numbers and other similar fields, the notion of "max" that I gave (which is, to repeat, not just a least upper bound) is the strongest notion that makes useful sense.

It's true that it may surprise readers coming from a classical background to find that the maximum of a pair of real numbers is not necessarily equal to one or to the other (at least, not for the strong "additive" notion of "or"). But there are a lot of surprising things about constructive mathematics to a reader coming from a classical background. As I mentioned, it's not true that every real number is either zero or invertible, but we still call them a field constructively. So I don't find that a very persuasive argument.

[Gro-Tsen]

I think comparisons with previous authors, such as Bishop and Troelstra-vanDalen, are more persuasive than appeals to what someone thinks is “standard” or “horrible”.

But the HoTT book already deviates from previous works in several notational aspects. Notably, Bishop writes $x\neq y$ to say that $|x-y|>0$: this is a terrible notation because it is established mathematical convention that $x\neq y$ means $\neg(x=y)$ and it is extremely confusing to use it for anything else (similarly to the case of $\max$, Bishop wants to make constructive analysis look as similar as possible to classical analysis, and this is why he uses this notation): the HoTT book writes $x\#y$ for this, which is so much better because it avoids confusion. Also, Bishop writes “nonvoid” for what the HoTT book calls “inhabited”, again a much better term because saying that $S$ is “nonvoid” should mean $\neg(S=\varnothing)$.

All three situations (using $x\#y$ rather than $x\neq y$, using “inhabited” rather than “nonvoid”, and using “sup” rather than “max”) follow the same pattern: Bridges was trying to make constructive analysis look and sound like classical analysis, but it turns out that it's highly confusing to change the meaning of an extremely standard mathematical term or notation ($x\neq y$ has the standard meaning $\neg(x=y)$, “nonvoid” has the standard meaning $\neg(S=\varnothing)$, and “max” has the standard meaning of belonging to the set), whereas the cost of using an unambiguous notation is very low. The HoTT book chooses clarity over following Bridges in the first two: I don't understand why the third should be treated differently. In fact the cost of writing $\sup(x,y)$ instead of $\max(x,y)$ is less than in the first two cases, because there's no new notation or terminology to invent: “sup” perfectly does the job.

I really don't understand what the problem with “sup” is: it's completely standard mathematical notation, so everyone knows what it means, and it's unambiguous so nobody will be surprised. What, exactly, is wrong about using “sup”?

As far as I can see, anything is better than “max”: call it “sup”, $\vee$, $\sqcup$, “wmax” (for “weak max” because it's a sort of weak linear order of max), max with a bar over it (because it's the max of the completion), anything whatsoever provided it's properly explained and does not redefine one of the most standard mathematical concepts in existence. Is there truly no compromise that can be deemed acceptable?

I mean, how do you propose to denote the max of a set $S$ in the usual sense of the term (the element of $S$, if it exists, which is $\geq$ every element of $S$) if max is used to denote something similar but still confusingly different?

If you really want to appeal to prior works, here's one example: Mandelkern's 1988 paper Constructively Complete Finite Sets (which is highly relevant here because it's all about such questions as whether a set of the form $\{x_1,\ldots,x_n\}$ is complete, has a max, and such stuff) uses $x\vee y$ and $x\wedge y$ to denote the sup and inf of two real numbers. (Also for what it's worth, he seems to have thought this notation was so clear that it didn't even require an explanation.)

The minimum and maximum are partial binary functions

$$\min, \max:\left(\sum_{x, y:\mathbb{R}} x \leq y \vee y \leq x\right) \to \mathbb{R}$$

which are only total binary functions in the presence of the analytic LLPO. This is similar to how the floor and ceiling are partial functions which are only total functions in the presence of the analytic LPO.