Comment by User23

> It's almost as if wanting a meaningful, intuitive solution prevented me from solving the problem.

This theme shows up repeatedly in Dijkstra's work[1]. The symbol manipulation is itself a calculation.

  As a final influence I must mention our desire to let the symbols do the work —more precisely: as much of the work as profitably possible—. The intuitive mathematician feels that he understands what he is talking about and uses formulae primarily to summarize situations and relations in to him familiar universes. When he seems to derive one formula from another, the transformations he allows are those that seem to be true in the universe he has in mind. The formalist, however, prefers to manipulate his formulae, temporarily ignoring all interpretations they might admit, the rules for the permissible symbol manipulations being formulated in terms of those symbols: the formalist calculates with uninterpreted formulae.

The diagrammatic solution the author uses is related to something else I've been interested in, namely Peirce's Existential Graphs[2]. They are also based on diagrammatic representations of mathematical objects with a small set (somewhere between 3 and 6 depending on how you count inversion) of permissible rewrites. Existential Graphs are powerful enough to represent propositional or predicate logic with the exact same rules of inference! There is also an extension for something equivalent to Tarski's modal logic, but I haven't looked into it really. Peirce also designed existential graphs to be amenable to uninterpreted manipulation.

The tutorial I link has some nice examples of proving Frege's axioms using only a single assumed axiom and rules of inference he proved sound. Frege assumed all of his axioms. I mean no disrespect to Frege, but it illustrates just how powerful existential graphs are.

[1] https://www.cs.utexas.edu/~EWD/transcriptions/EWD13xx/EWD130...

[2] https://www.jfsowa.com/pubs/egtut.pdf or https://www.jfsowa.com/peirce/ms514.htm