You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Evan Washington (Jan 12 2024 at 02:19):An interesting recent paper by Silvia de Toffoli on the status of mathematical diagrams in proofs, which is probably of interest to people here! Here's the abstract:
Mathematical diagrams are frequently used in contemporary mathematics. They are, however, widely seen as not contributing to the justificatory force of proofs: they are considered to be either mere illustrations or shorthand for non-diagrammatic expressions. Moreover, when they are used inferentially, they are seen as threatening the reliability of proofs. In this paper, I examine certain examples of diagrams that resist this type of dismissive characterization. By presenting two diagrammatic proofs, one from topology and one from algebra, I show that diagrams form genuine notational systems, and I argue that this explains why they can play a role in the inferential structure of proofs without undermining their reliability. I then consider whether diagrams can be essential to the proofs in which they appear.
In particular, what do you all think of the idea that diagrams are mere shorthand for more cumbersome non-diagrammatic expressions? Personally, I doubt whether the distinction between the diagrammatic and non-diagrammatic really makes sense!
Kevin Arlin (Jan 12 2024 at 02:24):Of course diagrams are genuine notational systems! Without looking more closely at the claims it seems like this must be being written without an awareness of the huge range of completely legitimate 2-dimensional syntaces familiar in category theory.
Damiano Mazza (Jan 12 2024 at 08:51):As long as there is the certainty that a diagrammatic calculus correctly reflects an underlying algebraic calculus (which is the case, for example, of string diagrams for all sorts of monoidal categories), then I don't see why anyone would attribute to diagrammatic proofs less legitimacy than non-diagrammatic proofs (this is good for me because I am utterly incapable of making any kind of reasoning in a monoidal category without drawing string diagrams :big_smile:).
Damiano Mazza (Jan 12 2024 at 08:54):Having worked a lot with linear logic proof nets in the past, my personal opinion is that the only real problem is the lack of a hassle-free human-computer interface for drawing diagrams. My dream, back then, was to have a software on a tablet such that you draw your proof net (or whatever diagram, including just a standard commutative diagram) with a stylus and it automatically converts it to LaTeX code. This is 100% realizable from the technological viewpoint, but the effort required to produce such a software is too big and the corresponding market too small for this to have been realized so far. The consequence, for me, was that at some point I just started writing papers using only -terms, although I would still prove everything drawing proof nets on a piece of paper :man_shrugging:
Morgan Rogers (he/him) (Jan 12 2024 at 10:05):Damiano Mazza said:
As long as there is the certainty that a diagrammatic calculus correctly reflects an underlying algebraic calculus (which is the case, for example, of string diagrams for all sorts of monoidal categories), then I don't see why anyone would attribute to diagrammatic proofs less legitimacy than non-diagrammatic proofs
I don't see why there has to be an "underlying" algebraic calculus. It so happens that many graphical calculi can be presented symbolically, like when one defines trees inductively, but the trees themselves are the subject of the reasoning and we can present formal rules for manipulating them (eg graph rewriting rules) without necessarily falling back on anything else. However, since we don't have a nuanced language for arguing with diagrams (explaining shortcuts in reasoning, say), and because telling stories with static diagrams is challenging, we often accompany diagrams by a bunch of text.
Damiano Mazza (Jan 12 2024 at 12:16):You are right, there doesn't have to be. I was thinking of formalisms that substitute algebraic calculi, but if a diagrammatic calculus is "primitive", of course that's fine as long as it conforms to the same kind of rigor that we demand of algebraic calculi. Anyway, if one sees terms as syntactic trees, any formalism is diagrammatic in some sense...
Mike Shulman (Jan 12 2024 at 15:11):Without disagreeing with any of that, I have the impression that not all graphical calculi that people use have yet been carefully proven to correctly reflect the intended algebraic structure. Usually this requires or amounts to a coherence theorem. That hasn't stopped me from inventing graphical calculi and using them without justification in the expectation that the relevant coherence theorem is true, so I don't expect it to stop others, but I do think it's something to be aware of.
Damiano Mazza (Jan 12 2024 at 15:30):I agree. Focusing only on the case of monoidal categories, I think Peter Selinger's survey is relatively explicit about when a rigorous proof exists and, if I remember correctly, this is the case for most of the basic variants (braided, symmetric, traced, compact closed, etc.). But outside of that, for example when one introduces a closed structure (that's not compact closed), or the simultaneous presence of products and/or coproducts, etc., I don't think I'd be able to give a reference to a formal correctness proof.
John Baez (Jan 12 2024 at 16:31):Evan wrote:
In particular, what do you all think of the idea that diagrams are mere shorthand for more cumbersome non-diagrammatic expressions? Personally, I doubt whether the distinction between the diagrammatic and non-diagrammatic really makes sense!
John Baez (Jan 12 2024 at 16:32):A lot of mathematicians who don't use diagrams find them confusing and have worries about their rigor. Those people are less likely to be found here!
John Baez (Jan 12 2024 at 16:34):I think an interesting issue about "diagrammatic versus nondiagrammatic" notation is the attitude towards how the meaning of a drawing on the page changes, or does not change, when you slightly change the picture.
John Baez (Jan 12 2024 at 16:35):For letters on the page, there should not be a change in meaning if I draw a letter, say X, in a slightly different way. I.e. the meaning should be invariant under change in handwriting.
John Baez (Jan 12 2024 at 16:37):However, the issue is subtler than I just indicated! We do expect that
means something different from
Sometimes it even means something different from
or
That is, sometimes people use all 4 of these letters to mean different things in the same text.
"Writing skeptics" might argue that this makes written mathematics hopelessly ambiguous. Exactly how much does your need to tilt before it becomes ? If we don't specify this, is our mathematics nonrigorous?
John Baez (Jan 12 2024 at 16:39):We tend to sweep these issues under the rug with writing, but they resurface in somewhat new ways when we use, say, string diagrams.
Julius Hamilton (Jun 11 2024 at 15:05):Damiano Mazza said:
I agree. Focusing only on the case of monoidal categories, I think Peter Selinger's survey is relatively explicit about when a rigorous proof exists
That’s an amazing article.
I’ve been thinking lately about a way to draw diagrams which present all the information in the category.
If one draws all objects as dots, and all morphisms as arrows, one still has to state the equivalence of morphisms under composition, which I’ve usually seen done in writing.
One could imagine a second collection of arrows which point from two morphisms to the morphism they compose to. But I have not often seen “forked arrows” in math, an arrow where two elements combine. I’ve also thought about this for drawing algebraic structures like groups.
It seems like a common strategy is to have two single arrows into something which represents “the combination of two things”; then an arrow from that. For example:
911F03CD-C15C-4414-9D7C-3ABEE46A31D9.jpg
Here, yellow represents the composition operation, and red is equality. (I accidentally wrote instead of ; let’s assume means “f, then g”.)
I have some ideas to explore. One thing that occurred to me just now, after reading some of Girard’s “Proofs and Types”, is that it is redundant to draw an arrow from to to represent “equality”. If they are identical, should we remove the name and refer to that arrow as ?
If not, then it seems the diagram has to distinguish between syntactic constructions and I think what might be called their “reduced form” in type theory. We have to show that from and , you can form term , and subsequently, there is a rule that permits the substitution of with term .
Jean-Baptiste Vienney (Jun 11 2024 at 16:57):John Baez said:
We tend to sweep these issues under the rug with writing, but they resurface in somewhat new ways when we use, say, string diagrams.
The issue of recognizing correctly the symbols is something I tell people about when they give a lot of importance to being extremely rigorous. We don’t think a lot about this step of recognizing the symbols. It shows that mathematics written by hand can’t be 100% formal because there is this informal step. This is more of a theoretical argument than a practical one. In practice, this is rarely an issue because we have been trained in writing and reading and today we use typesetting which writes symbols clearly for us.
I recognize that with string diagrams the issue comes back but still in practice, we seem to succeed in communicating effectively with string diagrams.
The good thing with diagrams, and here I think I just repeat something written in the book « Picturing Quantum Processes » is that instead of encoding mathematics in our human language using the alphabet plus other symbols, it is a way of taking advantage of our physical world in which we can depict path and other patterns. When I see a string diagram, I think about rivers, electrical circuits, deliveries of goods etc… and it can help in proving stuff.
In this sense, diagrams are not a shorthands for non-diagrammatic expressions! They are another language, often more effective but not all the time. When manipulating huge expressions in monoidal categories, the compactness of usual equations can make them more practical to use than string diagrams (here I’m thinking about concrete experience proving the Faà di Bruno rule in a differential category for instance).
Sometimes sequent calculus is better than both diagrams and usual equations, or lambda calculuses are better etc… To each mathematical practice (and here I include computer science as a mathematical practice), its best language. It’s all a matter of convenience and it can even depends on your mood. There is no best programming language, just some more practical than others in some situation. The same can be said of mathematical languages/notations.