ALCOP VI, 2015: Algebra and Coalgebra meet Proof Theory

The aim of this talk is to provide a better understanding of which monoidal operations appear in finite MTL-chains (i.e., the finite subdirectly irreducible algebras of the algebraic counterpart associated with the monoidal t-norm logic). We remind that MTL-chains are exactly the FLew-algebras which are also finite chains. Moreover, it is very easy to introduce them without requiring any logical background. They are the commutative monoid operations over {0,1,2,...,n-1} (for some finite cardinal number n) such that:

• n-1 is a neutral element,
• the monoid operation is monotonic with respect to the standard
  order in {0,1,2,...,n-1}.

For example, for the cardinal number 6 some of the operations we get are the following:

Indeed, these 7 tables provide all involutive ones (in the sense that zeros occur exactly in the upper diagonal part) of such cardinality.

The main results we will consider in the talk can be summarised in providing:

• a method to describe all such operations just using the
  involutive ones,
• a characterization (with some connections to algebraic geometry)
  of such involutive operations.

The usefulness of such characterization will be exhibited by explicitly providing a finite involutive MTL-chain where the equation

fails. It is worth pointing out that this last equation holds in all continuous t-norms (i.e., in all BL-chains).

   Substructural logics are axiomatic extensions of full Lambek calculus. They encompass, among many others, classical, intuitionistic, intermediate, fuzzy, and relevant logics. In my talk I will outline some results towards a uniform and systematic introduction of analytic calculi for substructural logics. Our main methodology is a new integration of proof theoretic and algebraic techniques (algebraic proof theory), developed together with N. Galatos and K. Terui. The introduced calculi are then used to provide uniform proofs of standard completeness for large classes of logics, that is completeness with respect to algebras based on truth values in [0,1].

   Coalgebra provides a general framework for modelling state-based dynamical systems, coalgebraic modal logics provide a generic way to reason about those systems. Coalgebra also has been used to provide a new semantics for logic programming, essentially by viewing a logic program as a coalgebra. Recent advances in both coalgebraic logic & logic programming have started to produce concrete algorithms and efficient implementations thereof. I will argue that these advances could also lead to a new versatile framework for querying semi-structured data.
I will first give a brief introduction to coalgebraic logic and to ontology-based data access, a method for querying heterogeneous, but semantically-related data. In particular, I will present my recent work in these areas on a coalgebraic generalisation of propositional dynamic logic (PDL) and on Datalog+/-. In the second, somewhat speculative part of the talk, I am going to sketch how coalgebraic techniques can be used to query data: models of dynamical systems are closely related to models of semi- or graph-structured data and query languages, such as XPath and Datalog+/-, are closely related to modal logics and logic programming.

 Following the suggested substructural theme of this edition of ALCOP, I will return to my old work with Tomasz Kowalski on completions of GBL-algebras; or, more precisely, on widespread lack thereof. GBL-algebras, also known as divisible residuated lattices, include MV-algebras, product algebras and lattice-ordered groups; we showed that none of these subvarieties admits local completions. Apart from presenting the paper itself, I will briefly discuss some of earlier research on completions of ordered algebraic structures by G. Bezhanishvili, M. Gehrke, J. Harding or H. Priestley. However, an equally important inspiration for us was the study of various notions of completeness for modal logics I undertook in my PhD Thesis. I will show how some notions of "strong completeness" generalize the standard notion of canonicity and correspond to closure under various types of completions; the modal setting allows particularly smooth construction of natural counterexamples (one of my favourites has been obtained by Frank Wolter, another by Timothy Surendonk). I will attempt to answer how this relationship between various types of completions and various notions of strong completeness transfers to the substructural case, although to the best of my knowledge, these waters are still somewhat uncharted.
Rather surprisingly, our paper resurfaced several years afterwards as a limitative result for algebraic proof theory. Hence, inasmuch as time allows, I will also sketch the relationship between admissibility of completions and cut elimination (unless this is going to be covered by other ALCOP presentations). Finally, in the unlikely case there is still some time left, I will briefly report on relevant aspects of my ongoing research with Peter Jipsen on algebraic semantics of extensions of BI and GBI, which combine modal and substructural features.

   (Joint work with Umberto Rivieccio)
The Logic of Epistemic Actions and Knowledge is an expansion of classical modal logic introduced by A. Baltag, L. S. Moss and S. Solecki as a framework for reasoning about knowledge in a dynamic logic setting. A. Kurz and A. Palmigiano recently showed that duality theory provides a flexible framework for modelling epistemic changes, which allows one to develop dynamic epistemic logics on a propositional basis that is weaker than classical logic (e.g., an intuitionistic basis).
In this talk we explain how the techniques of Kurz and Palmigiano can be further extended to define and axiomatize a bilattice-based Logic of Epistemic Actions and Knowledge. Our propositional basis is a modal expansion of the well-known four-valued logic of Belnap and Dunn, which is a system designed for handling inconsistent as well as potentially conflicting information. These features, we believe, make our framework particularly promising from a computer science perspective.

 Display calculi are well suited for modularly composing bigger calculi from smaller ones. A famous highlight is Belnap's cut elimination theorem: As long as rules adhere to some general format, adding rules to a display calculus preserves cut elimintation. On the downside, both proving in as well as proving theorems about these calculi can be difficult to handle by hand if they involve large number of rules. In this talk I will present some preliminary investigations in how to support reasoning in and about display calculi, followed by a demo of the tools we already have implemented.

   (Joint work with Nick Galatos and Luca Spada)
In this talk I will discuss a generalization of the methods of canonical formulas from Heyting algebras to n-potent residuated lattices. I will show that every variety of n-potent residuated lattices is axiomatizable by these formulas. I will also discuss some examples.

   Generalizing standard monadic second-order logic for Kripke models, we introduce monadic second-order logic interpreted over coalgebras for an arbitrary set functor T. Similar to well-known results for monadic second-order logic over trees, we provide a translation of this logic into a class of automata, relative to the class of T-coalgebras that admit a tree-like supporting Kripke frame. We then consider invariance under behavioral equivalence of MSO-formulas, and in particular we investigate whether the coalgebraic mu-calculus is the bisimulation-invariant fragment of MSO for T. Building on recent results by the third author we show that in order to provide such a coalgebraic generalization of the Janin-Walukiewicz Theorem, it suffices to find what we call an adequate uniform construction for the functor T. As applications of this result we obtain a partly new proof of the Janin-Walukiewicz Theorem, and bisimulation invariance results for the bag functor (graded modal logic) and all exponential polynomial functors.
Finally, we consider in some detail the monotone neighborhood functor M, which provides coalgebraic semantics for monotone modal logic. It turns out that there is no adequate uniform construction for M, whence the automata-theoretic approach towards bisimulation invariance does not apply directly. This problem can be overcome if we consider global bisimulations between neighborhood models: we can derive a characterization of the monotone modal mu-calculus extended with the global modalities, as the fragment of monadic second-order logic for the monotone neighborhood functor that is invariant for global bisimulations. From this result, we can derive as a corollary that the monotone mu-calculus is indeed the bisimulation-invariant fragment of monadic second-order
logic for M.

   In his book [4], Hájek introduces a discussion about the connections between fuzzy logic and probability. He points out several differences: for instance, fuzzy logic is a logic for the treatment of vagueness, whereas probabilistic logic is a logic for the treatment of uncertainty. Moreover, the most prominent fuzzy logics are truth functional, whereas probabilistic logic is not. Nevertheless, Hájek shows that probabilistic logic can be treated inside fuzzy logic, by means of a modality Pr to be interpreted as probably. In [2], the authors introduce a logic, called FP(Ł,Ł),in which it is possible to express the probability of fuzzy events. This logic is not algebraizable in the sense of Blok and Pigozzi (cf. [1]), and its semantics is not given by means of universal algebras but rather by means of Kripke models. On the algebraic side, Mundici in [5] introduces states on MV-algebras. These operators can be interpreted as probabilistic measures over many-valued formulas. Moreover, as shown by Mundici in [6], states are also related to subjective probability. Indeed, he shows that a probabilistic assessment over many-valued events can be extended to a state iff there is no Dutch-book for it.
Thus, both states and probabilistic fuzzy logics have to do with probability over fuzzy events. However, so far these two approaches to probability have been investigated separately. In [3], the authors try to connect them. To this purpose, they introduce an algebraizable logic, called SFP(Ł,Ł),which extends FP(Ł,Ł),and whose equivalent algebraic semantics is constituted by a variety of universal algebras, called SMV-algebras. These algebras are MV-algebras equipped with a unary operation whose properties somehow simulate the properties of states.
The purpose of the present talk is to connect the semantics of MV-algebras with a state to the semantics given by Kripke models, showing that both semantics are equivalent to a semantics given by a special kind of SMV-algebras, called σ-simple SMV-algebras. As a consequence, we establish some complexity theoretic results for the classes of SFP(Ł,Ł)-formulas which are 1-tautologies or 1-satisfiable (with respect to various kinds of semantics).

References
[1] Blok W., Pigozzi D., Algebraizable Logics. Mem. Amer. Math. Soc, 396 (77). Amer. Math Soc. Providence, 1989.
[2] Flaminio T., Godo L., A logic for reasoning on the probability of fuzzy events. Fuzzy Sets and Systems, 158, 625–638, 2007.
[3] T. Flaminio, F. Montagna, MV-algebras with internal states and probabilistic fuzzy logics. International Journal of Approximate Reasoning 50 (2009) 138–152.
[4] P. Hájek, Metamathematics of Fuzzy Logic, Trends in Logic Vol 4, Kluwer, Dordrecht, 1998.
[5] D. Mundici, Averaging the truth-value in Łukasiewicz logic. Studia Logica 55(1) (1995) 113-127.
[6] D. Mundici, Bookmaking over Infinite-valued Events. International Journal of Approximate Reasoning 43 (2006) 223–240.

   (Joint work with G. Greco, A. Kurz, A. Palmigiano, A. Tzimoulis)
In this talk I will discuss the main features of a multi-type display calculus for PDL (Propositional Dynamic Logic). I will expand on the design of the calculus and on the difficulties arising from the induction axiom for the operator + (transitive closure). Finally, I will discuss the open question of conservativity for this calculus.

   P. F. Conrad and other authors launched a general program for the investigation of lattice-ordered groups, aimed at elucidating some order-theoretic properties of these algebras by inquiring into the structure of their lattices of convex l-subgroups. This approach can be naturally extended to residuated lattices and their convex subalgebras. In this broader perspective, we revisit the Galatos-Tsinakis categorical equivalence between integral generalized MV algebras and negative cones of l-groups with a nucleus, showing that it restricts to an equivalence of the full subcategories whose objects are the projectable members of these classes. Upon recalling that projectable integral generalized MV algebras and negative cones of projectable l-groups can be endowed with a positive Gödel implication, and turned into varieties by including this implication in their signature, we prove that there is an adjunction between the categories whose objects are the members of these varieties and whose morphisms are required to preserve implications.

   In constructive proof theory, proving that a proposition A has a proof in the context Gamma amounts to showing that type A is inhabited by a proof p, namely it amounts to constructing p. This principle underlies most modern interactive theorem provers, e.g. Coq or Agda.
First-order automated theorem proving, in contrast, has much weaker, if any, support for capturing structural (constructive) properties of proofs. To prove that a proposition A follows from a logic program Gamma, the algorithm of SLD-resolution should derive a contradiction from assumption that A is false. The proof structure remains irrelevant in this decision procedure, as long as resolution algorithm succeeds.
The resolution approach has advantages, the main of which is efficient proof automation. However, neglecting proof structure comes at a price. It is extremely hard to analyse structural properties of programs. One striking example is the fact that in 40 years since introduction of logic programming, the community has never reached a consensus on the notion of universal termination of logic programs, let alone semi-deciding that property. In contrast, universal termination of Coq programs can be semi-decided by imposing the structural recursion check. In logic programming we can only talk about termination of individual SLD-derivations, for goals of certain kinds, so we can only work with various forms of existential termination.
In this talk, I will show how the recent coalgebraic semantics of logic programming inspired a new structural approach to untyped theorem proving. Structural Resolution is an analogue of constructive proof theory approach realised in the untyped first-order setting of logic programming. In particular, it allows to formulate, for the first time in logic programming, notions of a proof-witness, a generalised coinductive principle for structural derivations, as well as a new theory of universal productivity (a coinductive counterpart of universal termination).

 The talk will highlight some recent applications of weighted colimits and density to (co)algebraic logic from recent joint work with A. Balan and J. Velebil. The aim is to give a high level introduction to these notions in the expectation that they might prove useful more generally in (co)algebraic logics. The talk will assume some familiarity with basic category theory (functors, natural transformations, colimits, adjoints).

   (This is an undergoing joint work with Zhiguang Zhao (TU Delft))
Weak strict implication logics are logics for local consequence relation over Kripke frames. Their algebras are called weak Heyting algebras. In this talk, we will first present a Sahlqvist theory for weak strict implication logic, using algorithmic correspondence theory. Second, we will show that some weak strict implication logics can be conservatively extended to Lambek calculi above DFNL^+ (bounded distributive full non-associative Lambek calculus) uniformly, using canonical extension and a calculus based on an Ackerman Lemma. Those Lambek calculi admit cut elimination and the subformula property.

   Belnap's Display Calculus is a proof-calculus which generalises Gentzen's sequent calculus and is suitable for presenting logics whose logical operators are residuated. Indeed, the display calculus can be viewed as the proof-theoretic face of the algebraic semantics of a fully residuated logic. In particular, the residuation of the logical operators corresponds to a powerful structural property from the proof-theoretic perspective: the display property. The formalism has been applied to give analytic calculi (i.e. systems with the subformula property) for many different families of logics including substructural logics, tense logics and bunched implication logics. A particularly attractive feature from a proof-theoretic point of view is the general cut-elimination theorem which applies whenever the rules of the display calculus obey certain easily-to-verify conditions.
We begin by introducing the display calculus. Then, using substructural logics as an example, we show how to compute equivalent structural rules from (suitable) axioms, leading to analytic display calculi for the corresponding axiomatic extensions. The conditions specifying which axioms are suitable are stated in terms of (purely syntactic) abstract properties of the base calculus. The method thus applies directly to display calculi for many different logics. We show also how to obtain the converse direction i.e. structural rules to axioms.

Language is contextual and sheaf theory offers a setting to reason about contextuality. Can one be applied to reasoning about the other? In preliminary work with Abramsky (published in essays dedicated to Jim Lambek on the occasion of his 90th birthday, 2014), we showed how this may indeed be possible. We introduced a presheaf structure corresponding to a basic form of Kamp's Discourse Representation Structures. Within this setting, we formulated a notion of semantic unification as a form of sheaf-theoretic gluing. We then showed how these gluings could be used to provide a global semantics for a discourse by putting together the local logical semantics of each sentence within that discourse. This can be used to, for instance, resolve anaphora. Composing the sheaf functor with a distributions functor can be used to represent situations where multiple gluings are possible, and where we may need to rank the anaphoric resolutions using quantitative measures retrieved from corpora of text.

Coalgebraic modal logic serves as a unifying framework for a wide range of modal logics beyond the relational realm, including probabilistic and graded logics as well as conditional logics and logics based on neighbourhoods and games. Coalgebraic predicate logic (CPL), a generalization of a neighbourhood-based first-order logic introduced by Chang, has been identified as a natural first-order extension of coalgebraic modal logic, which in particular coincides with the standard first-order correspondence language when instantiated to Kripke-style relational modal operators. The classical van Benthem/Rosen theorem stating that both over arbitrary and over finite models, modal logic is precisely the bisimulation-invariant fragment of first-order logic, generalizes to the coalgebraic setting, with corresponding characterizations for, e.g., conditional logic, neighbourhood logic, and monotone modal logic arising as special cases. We originally established the generic result for a first-order language featuring explicit neighbourhoods and successor structures; in the talk, I will focus on specific aspects of a native proof for the Chang-style language, which in particular requires an extension of Gaifman locality to this setting.

Finitely presented MV-algebras are dually equivalent to rational polyhedra and Z-maps among them. This connection led to a number of pivotal results in their theory, but unfortunately it does not carry on to non-semisimple MV-algebras. In this talk I will discuss how the aforementioned duality can be lifted to the general category of MV-algebras through the method of ind- and pro- completions. In particular I will focus my attention on which conditions are to be required in order to have a workable definition of arrow in the latter categories.

   (Joint work with Giuseppe Greco, Minghui Ma, Alessandra Palmigiano, Zhiguang Zhao)
This presentation reports on the results of [11], and focuses on the formal connections between correspondence phenomena, well known from the area of modal logic, and the theory of display calculi, originated by Belnap [1].
Sahlqvist correspondence theory. Sahlqvist theory [15] is among the most celebrated and useful results of the classical theory of modal logic, and one of the hallmarks of its success. It provides an algorithmic, syntactic identification of a class of modal formulas whose associated normal modal logics are strongly complete with respect to elementary (i.e. first-order definable) classes of frames.
Unified correspondence. In recent years, building on duality-theoretic insights [7], Sahlqvist theory has significantly broadened its scope, extending the benefits it originally imparted to modal logic to a wide range of logics which includes, among others, intuitionistic and distributive lattice-based (normal modal) logics [5], non-normal (regular) modal logics [14], substructural logics [6], hybrid logics [9], and mu-calculus [2,3]. The breadth of this work has stimulated many and varied applications. Some are closely related to the core concerns of the theory itself, such as the understanding of the relationship between different methodologies for obtaining canonicity results [13], or of the phenomenon of pseudocorrespondence [8]. Other, possibly surprising applications include the dual characterizations of classes of finite lattices [10]. These and other results have given rise to a theory called unified correspondence [4].
Tools of unified correspondence theory. The most important technical tools in unified correspondence are: (a) a very general syntactic definition of the class of Sahlqvist formulas, which applies uniformly to each logical signature and is given purely in terms of the order-theoretic properties of the algebraic interpretations of the logical connectives; (b) the algorithm ALBA, which effectively computes first-order correspondents of input term-inequalities, and is guaranteed to succeed on a wide class of inequalities (the so-called inductive inequalities) which, like the Sahlqvist class, can be defined uniformly in each mentioned signature, and which properly and significantly extends the Sahlqvist class.
Unified correspondence and display calculi. The proposed talk focuses on an entirely different type of application of unified correspondence: the identification of the syntactic shape of axioms which can be translated into analytic rules of a display calculus. A rule is called analytic if adding it to a display calculus preserves Belnap’s cut-elimination theorem. The connections between Sahlqvist theory and display calculi have been seminally observed by Marcus Kracht in [12], in the context of his characterisation of those formulas of the language of basic modal logic (which he calls primitive formulas) which can be effectively transformed into structural rules of display calculi.
Contributions. The two tools of unified correspondence can be put to use to generalise Kracht’s transformation procedure from axioms into analytic rules. This generalisation concerns more than one aspect. Firstly, in the same way in which the definitions of Sahlqvist and inductive inequalities can be given uniformly in each logical signature, the definition of primitive formulas/inequalities is introduced for any logical framework the algebraic semantics of which is based on distributive lattices with operators. Secondly, in the context of each such logical framework, we introduce a hierarchy of subclasses of inductive inequalities, progressively extending the primitive inequalities, the largest of which is the class of so-called analytic inductive inequalities. This class significantly generalises the class of primitive formulas/inequalities. We provide an effective procedure, based on ALBA, which transforms each analytic inductive inequality into an equivalent set of analytic rules. Moreover, we show that any analytic rule can be effectively and equivalently transformed into some analytic inductive inequality.

References
[1] N. Belnap. Display logic. Journal of Philosophical Logic, 11:375–417, 1982.
[2] W. Conradie and A. Craig. Canonicity results for mu-calculi: an algorithmic approach. Journal of Logic and Computation, forthcoming.
[3] W. Conradie, Y. Fomatati, A. Palmigiano, and S. Sourabh. Algorithmic correspondence for intuitionistic modal mu-calculus. Theoretical Computer Science, 564:30–62, 2015.
[4] W. Conradie, S. Ghilardi, and A. Palmigiano. Unified correspondence. In A. Baltag and S. Smets, editors, Johan F.A.K. van Benthem on Logical and Informational Dynamics, volume 5 of Outstanding Contributions to Logic, pages 933–975, Springer, 2014.
[5] W. Conradie and A. Palmigiano. Algorithmic correspondence and canonicity for distributive modal logic. Annals of Pure and Applied Logic, 163(3):338 – 376, 2012.
[6] W. Conradie and A. Palmigiano. Algorithmic correspondence and canonicity for non-distributive logics. Journal of Logic and Computation, forthcoming.
[7] W. Conradie, A. Palmigiano, and S. Sourabh. Algebraic modal correspondence: Sahlqvist and beyond. Submitted, 2014.
[8] W. Conradie, A. Palmigiano, S. Sourabh, and Z. Zhao. Canonicity and relativized canonicity via pseudo-correspondence: an application of ALBA. Submitted, 2014.
[9] W. Conradie and C. Robinson. On Sahlqvist theory for hybrid logic. Journal of Logic and Computation, forthcoming.
[10] S. Frittella, A. Palmigiano, and L. Santocanale. Dual characterizations for finite lattices via correspondence theory for monotone modal logic. Journal of Logic and Computation, forthcoming.
[11] G. Greco, M. Ma, A. Palmigiano, A. Tzimoulis, and Z. Zhao. Unified correspondence as a proof-theoretic tool. Submitted, 2014.
[12] M. Kracht. Power and weakness of the modal display calculus. In Proof theory of modal logic, pages 93–121. Kluwer, 1996.
[13] A. Palmigiano, S. Sourabh, and Z. Zhao. Jónsson-style canonicity for ALBA-inequalities. Forthcoming, 2014.
[14] A. Palmigiano, S. Sourabh, and Z. Zhao. Sahlqvist theory for impossible worlds. Journal of Logic and Computation, forthcoming.
[15] H. Sahlqvist. Completeness and correspondence in the first and second order semantics for modal logic. In Studies in Logic and the Foundations of Mathematics, volume 82, pages 110–143, 1975.

   (Joint work with Sebastian Enqvist and Fatemeh Seifan)
While completeness results for basic modal logic and many of its coalgebraic variants are well known and understood, the situation is very different for extensions of modal logics with fixpoint operators. In particular, Igor Walukiwicz' seminal result for the modal mu-calculus has until now remained a stand-alone theorem. In the talk, which is based on work in progress, we analyze Walukiewicz' proof from a coalgebraic, automata-theoretic angle. Our purpose is to deconstruct the proof into pieces that can be understood and analyzed further in the theory of coalgebraic logic.