Multi-type calculi

Alessandra Palmigiano - Vrije Universiteit Amsterdam
Multi-type calculi
Nell'ambito del progetto "Teoria della dimostrazione e informazione extra-logica"

Abstract
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 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, 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, dynamic epistemic logic, linear logic, monotone modal logic, semi-De Morgan logic, the logic of lattices, of bilattices, of rough algebras, and inquisitive logic.
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.  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.