Spider Diagrams with Absence: Inference Rules for Clutter Reduction

Spider diagrams represent sets, their cardinalities and, sometimes, the specific individuals within those sets. They are expressively equivalent to monadic first-order logic with equality. Typically, diagrammatic logics with this level of expressiveness are not equipped to directly express the absence of an individual from a set. Instead, individuals must be asserted to be present and, thus, absent from the set's complement. The first time that absence could be directly asserted was in Venn-i. Since then, it been shown that in a related system called Venn-i^e (a monadic first-order logic without equality) the inclusion of absence information can significantly reduce diagram clutter. In this paper, we explore an extension of spider diagrams to include direct representation of the absence of individuals from sets. We identify necessary and sufficient conditions for satisfiability, allowing us to define an inconsistency rule allowing significant reductions in diagram clutter. Building on that, we introduce sound inference rules specifically related to spiders (which represent elements, individuals or their absence) that alter the levels of clutter in consistent diagrams. In the context of these rules, we explore the implications of including absence information for reducing clutter. In particular, we show that the significant benefits, in terms of clutter reduction, seen through the use of absence in Venn-i^e do not manifest to such an extent in spider diagrams.