On the expressiveness of second-order spider diagrams

Existing diagrammatic notations based on Euler diagrams are mostly limited in expressiveness to monadic first-order logic with an order predicate. The most expressive monadic diagrammatic notation is known as spider diagrams of order. A primary contribution of this paper is to develop and formalise a second-order diagrammatic logic, called second-order spider diagrams, extending spider diagrams of order. A motivation for this lies in the limited expressiveness of first-order logics. They are incapable of defining a variety common properties, like ‘is even', which are second-order definable. We show that second-order spider diagrams are at least as expressive as monadic second-order logic. This result is proved by giving a method for constructing a second-order spider diagram for any regular expression. Since monadic second-order logic sentences and regular expressions are equivalent in expressive power, this shows second-order spider diagrams can express any sentence of monadic second-order logic.