We've alluded to the debate surrounding the legitimacy of diagramming as a form of proof in mathematics.
Philosophers, great mathematicians, and working mathematicians have all taken sides in the debate. For example, Steve Awodey (who has multiple professorships at Carnegie Mellon in the Computer Science, Philosophy, and Mathematics Departments - CMU being one of the best Computer Science programs in the world and who was kind enough to help review a paper of mine in graduate school) has explored ways to link breakthrough research (often the considered the hottest current area in mathematics and which perhaps most famously hosted in part at The n-Category Café) in Homotopy Type Theory and Univalent Foundations.
To reprise, mathematical proof is deductive and follows from sound (tautological or necessarily (absolutely) true) axioms (not mere assumptions) written in First-Order Logic equipped with the Theory of Sets (e.g. - Proof Theory). How can a picture, therefore, be a proof?
Just wanted to throw a few quick, unvarnished thoughts into the ring.
I was recently in conversation with a math colleague about Temperley-Lieb Algebra and we stumbled across the topic of Kauffman’s Diagram Monoids (pp. 5).
The technique is apparently quite famous and is immediately compelling even to an abstract algebra dilettante like myself!
Of interest to this blog post is the manner by which the authors link the diagramming to the underlying set-theoretic notions. Nowhere present is the equivalent of a formal representation theorem. A few features of the diagram are linked to underlying operations (and the remaining operations, features, etc. ignored or abstracted away). For instance:
"Such diagrams are identified up to planar isotopy, i.e. continuous deformation within the portion of the plane bounded by the framing rectangle.." (pp. 5)
But that describes only some of the available or present phenomena within such a diagram.
At most that'd be some kind of homomorphism and is a far cry from something like isomorphism (or its contextual equivalents here like path deformation, etc). Does that
Some other examples discussing this topic and who take similar approaches:
To be fair, the papers above are discussing established and widely used accepted techniques. However, in considering some purported limitations of the above diagramming methods, our conversation returned to the familiar topic at the top of this post.
I looked into the original research by Kaufmann a tiny bit more. For instance his seminal paper An Invariant of Regular Isotopy.
The paper is incredibly precise and axiomatic in its approach. It exhibits certain properties thereby that we would traditionally ascribe to linguistic systems (closure principles, concatenation, substitution, etc.). I think this invites the question (and perhaps it's one that's been asked) - are diagrams just a kind of language? (I definitely argue as such for Connection Theory.)
Or, in the same way, that we extract from contentations of random symbol permutations in something like formal logic, the Well-Formed Formulae. Are some diagrams "linguistic"? (Or, validly considered as such? Others not - no pun!)
If some diagrams (or all of them) are linguistic then proof-theoretic exercises mapping diagrams to language systems would be meta-linguistic in nature - an exercise translating from one language system to another. Do some of the mysteries of diagrammatic reasoning fall away here?
Mathematical notation is quite varied and idiomatic (and more efficient or readily understandable notation is often a point of pride among successful mathematicians).
From a slightly different vantage point, I wonder if it is better to conceive of diagramming as not merely language per se but as a specific kind of short-handing language - which mathematical notation is often explicitly introduced to be.
Diagramming on this view is fully linguistic but it has certain implicit representational properties - it's mapped to some underlying syntax (of some target language). (I'm assuming that's what notation is doing - that it's fundamentally meta-linguistic which is not characteristic of all language.)
From the opposite vantage point, it might be more fruitful to view all formal language (given its grounding in symbolic calculus - that is to say, written symbol systems) as fundamentally diagrammatic rather than seeing diagrams as ancillary or derivative from language.
On such a view, drawing precedes language. Language can even be a way of mapping many pictures to a unitary drawn thing (e.g. - "the word"). Without art, language would not emerge as a faculty.
On this such, written systems are mapped to underlying pictures (and not the other way around) - indeed we do map our semantics to an underlying domain of discourse (which is taken to stand for or "picture" as Wittgenstein puts something in the world - setting the philosophical quibbles about the ultimate coherence of that conception).
Anyway, that seems a bit radical (but no doubt defended by someone somewhere).