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.