Intuitionistic Layered Graph Logic: Semantics and Proof Theory

TL;DR

This paper introduces ILGL, an intuitionistic layered graph logic, providing semantics, proof systems, and decidability results, with applications to modeling complex layered systems in physical and social sciences.

Contribution

It develops ILGL, a novel intuitionistic substructural logic for layering, with soundness, completeness, and decidability proofs, extending to predicate logic and applications.

Findings

Soundness and completeness of ILGL with respect to graph-based semantics

Decidability of ILGL established via algebraic semantics

Extension of ILGL to predicate logic with dual semantics

Abstract

Models of complex systems are widely used in the physical and social sciences, and the concept of layering, typically building upon graph-theoretic structure, is a common feature. We describe an intuitionistic substructural logic called ILGL that gives an account of layering. The logic is a bunched system, combining the usual intuitionistic connectives, together with a non-commutative, non-associative conjunction (used to capture layering) and its associated implications. We give soundness and completeness theorems for a labelled tableaux system with respect to a Kripke semantics on graphs. We then give an equivalent relational semantics, itself proven equivalent to an algebraic semantics via a representation theorem. We utilise this result in two ways. First, we prove decidability of the logic by showing the finite embeddability property holds for the algebraic semantics. Second, we prove a Stone-type duality theorem for the logic. By introducing the notions of ILGL hyperdoctrine and indexed layered frame we are able to extend this result to a predicate version of the logic and prove soundness and completeness theorems for an extension of the layered graph semantics . We indicate the utility of predicate ILGL with a resource-labelled bigraph model.