Towards Universal Logic: Gaggle Logics

Résumé En

A class of non-classical logics called gaggle logics is introduced, based on a Kripke-style relational semantics and inspired by Dunn's gaggle theory. These logics deal with connectives of arbitrary arity and we show that they capture a wide range of non-classical logics. In particular, we list the 96 binary connectives and 16 unary connectives of basic gaggle logic and relate their truth conditions to the non-classical logics of the literature. We establish connections between gaggle theory and group theory. We show that Dunn's abstract law of residuation corresponds to an action of transpositions of the symmetric group on the set of connectives of gaggle logics and that Dunn's families of connectives are orbits of the same action. Other operations on connectives, such as dual and Boolean negation, are also reformulated in terms of actions of groups and their combination is defined by means of free groups and free products. We show how notions of groups arise naturally from our gaggle logics and how gaggle logics can be canonically defined from given groups. Our other main contribution deals with the proof theory of gaggle logics. We show how sound and complete calculi can be systematically computed from any basic gaggle logic with or without Boolean connectives. These calculi are display calculi and we prove that the cut rule can be systematically eliminated from proofs. This allows us to prove that basic gaggle logics are decidable.