Spider diagrams
John Howse, Gem Stapleton and John Taylor
Abstract: The use of diagrams in mathematics has traditionally been
restricted to guiding intuition and communication. With rare
exceptions such as Peirce's alpha and beta systems, purely
diagrammatic formal reasoning has not been in the mathematician's
or logician's toolkit. This paper develops a purely diagrammatic
reasoning system of "spider diagrams" that builds on Euler, Venn
and Peirce diagrams. The system is known to be expressively
equivalent to first-order monadic logic with equality. Two levels
of diagrammatic syntax have been developed: an "abstract" syntax
that captures the structure of diagrams, and a "concrete" syntax
that captures topological properties of drawn diagrams. A number
of simple diagrammatic transformation rules are given, and the
resulting reasoning system is shown to be sound and complete.
|
