Multi-Type Algebraic Proof Theory

This dissertation pertains to algebraic proof theory, a research field aimed at solving problems in structural proof theory using results and insights from algebraic logic, universal algebra, duality and representation theory for classes of algebras. The main contributions of this dissertation involve the very recent theory of multi-type calculi on the proof-theoretic side, and the well established theory of heterogeneous algebras on the algebraic side. Given a cut-admissible sequent calculus for a basic logic (e.g. the full Lambek calculus), a core question in structural proof theory concerns the identification of axioms which can be added to the given basic logic so that the resulting axiomatic extensions can be captured by calculi which are again cut-admissible. This question is very hard, since the cut elimination theorem is notoriously a very fragile result. However, algebraic proof theory has given a very satisfactory answer to this question for substructural logics, by identifying a hierarchy (Nn, Pn) of axioms in the language of the full Lambek calculus, referred to as the substructural hierarchy, and guaranteeing that, up to the level N2, these axioms can be effectively transformed into special structural rules (called analytic) which can be safely added to a cut-admissible calculus without destroying cut-admissibility. The research program of algebraic proof theory can be exported to arbitrary signatures of normal lattice expansions, to the study of the systematic connections between algebraic logic and display calculi, and even beyond display calculi, to the study of the systematic connections between the theory of heterogeneous algebras and multi-type calculi, a proof-theoretic format generalizing display calculi, which has proven capable to encompass logics which fall out of the scope of the proof-theoretic hierarchy, and uniformly endow them with calculi enjoying the same excellent properties which (single-type) proper display calculi have. The defining feature of the multi-type calculi format is that it allows entities of different types to coexist and interact on equal ground: each type has its own internal logic (i.e. language and deduction relation), and the interaction between logics of different types is facilitated by special heterogeneous connectives, primitive to the language, and treated on a par with all the others. The fundamental insight justifying such a move is the very natural consideration, stemming from the algebraic viewpoint on (unified) correspondence, that the fundamental properties underlying this theory are purely order-theoretic, and that as long as maps or logical connectives have these fundamental properties, there is very little difference whether these maps have one and the same domain and codomain, or bridge different domains and codomains. This enriched environment is specifically designed to address the problem of expressing the interactions between entities of different types by means of analytic structural rules. In the present dissertation, we extend the semantic cut elimination and finite model property from the signature of residuated lattices to arbitrary signatures of normal lattice expansions, and build or refine the multi-type algebraic proof theory of three logics, each of which arises in close connection with a well known class of algebras (semi De Morgan algebras, bilattices, and Kleene algebras) and is problematic for standard proof-theoretic methods.