A New Road Towards Universal Logic?

A generic logic called ‘Gaggle logic’ is introduced. It is based on Gaggle theory and deals withconnectives of arbitrary arity that are related to each other by abstract laws of residuation. Welist the 96 binary connectives and the 16 unary connectives of Gaggle logic. We provide a soundand complete calculus for Gaggle logic which enjoys strong cut elimination and the displayproperty. We show that Gaggle logic is decidable and satisfies the properties of conservativityand interpolation. We also introduce specific inference rules called ‘protoanalytic’ inferencerules. These rules are such that, when added to the calculus of Gaggle logic, we obtain acalculus which still enjoys strong cut elimination and the display property. If the languageconsidered contains conjunction and disjunction, then the interpolation theorem also transfersto these extensions of Gaggle logic. In a second part of the report, we generalize the Kracht’scorrespondence results established for the basic tense logic to Gaggle logic. We prove that alogic extending Gaggle logic is axiomatizable by means of so-called ‘protoanalytic’ inferencerules if, and only if, the class of frames on which such a logic is based is definable by specificfirst-order frame conditions, also called ‘protoanalytic’. We provide algorithms that compute thecorresponding protoanalytic inference rules from the protoanalytic first-order frame conditions,and vice versa. We illustrate these algorithms on well-known structural inference rules and weshow in particular how we can recover classical logic from Gaggle logic by the addition ofprotoanalytic inference rules that refine the standard classical inference rules