Multi-type Calculi and Structural Control

In recent years, the multi-type approach to the automatic generation of analytic calculi for classes of logics has emerged, initially motivated by the goal of extending the reach of proper display calculi [16] (characterizations of those logics amenable to be captured by proper display calculi have been given in [5,13]) as a proof-theoretic format. This approach draws on semantic insights to obtain proof-theoretic results. Specifically, it hinges on the possibility of equivalently reformulating the algebraic semantics of a given logic in terms of a suitable variety of heterogeneous algebras [3], algebraic structures as in universal algebra in which more than one domain is allowed. Well-known logical frameworks to which the multi-type methodology has been successfully applied include first-order logic [1], dynamic epistemic logic , linear logic [11], monotone modal logic [4], semi-De Morgan logic [12], the logic of lattices [14], of bilattices [10], of rough algebras [9], and inquisitive logic [7,8].

Although these logical frameworks are very different from one another, both technically and conceptually, a common core to their being not properly displayable was precisely identified in the encoding of key interactions between different types, displaying different behaviour. For instance, for dynamic epistemic logic the difficulties lay in the interaction between (epistemic) actions, agents' beliefs, and facts of the world; for propositional dynamic logic, in the interaction between general and iterative actions; for linear logic, between general resources and reusable resources; for inquisitive logic, between general formulas (having both a sentential and an inquisitive content) and flat formulas (having only a sentential content). In each case, precisely the formal encoding of these interactions gave rise to non-analytic axioms in the original formulations of the logics. In each case, the multi-type approach allowed us to redesign the logics, so as to encode the key interactions into analytic multi-type rules, and define a multi-type analytic calculus for each of them. Metaphorically, adding types is analogous to adding dimensions to the analysis of the interactions, thereby making it possible to unravel these interactions, by reformulating them in analytic terms within a richer language.

Besides being used to solve technical problems of existing logics, the multi-type methodology can be also used for different purposes; for instance, as a design framework for new logics that serve to analyze specific interactions, as done in [2]. Precisely in this context, in [11], it is illustrated by a toy example how the multi-type framework can usefully be applied as a formal environment for accounting for various forms of grammatical exceptions in formal linguistics, and on this basis, it is argued that this methodology can be a useful tool for further developing structural control in type logical theory [15]. In this talk, I will discuss these ideas and propose some research directions.