Zulip Chat Archive

Stream: mathlib4

Topic: Notations vs Notation

Harald Husum (Sep 14 2025 at 13:29):

I noticed in the documentation style guide that files defining notation should contain a docstring header called "Notations".

Upon inspecting mathlib I saw that there are currently 110 such headers. There is a further 187 cases of "Notation" headers. In my mind "Notation" sounds better (even in the plural case) than "Notations" and I think this explains why the mandated version is less popular.

I'd personally like to standardize on "Notation", but I want to ask for the community's opinion before doing so.

Harald Husum (Sep 14 2025 at 13:31):

/poll Should I
Change all isntances of "Notation" headers to "Notations"
Change all isntances of "Notations" headers to "Notation" and try to get the style guide updated
None of the above (please ellaborate)

Aaron Liu (Sep 14 2025 at 13:34):

the module docstring "workspace snippet" thing in VSCode generates a section called "Notation"

Michael Rothgang (Sep 14 2025 at 13:50):

In my mind, "notation" is uncountable - so the plural sounds just awkward

Jireh Loreaux (Sep 14 2025 at 16:05):

I suspect (but am not sure) that English is in a transition from "notation" being a countable noun to being a uncountable one. As such, I think it's fine to leave both and this is not worth changing.

Thomas Murrills (Sep 14 2025 at 16:52):

I think “notation” can be either countable or uncountable, depending on context, as for many uncountable nouns: uncountable in most cases, when referring to the stuff of a convention (“there’s so much notation used in this file”, “adding more notation is contentious”) and countable when referring to (potentially multiple) whole conventions (“there are various notations for…”, “is there a notation yet for…?”). Similar to “water”/“waters”, “mass”/“masses”.

I’d tend to consider a single choice of multiple nonoverlapping conventions (e.g. notation for the identity map + notation for the hom type) still a single convention, and so lean towards using “notation” here. Likewise, “notations” connotes multiple alternative, possibly overlapping notations to me. (The boundary is indeed a little fuzzy, though, since collections of conventions can also be conventions!)

Harald Husum (Sep 15 2025 at 09:08):

I think I share the perspective of @Thomas Murrills here, that "notation" can be both countable and uncountable, depending on context, but that the case of this header seems to lean more in the uncountable direction.

I'm not sure it means much, but ChatGPT seems to agree:

Is the noun "notation" considered countable or uncountable?

The noun “notation” can be both countable and uncountable, depending on context:

1. Uncountable Usage

When referring to a system of symbols or a way of writing things, “notation” is usually uncountable.

Example: “Musical notation has evolved over centuries.”
Here, we treat it as a general concept, not something that can be counted.

2. Countable Usage

When referring to specific kinds or instances of notations, it can be countable.

Example: “Different notations are used in physics and mathematics.”
In this case, you’re talking about several distinct types of notation.