Title: Combination of first-order uniform interpolants via Beth definability

 Abstract: Uniform interpolants were largely studied in non-classical propositional logics since the nineties, and their connection to model completeness was pointed out in the literature. A successive parallel research line inside the automated reasoning community investigated uniform quantifier-free interpolants (sometimes referred to as “covers”) in first-order theories. In this contribution, we investigate cover transfer to theory combinations in the disjoint signatures case. We prove that, for convex theories, cover algorithms can be transferred to theory combinations under the same hypothesis needed to transfer quantifier-free interpolation (i.e., the equality interpolating property, aka strong amalgamation property). The key feature of our algorithm relies on the extensive usage of the Beth definability property for primitive fragments to convert implicitly defined variables into their explicitly defining terms. In the non-convex case, we show by a counterexample that covers may not exist in the combined theories, even in case combined quantifier-free interpolants do exist. However, we exhibit a cover transfer algorithm operating also in the non-convex case for special kinds of theory combinations; these combinations (called ‘tame combinations’) concern multi-sorted theories arising in many model-checking applications (in particular, the ones oriented to verification of data-aware processes).

Joint work with: Diego Calvanese · Alessandro Gianola · Marco Montali · Andrey Rivkin.

Title: Universal Proof Theory: Constructive Rules and Feasible Admissibility

Abstract: In this talk, we introduce a general family of sequent-style calculi over the modal language and its fragments to capture the essence of all constructively acceptable systems. Calling these calculi constructive, we show that any strong enough constructive sequent calculus, satisfying a mild technical condition, feasibly admits all Visser’s rules, i.e., there is a polynomial time algorithm that reads a proof of the premise of a Visser’s rule and provides a proof for its conclusion. As a positive application, we show the feasible admissibility of Visser’s rules in several sequent calculi for intuitionistic modal logics, including CK, IK and their extensions by the modal axioms T, B, 4, 5, the modal axioms of bounded width and depth and the propositional lax logic. On the negative side, we show that if a strong enough intuitionistic modal logic (satisfying a mild technical condition) does not admit at least one of Visser’s rules, then it cannot have a constructive sequent calculus. Consequently, no intermediate logic other than IPC has a constructive sequent calculus.

Title: Nested sequents, Kripke models, and uniform interpolation

Abstract: Proof-theoretic method is one of the primary sources for constructive proofs of interpolation. After first being used to prove Craig interpolation using cut-free sequent calculi, the method has been extended to Lyndon interpolation, and uniform interpolation, as well as to analytic sequent calculi. More recently, it has been extended to hypersequents, nested sequents, labelled sequents, yielding, for instance, a positive answer to the open problem of whether Gödel logic (intermediate logic of linear frames) has Lyndon interpolation.
An interesting feature of this extension is its essential use of Kripke semantics (for modal or intermediate logics). While the algorithm for contructing interpolants is purely proof-theoretic, the proof of its correctness relies on the semantics. More pertinently, the algorithm in general and individual interpolant transformations in particular are guided and shaped by the structure of Kripke models of the logic in question.
In this work, we extend this syntactico-semantic method to proving uniform interpolation for K, D, and T using nested sequents and for S5 using hypersequents.
Joint work with: Iris van der Giessen · Raheleh Jalali.

Title: Model completions and uniform interpolation

Abstract: A well-known theorem of classical model theory due to Robinson states that the (first-order) theory of totally ordered Abelian groups has a model completion. However, it was proved by Glass and Pierce that this is not the case for the theory of lattice-ordered Abelian groups. Similarly, it was proved by Lacava and Saeli that the theory of totally ordered MV-algebras has a model completion, but not the theory of all MV-algebras. In this talk, we will generalize these negative results to see that the theory of a variety of commutative pointed residuated lattices has a model completion if and only if the variety admits uniform deductive interpolation and has equationally definable principal congruences. We will also see how positive model completion results can be rescued for varieties that admit uniform deductive interpolation by adding an additional binary operator.

Title: Generalized Heyting Algebras and Duality

Abstract: ∇-algebras are the natural generalization of Heyting algebras, unifying many algebraic structures including bounded lattices, Heyting algebras, temporal Heyting algebras and point-free formalization of the dynamical systems. They are also powerful enough to represent any “natural” abstract implication.

In this talk, we will explain the algebraic and topological properties of different varieties of these algebras. We start with the algebraic theme of characterizing the subdirectly and simple ∇-algebras, the Dedekind-MacNeille completion, the canonical construction and the amalgamation property. Then, we will move to the topological theme to provide a unification of Priestley and Esakia dualities to capture the dual spaces corresponding to these algebras. This then leads to spectral duality and finally to some ring-theoretic representation for some of these algebras.

Title: Disjunctive Bases: Uniform Interpolation in Coalgebraic Modal Fixpoint Logic

Abstract: In this talk we will discuss the property of uniform interpolation for a wide variety of coalgebraic modal logic and their extensions with fixpoint operators. Starting with the work of Albert Visser, the semantic study of uniform interpolation is intimately connected with the notion of bisimulation quantifiers; in the setting of the modal mu-calculus, D’Agostino and Hollenberg brought automata theory into the framework. Since both the concept of bisimilarity and the framework of automata operating on infinite objects are essentially coalgebraic in nature, it is a natural question is to see whether the results on uniform interpolation for basic modal logic can be transferred to the wider coalgebraic setting, to include formalisms such as monotone and graded modal logic (and their fixpoint extensions). In this talk we introduce and motivate the notion of a disjunctive basis, and we show that any coalgebraic modal logic that admits a disjunctive basis, enjoys the uniform interpolation property.

Joint work with: Sebastian Enqvist.