In this article, we extend the research programme in algebraic proof theory from axiomatic extensions of the full Lambek calculus to logics algebraically captured by certain varieties of normal lattice expansions (normal LE-logics). Specifically, we generalize the residuated frames in Reference [ 34 ] to arbitrary signatures of normal lattice expansions (LE). Such a generalization provides a valuable tool for proving important properties of LE-logics in full uniformity. We prove semantic cut elimination for the display calculi \(\mathrm{D.LE}\) associated with the basic normal LE-logics and their axiomatic extensions with analytic inductive axioms. We also prove the finite model property (FMP) for each such calculus \(\mathrm{D.LE}\) , as well as for its extensions with analytic structural rules satisfying certain additional properties.

Abstract We define LE- $$\mathcal {ALC}$$ , a generalization of the description logic $$\mathcal {ALC}$$ based on the propositional logic of general (i.e. not necessarily distributive) lattices, and semantically interpreted on relational structures based on formal contexts from Formal Concept Analysis (FCA). The description logic LE- $$\mathcal {ALC}$$ allows us to formally describe databases with objects, features, and formal concepts, represented according to FCA as Galois-stable sets of objects and features. We describe ABoxes and TBoxes in LE- $$\mathcal {ALC}$$ , provide a tableaux algorithm for checking the consistency of LE- $$\mathcal {ALC}$$ knowledge bases with acyclic TBoxes, and show its termination, soundness and completeness. Interestingly, consistency checking for LE- $$\mathcal {ALC}$$ with acyclic TBoxes is in PTIME, while the complexity of the consistency checking of classical $$\mathcal {ALC}$$ with acyclic TBoxes is PSPACE-complete.

We introduce proper display calculi for intuitionistic, bi-intuitionistic and classical linear logics with exponentials, which are sound, complete, conservative, and enjoy cut elimination and subformula property. Based on the same design, we introduce a variant of Lambek calculus with exponentials, aimed at capturing the controlled application of exchange and associativity. Properness (i.e., closure under uniform substitution of all parametric parts in rules) is the main technical novelty of the present proposal, allowing both for the smoothest proof of cut elimination and for the development of an overarching and modular treatment for a vast class of axiomatic extensions and expansions of intuitionistic, bi-intuitionistic, and classical linear logics with exponentials. Our proposal builds on an algebraic and order-theoretic analysis of linear logic and applies the guidelines of the multi-type methodology in the design of display calculi.

A recent strand of research in structural proof theory aims at exploring the notion of analytic calculi (i.e., those calculi that support general and modular proof-strategies for cut elimination) and at identifying classes of logics that can be captured in terms of these calculi. In this context, Wansing introduced the notion of proper display calculi as one possible design framework for proof calculi in which the analyticity desiderata are realized in a particularly transparent way. Recently, the theory of properly displayable logics (i.e., those logics that can be equivalently presented with some proper display calculus) has been developed in connection with generalized Sahlqvist theory (a.k.a. unified correspondence). Specifically, properly displayable logics have been syntactically characterized as those axiomatized by analytic inductive axioms , which can be equivalently and algorithmically transformed into analytic structural rules so the resulting proper display calculi enjoy a set of basic properties: soundness, completeness, conservativity, cut elimination, and the subformula property. In this context, the proof that the given calculus is complete w.r.t. the original logic is usually carried out syntactically , i.e., by showing that a (cut-free) derivation exists of each given axiom of the logic in the basic system to which the analytic structural rules algorithmically generated from the given axiom have been added. However, so far, this proof strategy for syntactic completeness has been implemented on a case-by-case base and not in general. In this article, we address this gap by proving syntactic completeness for properly displayable logics in any normal (distributive) lattice expansion signature. Specifically, we show that for every analytic inductive axiom a cut-free derivation can be effectively generated that has a specific shape, referred to as pre-normal form .

The present article aims at establishing formal connections between correspondence phenomena, well known from the area of modal logic, and the theory of display calculi, originated by Belnap.These connections have been seminally observed and exploited by Marcus Kracht, in the context of his characterization of the modal axioms (which he calls primitive formulas) which can be effectively transformed into 'analytic'structural rules of display calculi.In this context, a rule is 'analytic'if adding it to a display calculus preserves Belnap's cut-elimination theorem.In recent years, the state-of-the-art in correspondence theory has been uniformly extended from classical modal logic to diverse families of non-classical logics, ranging from (bi-)intuitionistic (modal) logics, linear, relevant and other substructural logics, to hybrid logics and mu-calculi.This generalization has given rise to a theory called unified correspondence, the most important technical tools of which are the algorithm ALBA, and the syntactic characterization of Sahlqvist-type classes of formulas and inequalities which is uniform in the setting of normal DLE-logics (logics the algebraic semantics of which is based on bounded distributive lattices).We apply unified correspondence theory, with its tools and insights, to extend Kracht's results and prove his claims in the setting of DLE-logics.The results of the present article characterize the space of properly displayable DLE-logics.

We introduce a multi-type display calculus for Propositional Dynamic Logic (PDL). This calculus is complete w.r.t. PDL, and enjoys Belnap-style cut-elimination and subformula property.

The present article provides an analysis of the existing proof systems for dynamic epistemic logic from the viewpoint of proof-theoretic semantics. Dynamic epistemic logic is one of the best known members of a family of logical systems that have been successfully applied to diverse scientific disciplines, but the proof-theoretic treatment of which presents many difficulties. After an illustration of the proof-theoretic semantic principles most relevant to the treatment of logical connectives, we turn to illustrating the main features of display calculi, a proof-theoretic paradigm that has been successfully employed to give a proof-theoretic semantic account of modal and substructural logics. Then, we review some of the most significant proposals of proof systems for dynamic epistemic logics, and we critically reflect on them in the light of the previously introduced proof-theoretic semantic principles. The contributions of the present article include a generalization of Belnap's cut-elimination metatheorem for display calculi, and a revised version of the display-style calculus D.EAK [30]. We verify that the revised version satisfies the previously mentioned proof-theoretic semantic principles, and show that it enjoys cut-elimination as a consequence of the generalized metatheorem.

In the present article, we introduce a multi-type display calculus for dynamic epistemic logic, which we refer to as Dynamic Calculus. The display approach is suitable to modularly chart the space of dynamic epistemic logics on weaker-than-classical propositional base. The presence of types endows the language of the Dynamic Calculus with additional expressivity, allows for a smooth proof-theoretic treatment, and paves the way towards a general methodology for the design of proof systems for the generality of dynamic logics, and certainly beyond dynamic epistemic logic. We prove that the Dynamic Calculus adequately captures Baltag–Moss–Solecki's dynamic epistemic logic, and enjoys Belnap-style cut elimination.