Abstract : A generic logic called ‘protologic’ is introduced. It is based on Gaggle theory and deals with
connectives of arbitrary arity that are related to each other by abstract laws of residuation. We list
the 96 binary connectives and the 16 unary connectives of protologic. We provide a sound and
complete calculus for protologic which enjoys strong cut elimination and the display property.
We show that protologic is decidable and satisfies the properties of conservativity and interpolation.
We also introduce specific inference rules called ‘protoanalytic’ inference rules. These rules
are such that, when added to the calculus of protologic, we obtain a calculus which still enjoys
strong cut elimination and the display property. If the language considered contains conjunction
and disjunction, then the interpolation theorem also transfers to these extensions of protologic.
In a second part of the report, we develop a correspondence theory for protologic using the well–
known correspondence results for basic tense logic. We prove that a logic extending protologic
is axiomatizable with so-called ‘protoanalytic’ inference rules if, and only if, the class of frames
on which such a logic is based is definable by specific first-order frame conditions, also called
‘protoanalytic’. We provide algorithms that compute the corresponding protoanalytic inference rules
from the protoanalytic first-order frame conditions, and vice versa. We illustrate these algorithms
on well-known structural inference rules.