Algebra|Coalgebra Seminar

• Title: Fixed-point elimination in the Intuitionistic Propositional Calculus (Slides)
  Speaker: Luigi Santocanale (Aix-Marseille Université)
  Date: Wednesday, 26 May, 2021.
  Time: 16:00 (CEST)
  Location: Online (Zoom Meeting ID 922-5064-0302)
  [abstract]

  ---

  That fixed-points can be eliminated from mu-calculus based on the Intuitionistic Propositional Calculus (mu-IPC) is a consequence of Ruitenburg theorem. In this talk I'll present the elimination procedure of fixed points in the mu-IPC devised by Ghilardi, Gouveia, and myself, which also also yields a decision procedure for mu-IPC and the statement that its alternation hierarchy is trivial. The procedure equivalently shows that every positive (in some variable x) formula of the IPC has a finite closure ordinal. Contrary to previous results on full collapse of alternation hierarchies in mu-calculi, in this case there is no uniform upper bound of closure ordinals.

  The focus of the talk will be on the algebraic properties behind the elimination procedure: compatibility and strongness of formulas of the IPC, the role of the class of disjunctive formulas, and how it is possible to extract bounds on closure ordinals from standard equational properties of fixed-points.

  ---



• Title: Distributive lattice-ordered monoids (Joint work with A. Colacito, G. Metcalfe and S. Santschi)
  Speaker: Nick Galatos (University of Denver)
  Date: Wednesday, 12 May, 2021.
  Time: 16:00 (CEST)
  Location: Online (Zoom Meeting ID 922-5064-0302)
  [abstract]

  ---

  Lattice-ordered groups (l-groups) form natural algebraic structures and have been studied extensively. Holland's embedding theorem shows that every l-group can be embedded in the order automorphisms of a chain, while l-groups play an important role in the algebraic semantics of substructural logics (for example in relation to abelian relevance logic, MV-algebras, BL-algebras, cancellative residuated lattices). We study the subreducts of l-groups where the inverse operation is dropped; the resulting structures are distributive lattice-ordered monoids (DLMs). We focus on the abelian case, the representable/semilinear case and the general case, and explore connections between the full structures and their subreducts.

  We show that an inverse-free equation is valid in all l-groups iff it is valid in all DLMs; this contrasts with the abelian case where a discrepancy was known to exist. We prove that the discrepancy in the equation theories also holds in the semilinear case and we provide an axiomatization of semilinear DLMs.

  Furthermore, we prove that, surprisingly, every l-group equation is equivalent to an inverse-free equation, a fact that allows the reduction of the full equational theory of l-groups to that of DLMs. This further leads to a hybrid sequent/hypersequent calculus for l-groups, given that DLM's admit residuated frames semantics.

  We show that DLMs have the finite model property, and thus a decidable equational theory, and that they are generated as a variety by the DLM of all order-automorphisms of the rationals. Finally, we establish a correspondence between the validity of DLM equations and the existence of right orders on free monoids. As a byproduct we obtain that every right order on the free monoid extends to a right order on the free group.

  ---



• Title: Expressive Logics for Coinductive Predicates
  Speaker: Jurriaan Rot (Radboud University)
  Date: Wednesday, 28 April, 2021.
  Time: 16:00 (CEST)
  Location: Online (Zoom Meeting ID 922-5064-0302)
  [abstract]

  ---

  The classical Hennessy-Milner theorem says that two states of an image-finite transition system are bisimilar if and only if they satisfy the same formulas in a certain modal logic. We study this type of result in a general context, moving from transition systems to coalgebras and from bisimilarity to coinductive predicates. We formulate when a logic fully characterises a coinductive predicate on coalgebras, by providing suitable notions of adequacy and expressiveness, and give sufficient conditions on the semantics. This instantiates to expressiveness of logics for diverse predicates such as similarity, divergence of processes and a simple behavioural metric on automata.

  This is joint work with Clemens Kupke.

  ---



• Title: The topological mu-calculus
  Speaker: David Fernández-Duque (Gent University)
  Date: Wednesday, 21 April, 2021.
  Time: 16:00 (CEST)
  Location: Online (Zoom Meeting ID 922-5064-0302)
  [abstract]

  ---

  Joint work with Alexandru Baltag and Nick Bezhanishvili

  The language of the unimodal mu-calculus is readily interpretable over the class of topological spaces, both with the closure and derivative interpretations. Previous work by Goldblatt, Hodkinson, and others had focused on the special case of TD-spaces, but the generalization to arbitrary topological spaces poses some challenges. In this talk we will show that the topological mu-calculus is complete and decidable not only over the class of all topological spaces, but over a large collection of classes whose modal logic satisfies some natural conditions.

  ---



• Title: Towards a Proof Theory of Probabilistic Logics
  Speaker: Matteo Mio (ENS-Lyon)
  Date: Wednesday, 14 April, 2021.
  Time: 16:00 (CEST)
  Location: Online (Zoom Meeting ID 922-5064-0302)
  [abstract]

  ---

  Probabilistic Logics are formal languages designed to express properties of probabilistic programs. For most probabilistic logics several key problems are still open. One of such problems is to design convenient analytical proof systems in the style of Gentzen sequent calculus. This is practically important in order to simplify the task of proof search: the CUT-elimination theorem greatly reduces the search space. In this talk I will present some recent developments in this direction.

  ---



• Title: Measure-theoretic semantics for quantitative linear-time logics
  Speaker: Corina Cirstea (University of Southampton)
  Date: Wednesday, 31 March, 2021.
  Time: 16:00 (CEST)
  Location: Online (Zoom Meeting ID 922-5064-0302)
  [abstract]

  ---

  This talk will take a fresh look at the quantitative fixpoint logics described in [1], showing that in addition to a standard coalgebraic semantics and an equivalent automata-theoretic semantics, a measure-theoretic semantics can also be provided. Altogether this makes these logics similar to probabilistic Linear Time Logic, and further justifies their use in quantitative verification. In particular, instances of these logics can be used to reason about systems wherein the amount of resources required to achieve a certain behaviour is a key concern.

  [1] C. Cirstea, S. Shimizu and I. Hasuo. Parity Automata for Quantitative Linear Time Logics, Proceedings of CALCO 2017, volume 72 of Leibniz International Proceedings in Informatics, 2017.

  ---



• Title: A proof-theoretic approach to formal epistemology (joint work with Edi Pavlović)
  Speaker: Sara Negri (Università degli Studi di Genova)
  Date: Wednesday, 17 March, 2021.
  Time: 16:00 (CET)
  Location: Online (Zoom Meeting ID 922-5064-0302)
  [abstract]

  ---

  Ever since antiquity, attempts have been made to characterize knowledge through belief augmented by additional properties such as truth and justification. These characterizations have been challenged by Gettier counterexamples and their variants.

  A modern proposal, what is known as defeasibility theory, characterizes knowledge through stability under revisions of beliefs on the basis of true or arbitrary information (Hintikka (1962), Stalnaker (1998)). A formal investigation of such a proposal calls for the methods of dynamic epistemic logic: well-developed semantic approaches to dynamic epistemic logic have been given through plausibility models of Baltag and Smets (2008) and Pacuit (2013), but a corresponding proof theory is still in its beginning.

  We shall recast plausibility models in terms of the more general neighbourhood models and develop on their basis complete proof systems, following a methodology introduced in Negri (2017) and developed for conditional doxastic notions in Girlando et al. (2018).

  An inferential treatment of various epistemic and doxastic notions such as safe belief and strong belief will give a new way to study their relationships; among these, the characterization of knowledge as belief stable under arbitrary revision will be grounded through formal labelled sequent calculus derivations.

  ---



• Title: On cut-elimination for the Grzegorczyk modal logic (Slides)
  Speaker: Daniyar Shamkanov (Steklov Mathematical Institute)
  Date: Wednesday, 3 March, 2021.
  Time: 16:00 (CET)
  Location: Online (Zoom Meeting ID 922-5064-0302)
  [abstract]

  ---

  We are going to examine a sequent calculus for the Grzegorczyk modal logic Grz with non-well-founded proofs and discuss the cut-elimination theorem for it. In order to avoid nested co-inductive and inductive reasoning in the proof of cut-elimination, we adopt an approach from denotational semantics of computer languages, where program types are interpreted as ultrametric spaces and fixed-point combinators are encoded using fixed-point theorems. We consider the set of non-well-founded proofs of Grz and various sets of operations acting on these proofs as ultrametric spaces and define the cut-elimination operator following the lines of the Priess-Crampe fixed-point theorem. If time permits, we will also discuss how this approach to cut-elimination can be applied in the case of the modal logic of transitive closure. This is a joint work with Yury Savateev.

  ---



• Title: Strong Completeness in Topological Semantics
  Speaker: Philip Kremer (University of Toronto)
  Date: Wednesday, 17 February, 2021.
  Time: 16:00 (CET)
  Location: Online (Zoom Meeting ID 922-5064-0302)
  [abstract]

  ---

  In the topological semantics for modal logic, S4 is well-known to be complete for the rational line, for the real line, and for Cantor space: these are special cases of S4’s completeness for any dense-in-itself metric space. The construction used to prove completeness can be slightly amended to show that S4 is not only complete, but also strongly complete, for the rational line. But no similarly easy amendment is available for the real line or for Cantor space. In 2013, I proved that S4 is strongly complete for any dense-in-itself metric space, taking a detour through algebraic semantics. In this talk, I will review that proof.

  ---



• Title: Guarded Kleene Algebra with Tests: Coequations, Coinduction, and Completeness
  Speaker: Alexandra Silva (University College London)
  Date: Wednesday, 3 February, 2021.
  Time: 16:00 (CET)
  Location: Online (Zoom Meeting ID 922-5064-0302)
  [abstract]

  ---

  Guarded Kleene Algebra with Tests (GKAT), the efficient fragment of KAT, allows for almost linear decidability of equivalence. In this paper, we prove a completeness theorem for GKAT. This settles an open problem in Smolka et al. (2020), where a strong Uniqueness of Solutions axiom was used to derive completeness. We derive it as a corollary, exhibiting its dependence on the other axioms. Along the way, we prove a second completeness theorem for a reduced version of GKAT without so-called early termination. These two results are crucial as foundations to use GKAT in its intended purpose as a language for program verification. Interestingly, they also unveil a more general approach to completeness based on coequations and coinduction. Joint work with Todd Schmid, Tobias Kappe, and Dexter Kozen.

  ---



• Title: Isotropy Groups of Quasi-Equational Theories (Slides, PhD Thesis, Journal article)
  Speaker: Jason Parker (Brandon University)
  Date: Wednesday, 6 January, 2021.
  Time: 16:00 (CET)
  Location: Online (Zoom Meeting ID 922-5064-0302)
  [abstract]

  ---

  In [2], my PhD supervisors (Pieter Hofstra and Philip Scott) and I studied the new topos-theoretic phenomenon of isotropy (as introduced in [1]) in the context of single-sorted algebraic theories, and we gave a logical/syntactic characterization of the isotropy group of any such theory, thereby showing that it encodes a notion of inner automorphism or conjugation for the theory. In the present talk, I will summarize the results of my recent PhD thesis, in which I build on this earlier work by studying the isotropy groups of (multi-sorted) quasi-equational theories (also known as essentially algebraic, cartesian, or finite limit theories). In particular, I will show how to give a logical/syntactic characterization of the isotropy group of any such theory, and that it encodes a notion of inner automorphism or conjugation for the theory. I will also describe how I have used this characterization to exactly characterize the ‘inner automorphisms’ for several different examples of quasi-equational theories, most notably the theory of strict monoidal categories and the theory of presheaves valued in a category of models. In particular, the latter example provides a characterization of the (covariant) isotropy group of a category of set-valued presheaves, which had been an open question in the theory of categorical isotropy.

  [1] J. Funk, P. Hofstra, B. Steinberg. Isotropy and crossed toposes. Theory and Applications of Categories 26, 660-709, 2012.
  [2] P. Hofstra, J. Parker, P.J. Scott. Isotropy of algebraic theories. Electronic Notes in Theoretical Computer Science 341, 201-217, 2018.

  ---

• Title: The Univalence Principle
  Speaker: Paige Randall North (Ohio State University)
  Date: Wednesday, 2 December, 2020.
  Time: 15:00 (CET) Note: this seminar will be held one hour earlier than usual.
  Location: Online (Zoom Meeting ID 922-5064-0302)
  [abstract]

  ---

  The Equivalence Principle is an informal principle asserting that equivalent mathematical objects have the same properties. In Univalent Foundations -- a foundation of mathematics based on dependent type theory -- this principle has been formally stated and proven for various sorts of structured sets (such as monoids, groups, etc) and for categories. In fact, this follows from a similar principle that has been formally stated and proven in these cases: the Univalence Principle. This says that any two equivalent mathematical objects are equal. In this talk, I will describe a Univalence Principle that holds for more sorts of mathematical objects and, in particular, many higher-categorical structures. This is joint work with Benedikt Ahrens, Mike Shulman, and Dimitris Tsementzis.

  ---

• Title: Effective Kan fibrations in simplicial sets
  Speaker: Benno van den Berg (ILLC)
  Date: Wednesday, 4 November, 2020.
  Time: 16:00 (CET)
  Location: Online (Zoom Meeting ID 922-5064-0302)
  [abstract]

  ---

  Homotopy type theory started in earnest when Voevodsky formulated his univalence axiom and showed that the category of simplicial sets hosts a model of type theory in which this axiom holds. After he made these contributions, people wondered to which extent this model can be developed in a constructive metatheory and can be exploited for computational purposes. Some serious obstacles were found and in response many researchers switched to cubical sets and started working on "cubical type theories". In joint work with Eric Faber I have developed an approach which seeks to circumvent the obstructions for developing a simplicial sets model for homotopy type theory in a constructive fashion. In this talk I will try to give some idea of how we try to do this, what we have achieved thus far and how our project compares to related ones by Gambino, Henry, Szumilo and Sattler.

  ---

• Title: A Functional (Monadic) Second-Order Theory of Infinite Trees
  Speaker: Colin Riba (ENS de Lyon)
  Date: Wednesday, 21 October, 2020.
  Time: 16:00 (CEST)
  Location: Online (Zoom Meeting ID 922-5064-0302)
  [abstract]

  ---

  We present a complete axiomatization of Monadic Second-Order Logic (MSO) over infinite trees. By a complete axiomatization we mean a complete deduction system with a polynomial-time recognizable set of axioms. By naive enumeration of formal derivations, this formally gives a proof of Rabin’s Tree Theorem (the decidability of MSO over infinite trees). The deduction system consists of the usual rules for second-order logic seen as two-sorted first-order logic, together with the natural adaptation to infinite trees of the axioms of MSO on ω-words. In addition, it contains an axiom scheme expressing the (positional) determinacy of certain parity games.

  The main difficulty resides in the limited expressive power of the language of MSO. We actually devise an extension of MSO, called Functional (Monadic) Second-Order Logic (FSO), which allows us to uniformly manipulate (hereditarily) finite sets and corresponding labeled trees, and whose language allows for higher abstraction than that of MSO.

  ---

• Title: Guarded Kleene Algebra with Tests
  Speaker: Tobias Kappé (Cornell University)
  Date: Wednesday, 7 October, 2020.
  Time: 16:00 (CEST)
  Location: Online (Zoom Meeting ID 922-5064-0302)
  [abstract]

  ---

  A Guarded Kleene Algebra with Tests (GKAT) is a type of Kleene Algebra with Tests (KAT) that arises by restricting the operators of KAT to "deterministic" (predicate-guarded) versions. This makes GKAT especially suited to reason about flow control in imperative programs. In contrast with KAT, where the equivalence problem is PSPACE-complete, we show that equivalence in GKAT can be decided in almost linear time. We also provide a full Kleene theorem and prove completeness w.r.t. a Salomaa-style axiomatization, both of which require us to develop a coalgebraic theory of GKAT.

  ---

• Title: Modal Intuitionistic Logics as Dialgebraic Logics
  Speaker: Jim de Groot (Australian National University)
  Date: Wednesday, 8 July, 2020.
  Time: 11:00 (CEST) Note: this seminar will be held at a unusual time.
  Location: Online (Zoom Meeting ID 922-5064-0302)
  [abstract]

  ---

  In a recent LICS paper, Dirk Pattinson and I generalised the paradigm of coalgebraic logic to what we call dialgebraic logic. The main motivation behind this was to provide a coalgebra-like framework for modal intuitionistic logics. In this talk, I will explain the main ideas and constructions from the paper.

  Guided by an easy example of a modal intuitionistic logic we will see where the coalgebraic approach breaks down. We then use the notion of a dialgebra to fix this problem. This leads to a general (dialgebraic) framework, where modal logics can be given by predicate liftings and axioms, in a similar fashion as for Set-coalgebras. Finally, we investigate a categorical notion of completeness, obtain a general completeness result, and instantiate this to our example.

  ---



• Title: Choice-Free Duality for Orthocomplemented Lattices
  Speakers: Joseph McDonald (ILLC) & Kentarô Yamamoto (UC Berkeley)
  Date: Wednesday, 1 July, 2020.
  Time: 17:00 (CEST) Note: this seminar starts one hour later than usual.
  Location: Online (Zoom Meeting ID 922-5064-0302)
  [abstract]

  ---

  The aim of this talk is to outline our ongoing research in which we are developing a choice-free topological duality for orthocomplemented lattices (or simply, ortholattices) by means of a special subclass of spectral spaces, which we call upper Vietoris orthospaces (or simply, UVO-spaces). Our techniques combine the choice-free spectral space approach to the topological duality theory of Boolean algebras developed by Bezhanishvili and Holliday with the choice-dependent Stone space approach to the topological duality theory of ortholattices originally developed by Goldblatt, and then later by Bimbo. In light of this duality, we will discuss the "duality dictionary" we are currently developing, which makes explicit the translation between ortholattice and UVO-space concepts. Lastly, we discuss how our duality relates to other dualities and what applications we hope to explore.

  ---



• Title: From choice-free Stone duality to choice-free model theory?
  Speaker: Wesley Holliday (UC Berkeley)
  Date: Wednesday, 24 June, 2020.
  Time: 17:00 (CEST) Note: this seminar starts one hour later than usual.
  Location: Online (Zoom Meeting ID 922-5064-0302)
  [abstract]

  ---

  In a recent paper, "Choice-free Stone duality" (JSL, March 2020), Nick Bezhanishvili and I developed a choice-free duality theory for Boolean algebras using special spectral spaces, called upper Vietoris spaces (UV-spaces). In this talk, I will cover the basics of this duality and explain how it leads to “possibility semantics” for classical first-order logic. While the completeness theorem for first-order logic for uncountable languages with respect to traditional Tarskian models requires a nonconstructive choice principle unprovable in ZF set theory, I will sketch a choice-free proof of the completeness theorem for first-order logic for arbitrary languages with respect to possibility models. This result raises the prospect of a program of “choice-free model theory."

  ---



• Title: Slanted Canonicity of Analytic Inductive Inequalities
  Speaker: Laurent De Rudder (Université de Liège)
  Date: Wednesday, 17 June, 2020.
  Time: 16:00 (CEST)
  Location: Online (Zoom Meeting ID 922-5064-0302)
  [abstract]

  ---

  In this talk, we broach an algebraic canonicity theorem for normal LE-logics of arbitrary signature in the generalized setting of slanted algebras, i.e. lattices expansions in which the non-lattice operations map tuples of elements of the given lattice to closed or open elements of its canonical extension. Interestingly, the syntactic shape of LE-inequalities which guarantees canonicity in this generalized setting turns out to coincide with the shape of analytic inductive inequalities, which guarantees LE-inequalities to be equivalently captured by analytic structural rules of a proper display calculus.

  ---

• Title: Temporal interpretation of intuitionistic quantifiers (Joint work with G. Bezhanishvili)
  Speaker: Luca Carai (New Mexico State University)
  Date: Wednesday, 10 June, 2020.
  Time: 16:00 (CEST)
  Location: Online
  [abstract]

  ---

  In this talk we discuss how to provide a temporal interpretation of intuitionistic quantifiers: the universal quantifier is interpreted as "for every object in the future" and the existential quantifier as "for some object in the past". One of the merits of this perspective is overcoming the non-symmetry of the interpretation of quantifiers in the usual Kripke semantics for the predicate intuitionistic logic IQC.

  Our goal is to adapt the predicate Gödel translation to a translation of IQC into a suitable tense logic. Because of issues related to constant domains, we cannot choose the predicate tense S4 system QS4.t as the target of the translation. Following the work of Corsi, we introduce the tense logic Q°S4.t obtained by weakening the axioms of QS4.t. We then supply a full and faithful translation of IQC into Q°S4.t whose faithfulness is shown using syntactic methods and its fullness is proved utilizing the generalized Kripke semantics of Corsi.

  ---

• Title: Separable MV-algebras (Joint work with V. Marra)
  Speaker: Matías Menni (Conicet and Universidad Nacional de La Plata)
  Date: Wednesday, 3 June, 2020.
  Time: 16:00 (CEST)
  Location: Online
  [abstract]

  ---

  We will recall the definition of decidable object in an extensive category and characterize the decidable objects in the opposite of the category of MV-algebras.

  ---

• Title: Are locally finite MV-algebras a variety? (Joint work with M. Abbadini)
  Speaker: Luca Spada (Università degli Studi di Salerno)
  Date: Wednesday, 13 May, 2020.
  Time: 16:00 (CEST)
  Location: Online
  [slides]
  [abstract]

  ---

  We answer Mundici's problem number 3 (Advances Lukasiewicz calculus, page 235): Is the category of locally finite MV-algebras equivalent to an equational class? We prove:

  1. The category of locally finite MV-algebras is not equivalent to any finitary variety of algebras. More is true: the category of locally finite MV-algebras is not equivalent to any finitely-sorted finitary quasi-variety of algebras.
  2. The category of locally finite MV-algebras is equivalent to a variety of infinitary algebras (with operations of countable arity).
  3. The category of locally finite MV-algebras is equivalent to a countably-sorted variety of finitary algebras.

  Our proofs rest upon the duality between locally finite MV-algebras and the category of multisets by Cignoli, Dubuc and Mundici, and categorical characterisations of varieties and quasi-varieties proved by Lawvere, Duskin and many others.

  ---

• Title: Describable Nuclea, Negative Translations and Extension Stability
  Speaker: Tadeusz Litak (FAU Erlangen-Nürnberg)
  Date: Tuesday, 12 May, 2020.
  Time: 14:00 (CEST)
  Location: Online (see the TULIPS webpage note: pre-registration required)
  [abstract]

  ---

  What do soundness/completeness of negative translations of intutionistic modal logics, extension stability of preservativity/provability logics and the use of nuclea on Heyting Algebra Expansions (HAEs) to form other HAEs have in common? As it turns out, in all those cases one appears to deal with a certain kind of subframe property for a given logic, i.e., the question whether the logic in question survives a transition to at least some types of substructures of its Kripke-style or neighourhood-style frames. The nucleic perspective on subframe logics has been introduced by Silvio Ghilardi and Guram Bezhanishvili (APAL 2007) for the purely superintuitionistic syntax (without modalities or other additional connectives). It has not been used so much in the modal setting, mostly because the focus in the field tends to be on modal logics with classical propositional base, and nuclea are a rather trivial notion in the boolean setting. However, things are very different intuitionistically. Since the 1970’s, nuclea have been studied in the context of point-free topologies (lattice-complete Heyting algebras), sheaves and Grothendieck topologies on toposes, and finally arbitrary Heyting algebras (Macnab 1981). Other communities may know them as “lax modalities” or (a somewhat degenerate case of) “strong monads”.

  We marry the nuclei view on subframe properties with the framework of “describable operations” introduced to study subframe logics in Frank Wolter’s PhD Thesis (1993). Wolter’s original setting was restricted to classical modal logics, but with minimal care his setup can be made to work intuitionistically and nuclea provide the missing ingredient to make it fruitful. From this perspective, we revisit the FSCD 2017 study soundness and completeness of negative translations in modal logic (joint work with Miriam Polzer and Ulrich Rabenstein) and our present study of extension stability for preservativity logics based on the constructive strict implication (jointly with Albert Visser). Various characterization and completeness results can be obtained in a generic way.

  [This instalment of the seminar is joint with TULIPS at the Department of Philosophy and Religious Studies of Utrecht University.]

  ---

• Title: Modal logic and measurable cardinals
  Speaker: Guram Bezhanishvili (New Mexico State University)
  Date: Wednesday, 29 April, 2020.
  Time: 16:00
  Location: Online
  [abstract]

  ---

  I will discuss our recent result that characterizes the existence of a measurable cardinal in terms of the topological completeness of a simple modal logic with respect to a normal space.

  Joint work with N. Bezhanishvili, J. Lucero-Bryan, and J. van Mill

  ---

• Title: Circular proofs for the hybrid mu-calculus
  Speaker: Sebastian Enqvist (Stockholms universitet)
  Date: Wednesday, 15 April, 2020.
  Time: 16:00
  Location: Online
  [abstract]

  ---

  Circular proofs have recently been used by Afshari and Leigh to prove completeness of a cut-free sequent calculus for the modal mu-calculus. They make use of an annotated circular proof system due to Jungteerapanich and Stirling, which uses a system of names for fixpoint unfoldings. In this talk I present a circular proof system in the same style for the hybrid mu-calculus, extending the modal mu-calculus with nominals and satisfaction operators. My hope is that this work will be a starting point towards developing complete proof systems for extensions of the mu-calculus that lack the tree model property, like guarded fixpoint logic and two-way mu-calculus. I will present the proof system and outline some key parts of the completeness proof, and try to explain some of the difficulties posed by the hybrid operators.

  ---

• Title: Unification in coalgebraic modal logics
  Speaker: Johannes Marti (ILLC)
  Date: Wednesday, 1 April, 2020.
  Time: 16:00
  Location: Online
  [abstract]

  ---

  In this talk I present a characterization of the unification problem in coalgebraic modal logics in terms of the existence of a morphism between one-step coalgebras.

  The unification problem is the following decision problem: Given two terms in the free algebra of some variety, is there a substitution under which they are equal? In the work presented in this talk we consider the unification problem for varieties whose free algebras are the syntactic algebras of coalgebraic modal logics. We apply ideas from Ghilardi's characterization of the substitution in the theory of normal forms to reformulate the unification problem on the level of the one-step coalgebras that are dual to the one-step algebras approximating the free algebra. The advantage of this approach is that in many interesting cases the points of one-step coalgebras are finite tree-like objects and the unification problem becomes a combinatorial problem about these trees.

  We consider three instances of this characterization:

  1. We obtain a new proof of the decidability of unification for the modal logic (Alt1), which was originally established by Balbiani and Tinchev. (Alt1) is the modal logic of the class of frames in which every world has at most one successor. With our characterization the decidability of unification in this logic follows from a simple pumping argument.
  2. As a variation on the previous example we consider the logic over frames in which every world has exactly one successor that is labeled with either 0 or 1. In this case the unification problem can be reformulated as the question whether there exists a graph homomorphism from some de Bruijn graph into a graph given in the input. So far, we have not been able to establish whether this problem is decidable or not.
  3. An important motivation for developing our characterization is that the modal logic K can be presented as a coalgebraic modal logic. Despite considerable efforts the decidability of unification in K is an open question.

  ---

• Title: Nested sequents for the logic of conditional belief
  Speaker: Marianna Girlando (Inria Saclay - LIX)
  Date: Wednesday, 11 March, 2020.
  Time: 16:00
  Location: Room F3.20, Science Park 107, Amsterdam.
  [abstract]

  ---

  Conditional Doxastic Logic (CDL) is a multi-agent epistemic logic introduced by Baltag and Smets to model the conditional beliefs of an agent. In this talk I introduce a natural neighbourhood semantics for the static fragment of CDL. I then present a nested sequent calculus, sound and complete with respect to neighbourhood models for CDL. The proof system is analytic, has a direct formula interpretation and provides a decision procedure for CDL. Moreover, since the logic can be embedded into the multi-agent version of modal logic S5, called S5i, our proof system can be used to define a nested sequent calculus for S5i.

  This talk is based on a joint work with Björn Lellmann and Nicola Olivetti.

  ---

• Anne Troelstra Memorial Event
  Date: Friday, March 6, 2020
  Location: Amsterdam Science Park Congress Centre, Science Park 105, Amsterdam.
  [More information]

• Title: From Complementary Logic to Proof-Theoretic Semantics
  Speaker: Gabriele Pulcini (ILLC)
  Date: Wednesday, 4 March, 2020.
  Time: 16:00
  Location: Room F1.15, Science Park 107, Amsterdam.
  [abstract]

  ---

  Two proof-systems P and P* are said to be complementary when one proves exactly the non-theorems of the other. Complementary systems come as a particular kind of refutation calculi whose patterns of inference always work by inferring unprovable conclusions form unprovable premises.

  In the first part of my talk, I will focus on LK*, the sequent system complementing Gentzen system LK for classical logic. I will show, then, how to enrich LK* with two admissible (unary) cut rules, which allow for a simple and efficient cut-elimination algorithm. In particular, two facts will be highlighted: 1) for any given provable sequent, complementary cut-elimination always returns one of its simplest proofs, and 2) provable LK* sequents turn out to be "deductively polarized" by the empty sequent.

  In the second part, I will observe how an alternative complementary sequent system can be obtained by slightly modifying Kleene's system G4. I will finally show how this move could pave the way for a novel approach to multi-valuedness and proof-theoretic semantics for classical logic.

  ---

• Title: One step to admissibility in intuitionistic Gödel-Löb logic
  Speaker: Iris van der Giessen (Universiteit Utrecht)
  Date: Wednesday, 19 February, 2020.
  Time: 16:00
  Location: Room F1.15, Science Park 107, Amsterdam.
  [abstract]

  ---

  I would like to present ongoing work on intuitionistic modal logics iGL and iSL which have a close connection to the (unknown!) provability logic of Heyting Arithmetic. Classically, Gödel-Löb logic GL admits a provability interpretation for Peano Arithmetic. iGL is its intuitionistic counterpart and iSL is iGL extended by explicit completeness principles. I will characterize both systems via an axiomatization and in terms of Kripke models. The main goal is to understand their admissible rules in order to get insight in the structure of those logics. To do so, I want to focus on one step in this direction: Ghilardi’s wonderful result connecting projective formulas to the extension property in Kripke models.

  ---

• Title: Guarded Recursion for Coinductive and Higher-Order Stochastic Systems
  Speaker: Henning Basold (Universiteit Leiden)
  Date: Wednesday, 22 January, 2020.
  Time: 14:30
  Location: Room F1.15, Science Park 107, Amsterdam.
  [abstract]

  ---

  In stochastic modelling, as it appears in artificial intelligence, biology or physics, one often encounters the question of how to model a probabilistic process that may run indefinitely. Such processes have been described in non-probabilistic programming successfully by using coinductive types and coiteration. Vákár et al. (POPL'19) introduced semantics for a higher-order probabilistic programming language with full recursion in types and programs based on quasi-Borel spaces. Full recursion allows the introduction of coinductive types, but this comes at the price of losing termination and productivity.

  In this talk, we will discuss a language and its semantics for stochastic modelling of processes that run potentially indefinitely, like random walks, and for distributions that arise from indefinite runs, like geometric distributions. Such processes and distributions will be described as so-called coinductive types and programmed via so-called guarded recursion, which ensures that the programs describing random walks etc. are terminating. Central to guarded recursion is the so-called later modality, which allows one to express that the computation of an element of a type is delayed. This allows one to use type-checking to ensure termination instead of, e.g., syntactic guardedness. This eases reasoning about such processes, while the recursion offered by the language is still convenient to use.

  The language appeared in the paper "Coinduction in Flow — The Later Modality in Fibrations" that I presented at CALCO'19, see here.

  ---

• Workshop on the occasion of Dick de Jongh's 80th Birthday
  When: Wednesday, November 27, 2019
  Where: ILLC's Common Room, SP107, F1.21.
  [More information]

• Title: Points of Boolean contact algebras
  Speaker: Rafał Gruszczyński (Nicolaus Copernicus University in Toruń)
  Date: Wednesday, 6 November, 2019.
  Time: 16:00
  Location: Room F3.20, Science Park 107, Amsterdam.
  [abstract]

  ---

  One of the main tasks of philosophically oriented point-free theories of space is to deliver a plausible definition of points, entities which are assumed as primitives in point-based geometries and topologies. It is understood that - unlike in case of algebraically oriented theories of frames and locales - such definitions should be intuitive from geometrical point of view, and should refer to objects which can be interpreted in the real world. Thus points are replaced by regions and the former are explained as abstractions from the latter. The main purpose of the talk is to draw a comparison between three seminal defintions of points: Andrzej Grzegorczyk's, Alfred Whitehead's and Hendrik De Vries's, within the framework of Boolean contact algebras.

  ---

• Title: Profinite Heyting algebras and the representation problem for Esakia spaces
  Speaker: Tommaso Moraschini (Czech Academy of Sciences and University of Barcelona)
  Date: Wednesday, 23 October, 2019.
  Time: 16:00
  Location: Room F1.15, Science Park 107, Amsterdam.
  [abstract]

  ---

  A poset is said to be "representable" if it can be endowed with an Esakia topology. Gratzer's classical representation problem asks for a description of representable posets. A solution to this problem is not expected to take a simple form, as representable posets do not form an elementary class. Since at the moment a solution to the representation problem seems out of reach, we will address a simpler version of the problem which, roughly speaking, asks to determine the posets that may occur as top parts of Esakia spaces. Crossing the bridge between algebra and topology, this task amounts to characterizing the profinite Heyting algebras that are also profinite completions of some Heyting algebras. We shall report on the on-going effort to solve this problem, and on some preliminary results.

  This talk is based on joint work with G. Bezhanishvili, N. Bezhanishvili, and M. Stronkowski.

  ---

• Workshop on the occasion of Frederik Lauridsen’s PhD defense
  Title: Algebraic and Proof Theoretic Methods in Non-Classical Logic
  When: Thursday and Friday, October 10 - 11, 2019
  Where: Potgieterzaal (C0.01), University Library, Singel 425, Amsterdam.
  [More information]

• Title: Internal PCAs and their Slices
  Speaker: Jetze Zoethout (Utrecht University)
  Date: Wednesday, 2 October, 2019.
  Time: 16:00
  Location: Room F1.15, Science Park 107, Amsterdam.
  [abstract]

  ---

  A partial combinatory algebra (PCA) is an abstract model of computability. Every such PCA gives rise to a category of assemblies, which can be seen as the category of all datatypes that can be implemented in this PCA. It turns out that the class of all categories that arise in this way is not closed under slicing.

  In this talk, we will study a generalization of PCAs introduced by Wouter Stekelenburg, which has the property that the corresponding class of categories of assemblies is closed under slicing. These more general PCAs are constructed internally in a regular category, and express a relative notion of computability. We show how to perform the slice construction at the level of PCAs, and we show that these generalized PCAs, like the classical PCAs, form a 2-category. Moreover, we generalize the notion of computational density studied by Pieter Hofstra and Jaap van Oosten to the current setting.

  ---

• Title: A Quillen model structure for bigroupoids and pseudofunctors
  Speaker: Martijn den Besten (ILLC)
  Date: Wednesday, 2 October, 2019.
  Time: 15:00
  Location: Room F1.15, Science Park 107, Amsterdam.
  [abstract]

  ---

  A key notion in modern homotopy theory is that of a Quillen model structure. This concept was designed to capture axiomatically some of the essential properties of homotopy of topological spaces. A model structure is determined by specifying three classes of morphisms satisfying certain conditions. These conditions are motivated by the properties of certain classes of continuous functions in the category of topological spaces. Indeed, categories whose objects can be thought of as spaces often admit the structure of a model category. Awodey and Warren showed that Martin-Löf type theory with identity types can essentially be interpreted in any such category.
  
  In this talk, I will present a model structure on the category of bigroupoids and pseudofunctors. In the construction of the model structure, two coherence theorems are used, which allow us to recognize that certain diagrams commute at a glance. I will also spend some time discussing these theorems.

  ---

• Title: Spatial Model Checking and Applications to Medical Image Analysis
  Speaker: Vincenzo Ciancia (Institute of Information Science and Technologies “A. Faedo”)
  Date: Tuesday, 1 October, 2019.
  Time: 16:00
  Location: Room F1.15, Science Park 107, Amsterdam.
  [abstract]

  ---

  Spatial aspects of computation are prominent in Computer Science, especially when dealing with systems distributed in physical space or with image data acquired from various sources. However, formal verification techniques are usually concerned with temporal properties and do not explicitly handle spatial information.
  
  Our work stems from the topological interpretation of modal logics, the so-called Spatial Logics. We present a topology-based approach to model checking for spatial and spatio-temporal properties. Our results include theoretical developments in the more general setting of Cech closure spaces, a study of a "collective" variant, that has been compared to region calculi in recent work, publicly available software tools, and some case studies in the setting of smart transportation.
  
  In recent joint work with the University Hospital of Siena, we have explored the application domain of automatic contouring in Medical Imaging, introducing the tool VoxLogicA, which merges the state-of-the-art imaging library ITK with the unique combination of declarative specification and optimised execution provided by spatial model checking. The analysis of an existing benchmark of medical images for segmentation of brain tumours shows that simple VoxLogicA specifications can reach state-of-the-art accuracy, competing with best-in-class algorithms based on machine learning, with the advantage of explainability and easy replicability.

  ---

• Title: Exponentiability and Theories of Dependent Types
  Speaker: Taichi Uemura (ILLC)
  Date: Wednesday, 11 September, 2019.
  [abstract]

  ---

  I give a close relationship between exponentiable arrows in categories with finite limits and dependent type theories. Precisely, the opposite of the category of finitely presentable dependent type theories has an exponentiable arrow and is freely generated by this arrow (and some others) in a suitable sense. I will discuss some applications of this observation to the semantics of dependent type theory.

  ---

• Title: Coalgebraic positive logic and lifting functors
  Speaker: Jim de Groot (The Australian National University)
  Date: Wednesday, 26 June, 2019.
  [abstract]

  ---

  We recall coalgebraic semantics of positive modal logic and consider several examples. We encounter coalgebras for endofunctors on Pre, Pos and Pries, the categories of preorders, posets and Priestley spaces, respectively, and interpret Dunn's positive modal logic on these via predicate liftings. Thereafter, we investigate how endofunctors on these categories relate. In particular, we give two ways of lifting functors from Pos to Pries and investigate when these methods coincide.

  ---

• Title: Completeness of Game Logic
  Speaker: Helle Hvid Hansen (Delft University of Technology)
  Date: Wednesday, 22 May, 2019.
  [abstract]

  ---

  Game logic was introduced by Rohit Parikh in the 1980s as a generalisation of propositional dynamic logic (PDL) for reasoning about outcomes that players can force in determined 2–player games. Semantically, the generalisation from programs to games is mirrored by moving from Kripke models to monotone neighbourhood models. Parikh proposed a natural PDL-style Hilbert system which was easily proved to be sound, but its completeness has thus far remained an open problem.
  
  In this talk, I will present the results from a paper that will be presented at LICS 2019. In the paper, we present a cut-free sequent calculus for game logic and two cut–free sequent calculi that manipulate annotated formulas, one for game logic and one for the monotone μ–calculus. We show these systems are sound and complete, and that completeness of Parikh’s axiomatization follows. Our approach builds on recent ideas and results by Afshari & Leigh (LICS 2017) in that we obtain completeness via a sequence of proof transformations between the systems. A crucial ingredient is a validity-preserving translation from game logic to the monotone μ–calculus.
  
  This is joint work with Sebastian Enqvist, Clemens Kupke, Johannes Marti and Yde Venema.

  ---

• Title: A universal proof theoretical approach to interpolation
  Speaker: Raheleh Jalali (Institute of Mathematics of the Czech Academy of Sciences)
  Date: Wednesday, 1 May, 2019.
  [abstract]

  ---

  In her recent works, Iemhoff introduced a connection between the existence of terminating sequent calculi of a certain kind and the uniform interpolation property of the super–intuitionistic logic that the calculus captures. In this talk, we will generalize this relationship to also cover the sub–structural setting on the one hand and a much more powerful class of rules on the other. The resulting relationship then provides a uniform method to establish uniform interpolation property for the logics FL_e, FL_ew, CFL_e, CFL_ew, IPC, CPC, their K and KD–type modal extensions and some basic non–normal modal logics including E, M, MC and MN. More interestingly though, on the negative side, we will show that no extension of FL_e can enjoy a certain natural type of terminating sequent calculus unless it has the uniform interpolation property. It excludes almost all super–intutionistic logics (except seven of them), the logic K4 and almost all the extensions of the logic S4 (except six of them) from having such a reasonable calculus.

  ---

• Title: Towards a Logic for Conditional Strategic Reasoning
  Speaker: Valentin Goranko (Stockholm University)
  Date: Wednesday, 17 April, 2019.
  [abstract]

  ---

  This talk is based on a work in progress, joint with Fengkui Ju, Beijing Normal University.
  
  We consider systems of rational agents who act in pursuit of their individual and collective objectives and we study the reasoning of an agent or an external observer about the consequences from the expected choices of action of the other agents, based on their objectives, in order to assess the agent’s ability to achieve her own objective.
  
  For instance, consider a scenario where an agent, Alice, has an objective O(A) to achieve. Suppose, that Alice has several possible choices of an action (or, strategy) that would possibly, or certainly, guarantee the achievement of her objective O(A). Now, Bob, another agent or an external observer, is reasoning about the consequences from Alice’s possible actions with respect to the occurrence of Bob’s objective or intended outcome O(B). Depending on Bob’s knowledge about Alice’s objective and of her available strategic choices that would guarantee the achievement of that objective, there can be several possible cases for Bob’s reasoning, based on whether or not Bob knows Alice’s objective, her possible actions towards achieving that objective, and her intentions on how to act. Thus, Bob has to reason about his own abilities to achieve his objective O(B), conditional on what he knows or expect that Alice may decide to do. That scenario naturally extends to several agents reasoning about their abilities conditional on how they expect the others to act.
  
  In some of these cases, reasoning about conditional strategic abilities can be formally described in Coalition Logic (CL) or in its temporal extension, the alternating time temporal logic ATL(*), with semantics involving strategy contexts. Other cases, however, require new and more expressive operators capturing more refined patterns of strategic ability, especially suited for the kind of conditional strategic reasoning in scenarios described above. In our work we introduce and study such new operators and logical languages that can capture variations of conditional strategic reasoning.
  
  In this talk, after an informal discussion of conditional strategic reasoning, I will introduce some new strategic operators capturing such reasoning, will provide formal semantics for the resulting logical languages and will discuss briefly their expressiveness and some of their meta-properties. I will conclude with some open questions for future research.
  
  [This instalment of the seminar was joint with LIRa Seminar.]

  ---

• Title: Flat fixpoint logics with converse modalities
  Speaker: Sebastian Enqvist (Stockholm University)
  Date: Wednesday, 3 April, 2019.
  [abstract]

  ---

  I present a completeness theorem for a class of flat modal fixpoint logics extended with the converse modality, continuing the work of Santocanale and Venema on flat fixpoint logics. I will also discuss some algebraic aspects of the results, in particular, concerning the property of constructiveness for free algebras and finitary O-adjoints.

  ---

• Title: Cyclic proofs for circular reasoning
  Speaker: Graham Leigh (University of Gothenburg)
  Date: Wednesday, 27 March, 2019.
  [abstract]

  ---

  Modal logic is an efficient and effective language for state-based reasoning. Its versatility is witnessed in its robustness when extended by non-local modalities: common knowledge, temporal modalities, computationally motivated `path quantifiers' and dynamic modalities, and even provability. These are all examples of modalities expressing infinitary properties of state systems: reachability or closure under fixpoint semantics. Logics built over these fixpoint modalities have natural semantics but provide a clear challenge to the development of sound and complete proof systems. In this talk, I will overview the proof theory of these expressive modal logics with a focus on re-interpreting the notion of proof in view of semantic considerations.

  ---

• Title: Trajectory domains: analyzing the behavior of transition systems
  Speaker: Levin Hornischer (ILLC)
  Date: Wednesday, 13 March, 2019.
  [abstract]

  ---

  We develop a novel way to analyze the possible long-term behavior of transition systems. These are discrete, possibly non-deterministic dynamical systems. Examples range from computer programs, over neural- and social networks, to `discretized' physical systems. We develop a notion of when two trajectories in a system—i.e., possible sequences of states—exhibit the same type of behavior (e.g., agreeing on equilibria and oscillations). Our object of study thus is the partial order of `behaviors', i.e., equivalence classes of trajectories ordered by extension.
  
  We identify subsystems such that, if absent, this behavior poset is an algebraic domain—whence the name `trajectory domain'. We show that they are in correspondence with a particular category of partial orders. We investigate the natural topology on the possible long-term behaviors. Finally, we comment on possible logics to reason about the behavior of a system and note curious similarities to spacetimes.

  ---

• Title: Coalgebra Learning via Duality
  Speaker: Clemens Kupke (University of Strathclyde)
  Date: Wednesday, 27 February, 2019.
  [abstract]

  ---

  A key result in computational learning theory is Dana Angluin's L* algorithm that describes how to learn a deterministic finite automaton (DFA) using membership and equivalence queries. I will present a generalisation of this algorithm to the level of coalgebras. The approach relies on the use of logical formulas as tests, based on a dual adjunction between states and logical theories. This allows us to learn, e.g., labelled transition systems, using modal formulas as tests.
  
  Joint work with Simone Barlocco and Jurriaan Rot.

  ---

• Title: Modal logics of polygons and beyondy
  Speaker: David Gabelaia (Tbilisi State University, A. Razmadze Mathematical Institute)
  Date: Wednesday, 30 January, 2019.
  [abstract]

  ---

  We will present results of an ongoing project investigating modal logics that arise from interpreting modal formulas as piecewise linear subsets (polyhedra) of an Euclidean space of dimension n>0.
  We will focus in the talk on the case of n=2 and show that the modal logic of 2D polygons is finitely axiomatizable, has the finite model property in its Kripke semantics and is decidable. The finite axiomatization boils down semantically to identifying the finite set of `forbidden' Kripke frames, to which non-frames of the logic are reducible. We will discuss these `forbidden configurations' and their geometric meaning. Some of the observations made for n=2 generalize to higher dimensions, however the cases for n > 2 present substantial challenges some of which we also hope to highlight in the talk.
  
  This is a joint work with members of Esakia seminar.

  ---

• Title: Logical aspects of algebra-valued models of set theory
  Speaker: Robert Paßmann (ILLC)
  Date: Wednesday, 19 December, 2018.
  [abstract]

  ---

  In this talk, we will be concerned with the propositional logics of algebra-valued models of set theory. First, we will recall the basic construction, and introduce the notions of loyalty and faithfulness as measures for how much information about the underlying algebra is preserved in the model. Moreover, we will see how these notions connect to the de Jongh property. In the second part, we will survey some of the results we obtained so far in this area (partly joint with Galeotti, and with Löwe and Tarafder).

  ---

• Title: Automata that Transform Infinite Words
  Speaker: Jörg Endrullis (Vrije Universiteit Amsterdam)
  Date: Wednesday, 5 December, 2018.
  [abstract]

  ---

  Finite automata can act as acceptors, to define (sets of) words, and as transformers, that transform words. While automata on infinite words play a central role in model checking and in the theory of automatic sequences, the transformational aspect of automata has hardly been studied for infinite words, also known as streams. There is a complete lack of theory to even answer simple concrete questions whether certain transformations are possible.
  
  This talk focuses on finite state transducers, a generalised form of Mealy machines, and the ensuing stream transformation (also called transduction). The transducibility relation on streams gives rise to a hierarchy of stream degrees, analogous to the well-known Turing degrees. We refer to this hierarchy as the Transducer degrees. In contrast to the Turing degrees, which have been studied extensively in the 60ths and 70ths, the Transducer degrees are largely unexplored territory. Despite finite state transducers being very simple and elegant devices, we hardly understand their power for transforming streams. In this talk, I will mention a few results that we have obtained in our initial exploration of the Transducer degrees, and several challenging open questions.

  ---

• Title: Beth definability and the Stone-Weierstrass Theorem
  Speaker: Luca Reggio (Czech Academy of Sciences)
  Date: Wednesday, 28 November, 2018.
  [abstract]

  ---

  Weierstrass approximation theorem states that any continuous real-valued function defined on a closed real interval can be uniformly approximated by polynomials. In 1937 Marshall Stone proved a vast generalisation of this result: nowadays known as the Stone-Weierstrass theorem, this is a fundamental result of functional analysis with far-reaching consequences. We show, through duality theory, that the Stone-Weierstrass theorem is a consequence of the Beth definability property of a certain logic, stating that implicit definability is equivalent to explicit definability.

  ---

• Title: What is the size of a formula? Basic size matters in the modal mu-calculus
  Speaker: Yde Venema (ILLC)
  Date: Wednesday, 21 November, 2018.
  [abstract]

  ---

  There are at least three ways to define the size of a formula in the modal mu-calculus: as its length (number of symbols), as its subformula size (number of subformulas) or as its closure-size (the size of its Fischer-Ladner closure set). While it is well-known that the subformula size of a formula can be exponentially smaller than its length, it came as a surprise to many when Bruse, Friedman & Lange showed that the closure size can be exponentially smaller then the subformula size. In the talk we discuss some size matters in the mu-calculus. The main point will be to argue that closure size is a more natural notion than subformula size. All definitions will be defined and explained.
  
  The talk reports on ongoing joint work with Clemens Kupke and Johannes Marti.

  ---

• Title: Etale groupoid convolution algebras
  Speaker: Benjamin Steinberg (CUNY)
  Date: Wednesday, 7 November, 2018.
  [abstract]

  ---

  In a 2010 paper I assigned a convolution algebra over any commutative base ring to an etale groupoid with totally disconnected unit space. These kinds of algebras include several families of well studied rings including group rings, commutative algebras generated by idempotents over fields, crossed products of the previous two examples, inverse semigroup rings and Leavitt path algebras. All these algebras are discrete analogues of well studied C*-algebras. It turns out that there are a number of analogies between algebraic properties of etale groupoid convolutions algebras and the C*-algebras of the groupoids (e.g., simplicity, Cartan pairs). In this talk we will survey examples, recent results and highlight the connection between sheaves over the etale groupoid and modules over the algebra.

  ---

• Title: Difference hierarchies and duality
  Speaker: Célia Borlido (Laboratoire J.A. Dieudonné)
  Date: Wednesday, 31 October, 2018.
  [abstract]

  ---

  The notion of a difference hierarchy, first introduced by Hausdorff, plays an important role in many areas of mathematics, logic and theoretical computer science such as in descriptive set theory, complexity theory, and in the theory of regular languages and automata. From a lattice theoretic point of view, the difference hierarchy over a bounded distributive lattice stratifies the Boolean algebra generated by it according to the minimum length of difference chains required to describe each Boolean element. While each Boolean element has a description by a finite difference chain, there is no canonical such writing in general. In this talk I will show that, relative to the filter completion, or equivalently, the lattice of closed upsets of the dual Priestley space, each Boolean element over the lattice has a canonical minimum length decomposition into a Hausdorff difference. As a corollary each Boolean element over a (co-)Heyting algebra has a canonical difference chain. With a further generalization of this result involving a directed family of adjunctions with meet-semilattices, we give an elementary proof of the fact that a regular language is given by a Boolean combination of purely universal sentences using arbitrary numerical predicates if and only if it is given by a Boolean combination of purely universal sentences using only regular numerical predicates.
  
  This is based on joint work with Gehrke, Krebs and Straubing.

  ---

• Title: Point-free geometries - foundations and systems
  Speaker: Rafał Gruszczyński (Nicolaus Copernicus University)
  Date: Wednesday, 10 October, 2018.
  [abstract]

  ---

  In a nutshell, point-free geometry is a branch of geometry in which the notion of point is absent from the inventory of basic concepts. Instead, regions or spatial bodies are assumed as primitives, next to an order relation on elements of the domain. In my talk I would like to discuss philosophical assumptions of point-free geometry and present two such systems: first, due to Polish mathematician Aleksander Śniatycki, based on the notion of half-plane, and second, due to Giangiacomo Gerla and the speaker, based on the notion of oval (a point-free counterpart of the notion of convex set). Slides.

  ---

• Title: Hyper-MacNeille completions of Heyting algebras
  Speaker: Frederik M. Lauridsen (ILLC)
  Date: Wednesday, 26 September, 2018.
  [abstract]

  ---

  Many intermediate logics for which no cut-free Gentzen-style sequent calculus is known may be captured by so-called hypersequent calculi without the cut-rule. For a large class of such hypersequent calculi a uniform algebraic proof of cut-admissibility may be given (Ciabattoni, Galatos, and Terui, 2017). The central construction of this proof gives rise to a new type of completion; the, so-called, hyper-MacNeille completion. We will briefly review the connection between the algebraic proof of cut-admissibility and MacNeille completions of Heyting algebras. We will then focus on describing the hyper-MacNeille completion of Heyting algebras. In particular, we will discuss the relationship between the MacNeille and the hyper-MacNeille completion.
  
  This is ongoing work with John Harding.

  ---

• Title: A perspective on non-commutative frame theory
  Speaker: Ganna Kudryavtseva (University of Ljubljana)
  Date: Wednesday, 12 September, 2018.
  [abstract]

  ---

  We discuss an extension of fundamental results of frame theory to a non-commutative setting where the role of locales is taken over by etale localic categories. These categories are put in a duality with complete and infinitely distributive restriction monoids (restriction monoids being a well-established class of non-regular generalizations of inverse monoids). As a special case this includes the duality between etale localic groupoids and pseudogroups (defined as complete and infinitely distributive inverse monoids). The relationship between categories and monoids is mediated by a class of quantales called restriction quantal frames. Projecting down to topological setting, we extend the classical adjunction between locales and topological spaces to an adjunction between etale localic categories and etale topological categories. As a consequence, we deduce a duality between distributive restriction semigroups and spectral etale topological categories. Our work unifies and upgrades the earlier work by Pedro Resende, and also by Mark V. Lawson and Daniel H. Lenz.
  
  The talk is based on a joint work with Mark V. Lawson.

  ---

• Title: How to extend de Vries duality to completely regular spaces
  Speaker: Guram Bezhanishvili (New Mexico State University)
  Date: Wednesday, 20 June, 2018.
  [abstract]

  ---

  De Vries duality yields a dual equivalence between the category of compact Hausdorff spaces and a category of complete Boolean algebras with a proximity relation on them, known as de Vries algebras. I will report on a recent joint work with Pat Morandi and Bruce Olberding on how to extend de Vries duality to completely regular spaces by replacing the category of de Vries algebras with certain extensions of de Vries algebras. This we do by first formulating a duality between compactifications and de Vries extensions, and then specializing to the extensions that correspond to Stone-Čech compactifications.

  ---

• Title: Fine-Grained Computational Complexity
  Speaker: Jouke Witteveen (ILLC)
  Date: Wednesday, 6 June, 2018.
  [abstract]

  ---

  Classically, complexity theory focuses on the hardest instances of a given length. A set is in P if there is a decision procedure for it that runs in polynomial time even on the most difficult-to-decide instances. Parameterized complexity theory, on the other hand, looks at the identification of easy instances. In this talk, we shall define parameterizations as independent objects and show that the class of parameterizations naturally forms a lattice. The parameterizations that put a given set in any of the standard parameterized complexity classes are filters in this lattice. From these insights, we conjecture a separation property for P.

  ---

• Title: W Types with Reductions
  Speaker: Andrew Swan (ILLC)
  Date: Wednesday, 23 May, 2018.
  [abstract]

  ---

  In type theory many inductively defined types can be formulated using the notion of W type. A basic example is the natural numbers. A natural number is either 0, or the successor Succ(n) of a natural number n we have already constructed. Moerdijk and Palmgren showed that when we interpret type theory in a locally cartesian closed category, W types can be characterised elegantly as the initial algebras for certain endofunctors (polynomial endofunctors). For example the natural numbers are the initial algebra for the endofunctor X → X + 1.
  
  I’ll show a generalisation called W types with reductions. For example, we can modify the natural numbers by adding the following reduction. We start off with the natural numbers as usual now, but later we identify each Succ(n) with its predecessor n (and so everything ends up identified with 0). We can use this idea to capture constructions in homotopical algebra where we modify a space by pasting on new cells and repeat this transfinitely. It is impossible to formulate this idea using initial algebras of endofunctors, so we move to pointed endofunctors, which are endofunctors P equipped with a natural transformation Id ⇒ P. Polynomial endofunctors can be generalised to *pointed* polynomial endofunctors, whose initial algebras are W types with reductions. In a large class of categories, including all predicative toposes, W types with reductions can always be constructed.

  ---

• Title: A simple propositional calculus for compact Hausdorff spaces
  Speaker: Nick Bezhanishvili (ILLC)
  Date: Wednesday, 9 May, 2018.
  [abstract]

  ---

  In recent years there has been a renewed interest in the modal logic community toward Boolean algebras equipped with binary relations. The study of such relations and their representation theory has a long history, and is related to the study of point-free geometry, point-free topology, and region based theory of space. Our primary examples of Boolean algebras with relations will be de Vries algebras, which are dual to compact Hausdorff spaces. Our main goal is to use the methods of modal logic and universal algebra to investigate the logical calculi of Boolean algebras with binary relations. This will lead, via de Vries duality, to simple propositional calculi for compact Hausdorff spaces, Stone spaces, etc.

  ---

• Title: Uniform interpolation via an open mapping theorem for Esakia spaces
  Speaker: Sam van Gool (ILLC)
  Date: Wednesday, 25 April, 2018.
  [abstract]

  ---

  We prove an open mapping theorem for the topological spaces dual to finitely presented Heyting algebras. This yields in particular a short, self-contained semantic proof of the uniform interpolation theorem for intuitionistic propositional logic, first proved by Pitts in 1992. Our proof is based on the methods of Ghilardi & Zawadowski. However, our proof does not require sheaves nor games, only basic duality theory for Heyting algebras.
  
  Reference:
  S. J. v. Gool and L. Reggio, An open mapping theorem for finitely copresented Esakia spaces, Topology and its Applications, vol. 240, 69-77 (2018).

  ---

• Title: Classical equivalents of intuitionistic implication
  Speakers: Esther Boerboom and Noor Heerkens (ILLC)
  Date: Wednesday, 11 April, 2018.
  [abstract]

  ---

  The objective of our study was to find suitable classical equivalents of intuitionistic implication. Since the formula p implies q has infinitely many classical equivalents in the full fragment of intuitionistic propositional logic, we restricted ourselves first of all to finite fragments. In order to find the most suitable candidates we examined important features of the candidates in these fragments, such as reflexivity and transitivity. Additionally we examined if the formulas are weaker or stronger than intuitionistic implication and whether they are exact.

  ---

• Title: Long-Term Values in Markov Decision Processes, (Co)Algebraically
  Speaker: Frank Feys (TU Delft)
  Date: Wednesday, 28 March, 2018.
  [abstract]

  ---

  Markov Decision Processes (MDPs) provide a formal framework for modeling sequential decision making, used in planning under uncertainty and reinforcement learning. In the classical theory, in an MDP the objective of the agent is to make choices such that the expected total rewards, the long-term values, are maximized; a rule that in each state dictates the agent which choice to make in order to achieve such an optimal outcome is called an optimal policy. A classical algorithm to find an optimal policy is Policy Iteration. In this talk, we show how MDPs can be studied from the categorical perspective of coalgebra and algebra. Probabilistic systems, similar to MDPs but without rewards, have been extensively studied, also coalgebraically, from the perspective of program semantics. We focus on the role of MDPs as models in optimal planning, where the reward structure is central. Our aim is twofold. First, to give a coinductive explanation of the correctness of Policy Iteration using a new proof principle, based on Banach’s Fixpoint Theorem, that we called Contraction Coinduction. Second, to show that the long-term value function of a policy with respect to discounted sums can be obtained via a generalized notion of corecursive algebra, designed to take boundedness into account.
  
  (This talk is based on joint work with Helle Hvid Hansen and Larry Moss.)

  ---

• Title: MacNeille transferability
  Speaker: Frederik M. Lauridsen (ILLC)
  Date: Wednesday, 21 March, 2018.
  [abstract]

  ---

  In 1966 Grätzer introduced the notion of transferability for finite lattices. A finite lattice L is transferable if whenever L has an embedding into the ideal completion of a lattice K, then L already has an embedding into K. In this talk we will introduce the analogous notion of MacNeille transferability, replacing the ideal completion with the MacNeille completion. We will pay particular attention to MacNeille transferability of finite distributive lattices with respect to the class of Heyting algebras. This will also allow us to find universal classes of Heyting algebras closed under MacNeille completions.
  
  This is joint work with G. Bezhanishvili, J. Harding, and J. Ilin.

  ---

• Title: Path categories
  Speaker: Benno van den Berg (ILLC)
  Date: Wednesday, 7 March, 2018.
  [abstract]

  ---

  The purpose of this talk is to introduce the notion of a path category (short for a category with path objects). Like other notions from homotopical algebra, such as a category of fibrant objects or a Quillen model structure, it provides a setting in which one can develop some homotopy theory. For a logician this type of category is interesting because it provides a setting in which many of the key concepts of homotopy type theory (HoTT) make sense. Indeed, path categories provide a syntax-free way of entering the world of HoTT, and familiarity with (the syntax of) type theory will not be assumed in this talk. Instead, I will concentrate on basic examples and results. (This is partly based on joint work with Ieke Moerdijk.)

  ---

• Title: Duality in Logic and Computer Science
  Speakers: Thijs Benjamins, Chase Ford, Kristoffer Kalavainen, Kyah Smaal, and Tatevik Yolyan (ILLC)
  Date: Wednesday, 31 January, 2018.
  [abstract]

  ---

  This special session of the A|C seminar will consist of five 25-minute presentations by the participants of the MoL January project taught by Sam van Gool. Each participant studied one recent article on duality theory and its applications in logic and computer science, and will give a presentation in which they summarize the main results of the paper and highlight points of particular interest. The following papers will be presented:

  • G. Bezhanishvili & N. Bezhanishvili, An Algebraic Approach to Canonical Formulas: Modal Case (2011), presented by Kyah Smaal;
  • T. Colcombet & D. Petrisan, Automata and Minimization (2017), presented by Thijs Benjamins;
  • S. Ghilardi, Continuity, Freeness and Filtrations (2010), presented by Tatevik Yolyan;
  • W. Holliday, Possibility Frames and Forcing for Modal Logic (2016), the section on duality theory, presented by Chase Ford;
  • T. Place & M. Zeitoun, Separating Regular Languages with First-order Logic (2016), presented by Kristoffer Kalavainen.

  
  There will be some time for discussion and Q&A after each presentation.

  ---

• Title: Stone-Priestley duality for MTL triples
  Speaker: Wesley Fussner (University of Denver)
  Date: Wednesday, 13 December, 2017.
  [abstract]

  ---

  Triples constructions date back to Chen and Grätzer’s 1969 decomposition theorem for Stone algebras: Each Stone algebra is characterized by the triple consisting of its lattice of complemented elements, its lattice of dense elements, and a homomorphism associating these structures. There is a long history of dual analogues of this construction, with Priestley (1972) providing a conceptually-similar treatment on duals in 1972 and Pogel also exploring dual triples in his 1998 thesis. At the same time, triples decompositions have been extended to account for richer algebraic structure. For example, Aguzzoli-Flaminio-Ugolini and Montagna-Ugolini have provided similar triples decompositions for large classes of monoidal t-norm (MTL) algebras, the algebraic semantics for monoidal t-norm based logic. Here we provide a duality theoretic perspective on these recent innovations, and see that the Stone-Priestley duality offers a clarifying framework that sheds light on these constructions
  
  This is joint work with Sara Ugolini.

  ---

• Title: Choice-free Stone duality
  Speaker: Nick Bezhanishvili (ILLC)
  Date: Wednesday, 17 April, 2017.
  [abstract]

  ---

  In this talk I will discuss a Stone-like topological duality for Boolean algebras avoiding the Prime Filter Theorem. This is joint work with Wes Holliday.

  ---

• Title: Ordering Free Groups
  Speaker: George Metcalfe (Universität Bern)
  Date: Wednesday, 26 April, 2017.
  [abstract]

  ---

  Ordering conditions for groups provide useful tools for the study of various relationships between group theory, universal algebra, topology, and logic. In this talk, I will describe a new algorithmic ordering condition for extending partial orders on groups to total orders. I will then show how this condition can be used to show that extending a finite subset of a free group to a total order corresponds to checking validity of a certain inequation in the class of totally ordered groups. As a direct consequence, we obtain a new proof that free groups are orderable.

  ---

• Title: Modal logics of the real line
  Speaker: Andrey Kudinov (HSE Moscow)
  Date: Wednesday, 14 December, 2016.
  [abstract]

  ---

  The real line is probably the most well known and well studied topological space. There are 6 different combinations of languages of this kind (two unimodal and four bimodal). The first modality in bimodal and the modality in unimodal languages we will interpret either using closure or derivation topological operators. For the second modality in bimodal settings we use universal or difference modalities. We will discuss logics of the real line that arise in all these languages.

  ---

• Title: Nominal Sets in Constructive Set Theorys
  Speaker: Andrew Swan (ILLC)
  Date: Wednesday, 9 November, 2016.
  [abstract]

  ---

  Nominal sets are simple structures originally used (by Gabbay and Pitts) to provide an abstract theory of the binding of variables. Since then, they have seen application in other areas, including the semantics of homotopy type theory. A basic notion in nominal sets is that of finite support. However, if we work in constructive set theory (roughly speaking, set theory avoiding the axiom of excluded middle), then finite sets can behave very differently to how they behave with classical logic. I will give a couple of examples to show how finite support in nominal sets can behave in constructive set theory. The results illustrate how the notion of finite differs in constructive set theory, and the proof illustrates some common techniques used in constructive set theory.

  ---

• Title: Some model theory for the modal μ-calculus
  Speaker: Yde Venema (ILLC)
  Date: Wednesday, 26 October, 2016.
  [abstract]

  ---

  We discuss a number of semantic properties pertaining to formulas of the modal μ-calculus. For each of these properties we provide a corresponding syntactic fragment, in the sense that a mu-calculus formula φ has the given property iff it is equivalent to a formula φ' in the corresponding fragment. Since this formula φ' will always be effectively obtainable from φ, as a corollary, for each of the properties under discussion, we prove that it is decidable in elementary time whether a given μ-calculus formula has the property or not. The properties that we study have in common that they all concern the dependency of the truth of the formula at stake, on a single proposition letter p. In each case the semantic condition on φ will be that φ, if true at a certain state in a certain model, will remain true if we restrict the set of states where p holds, to a special subset of the state space. Important examples include the properties of complete additivity and (Scott) continuity, where the special subsets are the singletons and the finite sets, respectively. Our proofs for these chacracterization results will be automata-theoretic in nature; we will see that the effectively defined maps on formulas are in fact induced by rather simple transformations on modal automata.

  ---

• Title: On generalized Van-Benthem-type characterizations
  Speaker: Grigory Olkhovikov (Ruhr-Universitaet Bochum, Institut fuer Philosophie II)
  Date: Wednesday, 28 September, 2016.
  [abstract]

  ---

  A guarded connective is a propositional formula built from monadic atoms preceded by a (possibly empty) prefix which consists of quantifiers guarded by chains of binary relations. An application of guarded connective to a tuple of monadic formulas is the result of respective substitution of these formulas for monadic atoms in the connective. A guarded fragment is a set of formulas containing monadic atoms and closed w.r.t. substitutions into a fixed finite set of guarded connectives. A guarded fragment is thus a generalized version of a set of standard translations of formulas of a given intensional propositional logic into first-order classical logic. We generalize bisimulations so as to get a model-theoretic characterization of a wide class of guarded fragments. Van Benthem Modal Characterization Theorem itself, as well as many analogous results obtained for other intensional propositional systems, come out as special cases of this generalized result.

  ---

• Title: Bitopology and four-valued logic
  Speaker: Tomáš Jakl (Charles University, Prague and University of Birmingham)
  Date: Wednesday, 4 May, 2016.
  [abstract]

  ---

  Bilattices and d-frames are two different kinds of structures with a four-valued interpretation. Whereas d-frames were introduced with their topological semantics in mind, the theory of bilattices has a closer connection with logic. In this talk we introduce a common generalisation of both structures and show that this not only still has a clear bitopological semantics, but that it also preserves most of the original bilattice logic. Moreover, we also obtain a new bitopological interpretation for the connectives of four-valued logic.

  ---

• Title: MV-algebras and the Pierce-Birkhoff conjecture
  Speaker: Serafina Lapenta (University of Salerno)
  Date: Wednesday, 20 April, 2016.
  [abstract]

  ---

  In this talk, we present a new class of MV-algebras, namely fMV-algebras. They are obtained when we endow an MV-algebra with a “ring-like” product and a scalar multiplication. We will discuss this class from an algebraic point of view, and characterize three relevant subclasses. The main motivation for this investigation is the long standing Pierce-Birkhoff conjecture, that aims to characterize the free lattice-ordered algebra (free lattice-ordered ring) as the algebra of piecewise polynomial functions with real coefficients (integer coefficients). The conjecture is standing since 1956: it has been solved for $n$ ≤ 2 by L. Mahé, while it is unsolved for $n$ >3. In this framework, the Pierce-Birkhoff conjecture became a normal form problem for the logic of fMV-algebras. Finally, we use the tensor product of MV-algebras – defined by D. Mundici – to provide a different perspective on the problem

  ---

• Title: Studying profinite semigroups via logic
  Speaker: Sam van Gool (CUNY City College and ILLC)
  Date: Wednesday, 30 March, 2016.
  [abstract]

  ---

  My aim in this talk is to introduce my current joint research project with Benjamin Steinberg on studying profinite semigroups via logic, and to indicate some tentative first results. A profinite semigroup is a Stone space equipped with a continuous semigroup operation. Through Stone duality, such semigroups correspond to certain Boolean algebras with operators. For this talk, the relevant instance of this phenomenon is the following. By a classical theorem of Schützenberger, the free profinite aperiodic semigroup over a finite set A is the dual space of the Boolean algebra of first-order definable sets of finite A-labelled linear orders (“A-words”). Therefore, elements of this semigroup can be viewed as elementary equivalence classes of models of the theory of finite A-words, in the sense of classical first-order model theory. We exploit this view of the free profinite aperiodic semigroup and use model-theoretic methods to prove both old and new things about it.

  ---

• Title: Investigations on Gödel’s incompleteness properties for guarded fragment and other decidable versions of FOL
  Speaker: Mohamed Khaled (Central European University, Budapest)
  Date: Wednesday, 16 March, 2016.
  [abstract]

  ---

  The guarded fragment of first order logic was introduced by Andréka, van Benthem and Németi in [4]. It is very closely connected to FOL with generalized semantics which was introduced by Henkin in [1] and Németi in [2]. These logics were considered by many logicians and it was shown that they have a number of desirable properties, e.g. decidability. These logics are considered to be the most important decidable versions of first order logic among the large number that have been introduced over the years. They have applications in various areas of computer science and were more recently shown to be relevant to description logics and to database theory. For a survey on generalized semantics see [6]. In this talk, we investigate Gödel’s incompleteness property for the above logics. We show that guarded fragment has neither Gödel’s nor weak Gödel’s incompleteness properties. The reason for that is the presence of the polyadic quantifiers. Indeed, we show that as a contrast, both the solo-quantifiers fragments of guarded fragment and FOL with generalized semantics have week Gödel’s incompleteness property because of the absence of the polyadic quantifiers. All the results to be mentioned in this talk are either algebraic or induced from some algebraic results. For instance, we prove that Henkin’s generalization of FOL with solo-quantifiers has weak Gödel’s incompleteness property by showing that free algebras of the classes of relativized cylindric algebras are not atomic. This gives an answer for a long-standing open problem posed, by Németi in 1985, in [2], [3] and [5].

  References
  1. L. Henkin (1950). The Completeness of Formal Systems. PhD thesis, Princenton University, Princeton, USA.
  2. I. Németi (1986). Free algebras and decidability in algebraic logic. Academic doctoral Dissertation, Hungarian Academy of Sciences, Budapest, Hungary.
  3. H. Andréka, J. D. Monk and I. Németi (1991). Algebraic Logic. North Holland, Amsterdam, Colloquia Mathematica Societatis János Bolyai, 54.
  4. H. Andréka, J. van Benthem and I. Németi (1998). Modal languages and bounded fragments of predicate logic. Journal of Philosophical Logic 27 (3), pp. 217-274.
  5. H. Andréka, M. Ferenczi and I. Németi (2013). Cylindric-like algebras and algebraic logic. Springer Verlag.
  6. H. Andréka, J. van Benthem, N. Bezhanishvili and I. Németi (2014). Changing a semantics: opportunism or courage? Springer Verlag.

  ---

• Title: Subminimal Logics of Negation
  Speaker: Almudena Colacito (ILLC)
  Date: Wednesday, 9 March, 2016.
  [abstract]

  ---

  Starting from the original formulation of Minimal Propositional Logic proposed by Johansson, we investigate some of its relevant sub- systems. The main focus is on the negation, defined as a primitive unary operator in the language. Each of the considered subsystems is axiomatized extending the positive fragment of intuitionistic logic by means of some axioms of negation. The basic logic of our setting is the one in which the negation operator has no properties at all, but the one of being a function. A Kripke semantics is developed for these logics, where the semantic clause for negation is determined by a persistent function N. The axioms defining extensions of the basic system enrich such a function with different properties (e.g., anti-monotonicity). We define a cut-free sequent calculus system and we work with it, proving some standard results for the considered logics. (This is a Master Thesis project supervised by Marta Bílková and Dick de Jongh)

  ---

• Title: Weak Subintuitionistic Logic
  Speaker: Fatemeh Shirmohammadzadeh Maleki (Shahid Beheshti University, Tehran and ILLC)
  Date: Wednesday, 24 February, 2016.
  [abstract]

  ---

  Subintuitionistic logics were studied by Corsi in 1987, who introduced a basic system F and by Restall in 1994, who defined a similar system SJ, both with a Kripke semantics. Basic logic, a much studied extension of F was already introduced by Visser in 1981. We will introduce a system WF, weaker than F and study it by means of a neighborhood semantics. (This is joint work with Dick de Jongh.)

  ---

• Title: Monadic second order logic as the model companion of temporal logic
  Speaker: Silvio Ghilardi (University of Milan)
  Date: Wednesday, 27 January, 2016.
  [abstract]

  ---

  In model theory, a model companion of a theory is a first-order description of the models where all solvable systems of equations and non-equations have solutions. We newly apply this model-theoretic framework in the realm of monadic second-order and temporal logic. (This is joint work with Sam van Gool)

  ---

• Title: Duality for Non-monotonic Consequence Relations and Antimatroids
  Speakers: Joahnnes Marti and Riccardo Pinosio (ILLC)
  Date: Wednesday, 2 December, 2015.
  [abstract]

  ---

  We present a duality between non-monotonic consequence relations over Boolean algebras and antimatroids over Stone spaces that extends the Stone duality. Non-monotonic consequence relations over Boolean algebras provide an abstract algebraic setting for the study of conditional logics and KLM-style non-monotonic consequence relations. Antimatroids over Stone spaces are a generalization of the usual order semantics for conditional logics and KLM-style systems. In the finite case antimatroids have already been studied as a combinatorial notion of convexity. The existing theory of antimatroids clarifies the constructions needed in completeness proofs for conditional logics and KLM-style systems with respect to the order semantics.

  ---

• Title: Some open problems concerning MSO for coalgebras
  Speaker: Sebastian Enqvist (ILLC)
  Date: Wednesday, 18 November, 2015.
  [abstract]

  ---

  I present some recent joint work with Fatemeh Seifan and Yde Venema, in which we introduced monadic second-order logic interpreted on coalgebras. Our main results provided conditions under which the coalgebraic modal mu-calculus for a given functor is the bisimulation invariant fragment of the corresponding MSO language. The focus of the talk will be on some open problems related to this topic.

  ---

• Title: Derivative and counting operators on topological spaces
  Speaker: Alberto Gatto (Imperial College London)
  Date: Wednesday, 18 November, 2015.
  [abstract]

  ---

  In the book 'Topological model theory' by Flum and Ziegler (1980), the authors introduced two first-order languages, L2 and its fragment Lt, to talk about topological spaces. Unlike L2, Lt enjoys several properties 'typical' of first-order logics such as compactness and Löwenheim Skolem Theorem; moreover Lt can express 'non-trivial' topological properties such as T0, T1, T2 and T3, and no language more expressive than Lt enjoys compactness and Löwenheim Skolem Theorem; finally, Lt is equivalent to the fragment of L2 that is invariant under changing basis.

  Languages to talk about topological spaces have been defined in modal terms as well. They have a long history (see e.g. the seminal paper 'The algebra of topology' by McKinsey and Tarski (1944)) and there is ongoing interest in the field. The main idea is to associate propositional variables to points of a topological space and give a topologically flavored semantics to modal operators.

  I will introduce the first-order languages L2 and Lt, and the modal language Lm with derivative and counting operators. I will then illustrate original work which establishes the equivalence between Lt and Lm over T3 spaces, and that the result fails over T2 spaces. I will then present a recent axiomatisation of the Lm theory of the classes of all T3, T2, and T1 spaces. I will then discuss the open problem of proving that Lm enriched with only finitely many other modal operators is still less expressive than Lt over T2 spaces, and present some partial results. Finally, I will conclude by illustrating possible directions of future work.

  ---

• Title: Coalgebraic many-valued logics
  Speaker: Marta Bílková (Charles University in Prague)
  Date: Wednesday, 4 November, 2015.
  [abstract]

  ---

  There are in general (at least) two ways how to obtain expressive modal logical languages for certain type of systems modelled as coalgebras: one is based on a single modal operator whose arity is given by the coalgebra functor and semantics given by relation lifting, the other is based on a logical connection (dual adjunction between semantics and syntax) producing, for a given coalgebra functor, all possible modalities (also known as predicate liftings). We discuss both of these approaches in the case valuations of formulas in coalgebraic models are many-valued, in particular taking values in a fixed residuated lattice or a quantale V. The possibilities we consider are: to stay in the category of sets, which in particular means, for the first approach, to prove a many-valued relation lifting theorem, and, for the second approach, to find an appropriate logical connection; or we can take the truth values seriously and change the base category to the enriched setting of V-categories. In the second case we are still able to provide a relation-lifting theorem. This is joint work with Matej Dostal.

  ---

• Title: The Wellfounded Parts of Final Coalgebras are Initial Algebras
  Speaker: Larry Moss (Indiana University Logic Program and Math department)
  Date: Wednesday, 8 July, 2015.
  [abstract]

  ---

  This talk is about the relation between initial algebras and final coalgebras. The prototypes of these results are about functors on sets. For many set functors F, the terminal coalgebra carries a complete metric which is the Cauchy completion of the metric induced on the initial algebra. In a different direction, the final coalgebra often has a CPO ordering which is the ideal completion of the ordering induced on the initial algebra. These basic results are due to Barr and Adamek. I'll review them, and then strike out on a different kind of relation between initial algebras and final coalgebras, one which I think clarifies the matter of relating initial algebras and final coalgebras. It is based on the categorical formulation of well-foundedness coming from Osius and then Taylor, and then further studied by Adamek, Milius, Sousa, and myself.

  ---

• Title: Stable canonical rules: bounded proofs, dichotomy property and admissible bases
  Speaker: Silvio Ghilardi (University of Milan)
  Date: Wednesday, 27 May, 2015.
  [abstract]

  ---

  During the talk I shall review recent joint work (with G. & N. Bezhanishvili, D. Gabelaia, M. Jibladze) concerning canonical multi-conclusion rules. In particular, bases for admissible rules in Int, K4, S4 are obtained by establishing a dichotomy property (in Jerabek's style).

  ---

• Title: Stone duality above dimension zero
  Speaker: Vincenzo Marra (University of Milan)
  Date: Wednesday, 27 April, 2015.
  [abstract]

  ---

  In 1969 Duskin proved that the dual of the category $\mathsf{KHaus}$ of compact Hausdorff spaces and continuous maps is monadic over Set [2, 5.15.3]. As a consequence, $\mathsf{KHaus^{op}}$ is a variety, that is, it must be axiomatisable by equations in an algebraic language that is possibly infinitary (=operations of infinite arity are allowed). By contrast, it can be shown that the endofunctor of the induced monad on $\mathsf{Set}$ does not preserve directed colimits, and this entails that finitary operations do not suffice to axiomatise $\mathsf{KHaus^{op}}$. (Banaschewski proved a considerably stronger negative result in [1].) However, Isbell exhibited in [3] finitely many finitary operations, along with exactly one operation of countably infinite arity, that do suffice. The problem of axiomatising by equations this variety has so far remained open. Using Chang's MV-algebras as a key tool, we provide an axiomatisation that, moreover, is finite. We introduce by this finite axiomatisation the infinitary variety of $\delta$-algebras, and we prove that it is dually equivalent to $\mathsf{KHaus}$. In a very precise sense, this extends Stone duality from Boolean spaces to compact Hausdorff spaces.

  References
  1. Bernhard Banaschewski, More on compact Hausdorff spaces and finitary duality, Canad. J. Math. 36 (1984), no. 6, 1113–1118.
  2. John Duskin,Variations on Beck's tripleability criterion, Reports of the Midwest Category Seminar, III, Springer, Berlin, 1969, pp. 74–129.
  3. John Isbell,Generating the algebraic theory of C(X), Algebra Universalis 15 (1982), no. 2, 153–155.

  ---

• Title: Modal logic of topology
  Speaker: Nick Bezhanishvili (ILLC) and Jan van Mill (KdVI)
  Date: Wednesday, 15 April, 2015.
  [abstract]

  ---

  In this talk we will discuss topological semantics of the well-known modal logic S4.3. This logic is sound and complete with respect to hereditarily extremally disconnected spaces. We will show how to construct a Tychonoff hereditarily extremally disconnected space X whose logic is S4.3.

  ---

• Title: Global caching for the alternation-free coalgebraic mu-calculus
  Speaker: Daniel Hausmann (Friedrich-Alexander University of Erlangen and Nurnberg)
  Date: Wednesday, 1 April, 2015.
  [abstract]

  ---

  The extension of basic coalgebraic modal logic by fixed point operators leads to the so-called coalgebraic mu-calculus [1], generalizing the well-known (propositional) mu-calculus. We consider the satisfiability problem of its alternation-free fragment; in order to decide the problem, we introduce a global caching algorithm (generalizing ideas from [2] and [3]) which employs a non-trivial process of so-called propagation, keeping track of least fixed point literals (referred to as eventualities) in order to ensure their eventual satisfaction. Our algorithm operates over subsets of the ordinary Fischer-Ladner closure of the target formula, however, the model construction in the accompanying completeness proof yields so-called focussed models of size at most n*(4^n) where n denotes the size of the satisfiable target formula - in particular improving upon previously known lower bounds on model size for e.g. ATL and the alternation-free mu-calculus (both 2^O(n*log n)).

  [1] C. Cirstea, C. Kupke, and D. Pattinson. EXPTIME tableaux for the coalgebraic μ-calculus.
  [2] M. Lange, C. Stirling. Focus games for satisfiability and completeness of temporal logic.
  [3] R. Goré, C. Kupke, D. Pattinson, L. Schröder. Global Caching for Coalgebraic Description Logics.
  

  ---

• Title: Dependency as question entailment
  Speaker: Ivano Ciardelli (ILLC, University of Amsterdam)
  Date: Wednesday, 18 March, 2015.
  [abstract]

  ---

  Over the past few years, a tight connection has emerged between logics of dependency and logics of questions. In this talk, I will show that this connection, far from being an accident, stems from a fundamental relation between dependency and questions: once we expand our view on logic by bringing questions into the picture, dependency emerges as a facet of the familiar notion of entailment, namely, entailment among questions. Besides providing a neat and insightful conceptual picture, this perspective yields the tools for a general and well-behaved logical account of dependencies.

  ---

• Title: Up-to techniques for bisimulations with silent moves
  Speaker: Daniela Petrişan (Raboud University, Nijmegen)
  Date: Wednesday, 4 March, 2015.
  [abstract]

  ---

  Bisimulation is used in concurrency theory as a proof method for establishing behavioural equivalence of processes. Up-to techniques can be seen as a means of optimizing proofs by coinduction. For example, to establish that two processes are equivalent one can exhibit a smaller relation, which is not a bisimulation, but rather a bisimulation up to a certain technique, say `up-to contextual closure'. However, the up-to technique at issue has to be sound, in the sense that any bisimulation up-to should be included in a bisimulation.

  In this talk I will present a general coalgebraic framework for proving the soundness of a wide range of up-to techniques for coinductive unary predicates, as well as for bisimulations. The specific up-to techniques are obtained using liftings of functors to appropriate categories of relations or predicates. In the case of bisimulations with silent moves the situation is more complex. Even for simple examples like CCS, the weak transition system gives rise to a lax bialgebra, rather than a bialgebra. In order to prove that up-to context is a sound technique we have to account for this laxness. The flexibility and modularity of our approach, due in part to using a fibrational setting, pays off: I will show how to obtain such results by changing the base category to preorders.

  This is joint work with Filippo Bonchi, Damien Pous and Jurriaan Rot.

  ---

• Title: Strong Completeness for Iteration-free Coalgebraic Dynamic Logics.
  Speaker: Helle Hansen (TU Delft)
  Date: Wednesday, 18 February, 2015.
  [abstract]

  ---

  We present a (co)algebraic treatment of iteration-free dynamic modal logics such as Propositional Dynamic Logic (PDL) and Game Logic (GL), both without star. The main observation is that the program/game constructs of PDL/GL arise from monad structure, and the axioms of these logics correspond to certain compatibilty requirements between the modalities and this monad structure. Our main contribution is a general soundness and strong completeness result for PDL-like logics for T-coalgebras where T is a monad and the ”program” constructs are given by sequential composition, test, and pointwise extensions of operations of T.

  ---

• Title: Residuated Basic Algebras
  Speaker: Minghui Ma (Southwest University)
  Date: Wednesday, 4 February, 2015.
  [abstract]

  ---

  Visser’s basic propositional logic BPL is the subintuitionistic logic which is characterized by the class of all transitive Kripke frames. Algebras for BPL are called basic algebras (BCA), which are distributive lattices with strict implication (called basic implication). The basic implication is a binary operator over a bounded distributive lattice satisfying certain conditions. It is not intuitionistic implication and hence not the right residual of conjunction.

  We introduce residuated basic algebras (RBA) which are defined as distributive lattice ordered residuated groupoids with additional axioms for the product operator. Those additional axioms correspond to some axioms for basic algebras. The variety RBA has the finite embeddability property, and so does the variety BCA.

  The logic RBL determined by the variety RBA can be shown as a conservative extension of BPL. There are several ways for proving the conservativity. One typical way is to apply the method of canonical extension. Another way is realized by Kripke semantics. Then we present a Gentzen-style sequent system for RBL, from which a sequent calculus for BPL is obtained if we drop the rules for additional operators. The sequent calculus for RBL enjoys cut elimination and the subformula property.

  One application is that we can use the sequent calculus for RBL and the conservativity to prove that the intuitionistic logic is embeddable into BPL. The embedding is defined on sequents. It follows that classical propositional logic is also embeddable into BPL. The above is my joint work with Zhe Lin (Institute of Logic and Cognition, Sun Yat-Sen University, Guangzhou, China).

  Our approach can be extended to the minimal subintuitionistic logic which is sound and complete with respect to the class of all Kripke frames. Moreover, we can define a syntax of propositional formulas such that we can get sequent calculi for extensions of the minimal subintuitionistic logics which enjoy the cut elimination and some other properties.

  Finally, I will comment on some embedding theorems for extension of the minimal subintuitionistic logics into classical modal logics.

  ---

• Title: Non-self-referential realizable frangments of modal and intuitionistic logics
  Speaker: Junhua Yu (Tsinghua University)
  Date: Wednesday, 21 January, 2015.
  [abstract]

  ---

  In the framework of justification logic, formula t:F generally means that term t is a justification of formula F. What interesting is that t may also occur in F, giving the formula t:F(t) a self-referential meaning, i.e., t is a justification of assertion F about t itself. This kind of self-referential formulas are necessary for justification logic to offer constructive semantics for many modal and intuitionistic logics via Artemov's realization. In this talk, we will see a research on fragments of modal and intuitionistic logics consists of theorems that are free of self-referentiality via realization.

  ---

• Title: Modal Logics for Presheaf Categories
  Speaker: Giovanni Cina (ILLC, University of Amsterdam)
  Date: Wednesday, 3 December, 2014.
  [abstract]

  ---

  In this paper we investigate a Modal Logic perspective on presheaf categories. We show that, for a given small category C, the category of presheaves over C can be embedded into the category of transition systems and functional bisimulations. We characterize the image of such embedding, defining what we call "typed transition systems arising from C", and prove that $Set^{C^{op}}$ is equivalent to the category of such typed transition systems. Coupled with the results inprevious papers, this equivalence suggests a procedure to turn a transition system into a deterministic one.

  Typed transition systems seem to offer a general relational semantics for typed processes. For this reason we propose a modal logic for typed transition systems arising from C, called $LTTS^{C}$. We prove that a first version of this logic, in which we add an infinitary rule, is sound and strongly complete for the class of these relational structures. Removing the infinitary rule we obtain a second system which is sound and weakly complete.

  ---

• Title: Completeness and Incompleteness in Nominal Kleene Algebra
  Speaker: Dexter Kozen (Cornell University)
  Date: Wednesday, 26 November, 2014.
  [abstract]

  ---

  Gabbay and Ciancia (2011) presented a nominal extension of Kleene algebra as a framework for trace semantics with dynamic allocation of resources, along with a semantics consisting of nominal languages. They also provided an axiomatization that captures the behavior of the scoping operator and its interaction with the Kleene algebra operators and proved soundness over nominal languages. In this work we show that the axioms are complete and describe the free language models. (Joint work with Konstantinos Mamouras and Alexandra Silva)

  ---

• Title: Polyhedra: from geometry to logic
  Speaker: Andrea Pedrini (University of Milan)
  Date: Wednesday, 5 November, 2014.
  [abstract]

  ---

  We study the Stone-Priestley dual space of the lattice of subpolyhedra of a compact polyhedron, with motivations coming from geometry, topology, ordered-algebra, and non-classical logic. We give a geometric representation of the spectral space of prime filters of the lattice of subpolyhedra of a compact polyhedron in terms of directions in the Euclidean space.

  From the perspective of algebraic logic, our contribution is a geometric investigation of lattices of prime theories in Lukasiewicz logic, possibly extended with real constants. We use the geometry of subpolyhedra to interpret provability in Lukasiewicz infinite-valued propositional logic into Intuitionistic propositional logic.

  ---

• Title: Exact Unification Type and Admissible rules
  Speaker: Leonardo Cabrer (University of Florence, Italy)
  Date: Wednesday, 29 October, 2014.
  [abstract]

  ---

  (Joint work with George Metcalfe)
  
  Motivated by the study of admissible rules, we introduce a new hierarchy of “exact" unification types. The main novelty of this hierarchy is the definition of order between unifiers: a unifier is said more exact than another unifier if all identities unified by the first are unified by the second. This simple change perspective, from syntactic to semantic to compare unifier has a large number of consequences. Exact unification has two important features: firstly, on each problem exact unification type is always smaller than or equal to the classical unification type, and secondly, there are equational theories having unification problems of classical unification type zero or infinite but whose exact unification type is finite. We will present examples of equational classes distinguishing the two hierarchies.
  
  We will also present a Ghilardi-style algebraic interpretation of this hierarchy that uses exact algebras rather than projective algebras.

  ---

• Title: PDL has Craig Interpolation since 1981
  Speaker: Malvin Gattinger (ILLC, University of Amsterdam)
  Date: Wednesday, 1 October, 2014.
  [abstract]

  ---

  Many people believe it to be an open question whether Propositional Dynamic Logic has Craig Interpolation. At least three proofs have been attempted and two of them published but all of them have also been claimed to be wrong, both more or less publicly.

  We recover a proof originally presented in a conference paper by Daniel Leivant (1981). The main idea and method here is still the same: Using the small model property we obtain a finitary sequent calculus for PDL. Furthermore, in proofs of star-formulas we find a repetitive pattern that allows us to construct interpolants. Our new presentation fixes many details and uses new results to simplify and clarify the proof. In particular we defend the argument against a criticism expressed by Marcus Kracht (1999), to show that the method indeed does not only apply to finitary variants of PDL but covers the whole logic.

  ---

• Title: Changing a Semantics: Opportunism, or Courage?
  Speaker: Johan van Benthem (ILLC, University of Amsterdam)
  Date: Wednesday, 17 September, 2014.
  [abstract]

  ---

  Henkin's models for higher-order logic are a widely used technique, but their status remains a matter of dispute. This talk reports on work with Hajnal Andréka, Nick Bezhanishvili & Ístvan Németi on the scope and justification of the method (ILLC Tech Report, to appear in M. Mazano et al. eds., "Henkin Book"). We will look at general models in terms of 'intended models', calibrating proof strength, algebraic representation, lowering complexity of core logics, and absoluteness. Our general aim: general perspectives on design of generalized models in logic, and links between these. We state a few new results, raise many open problems, and, in particular, explore the fate of generalized models on a less standard benchmark: fixed-point logics of computation.

  
  Lit. http://www.illc.uva.nl/Research/Publications/Reports/PP-2014-10.text.pdf

  ---

• Title: Axiomatizations of intermediate logics via the pseudo-complemented lattice reduct of Heyting algebras
  Speaker: Julia Ilin (ILLC, University of Amsterdam)
  Date: Wednesday, 11 June, 2014.
  [abstract]

  ---

  In this work we study Boolean algebras (BAs) with a binary relation satisfying some of Heyting algebras. The generalized canonical formulas encode the reduct structure of the Heyting algebra fully, but encode the behavior of the remaining structure only partially. Such canonical formulas were studied for the meet-implication reduct and the meet-join reduct of Heyting algbras. In both cases the corresponding canonical formulas are able to axiomatize all intermediate logics.

  In this talk, we will see that also the meet-join-negation reduct of Heyting algebras can be used in a similar way. Moreover, we investigate new classes of intermediate logics that the meet-join-negation reduct of Heyting algebras gives rise to.

  References
  [1] G. Bezhanishvili and N. Bezhanishvili. "An algebraic approach to canonical formulas: Intuitionistic case." In: Review of Symbolic Logic 2.3 (2009).
  [2]G. Bezhanishvili and N. Bezhanishvili. "Locally finite reducts of Heyting algebras and canonical formulas". To appear in Notre Dame Journal of Formal Logic. 2014.

  ---

• Title: Duality and canonicity for Boolean algebra with a relation
  Speaker: Sumit Sourabh (ILLC, University of Amsterdam)
  Date: Wednesday, 11 June, 2014.
  [abstract]

  ---

  In this work we study Boolean algebras (BAs) with a binary relation satisfying some properties. In particular, we introduce categories of BA with an operator relation (BAOR) which preserves finite joins in each coordinate and BA with a dual operator relation (BADOR) which preserves finite meets in each coordinate. The maps in these categories are Boolean homomorphisms preserving the relation. It turns out that well- known algebras such as de Vries algebras, contact algebras, lattice subordinations and Boolean proximity lattices are examples of objects in these categories. Using the char- acteristic map of the relations, we show that the category of BAOR (resp. BADOR) is isomorphic to category of BA with binary operators (resp. dual operators) into the 2-element BA 2. This allows us to import results from the theory of BAOs into our setting.

  We show that both finite BAOR and BADOR are dual to the category of Kripke frames with weak p-morphisms. In the infinite case, we show that both BAOR and BAOR are dual to the category of Stone spaces with closed binary relations and continuous maps. We also define canonical extensions of BAOR and BADOR, and show that Sahlqvist inequalities are canonical.

  ---

• Title: Adding the Supremum to Interpretability Logic
  Speaker: Paula Henk (ILLC, University of Amsterdam)
  Date: Wednesday, 28 May, 2014.
  [abstract]

  ---

  The relation of relative interpretability was first introduced and carefully studied by Tarski, Mostowski and Robinson. It can be seen as a definition of what it means for one theory to be at least as strong as another one. A collection of finite extensions of Peano Arithmetic (PA) that are equally strong in this sense is called a degree. The collection of all degrees (together with the relation of interpretability) is a distributive lattice.

  We are interested in using modal logic for investigating what is provable in PA about the lattice of its interpretability degrees. Part of the answer is provided by the interpretability logic ILM. However, the existence of the supremum in the lattice of interpretability degrees is not expressible in ILM. In order to eliminate this deficiency, we want to add to ILM a new modality. As it turns out, a unary modality is sufficient for this purpose. Furthermore, the dual of this unary modality satisfies the axioms of GL (provability logic), and can be therefore seen as a nonstandard provability predicate. The final part of the talk is concerned with the bimodal logic that results when adding to GL logic a unary modality whose intended meaning is such a nonstandard provability predicate.

  ---

• Title: Duality for Logic of Quantum Actions
  Speaker: Shengyang Zhong (ILLC, University of Amsterdam)
  Date: Wednesday, 28 May, 2014.
  [abstract]

  ---

  Traditionally, study in quantum logic and foundations of quantum theory focuses on the lattice structure of testable properties of quantum systems. The essence of this structure is captured in the definition of a Piron lattice [2]. In 2005, Baltag and Smets [1] proposed to organize states of a quantum system into a labelled transition system with tests of properties and unitary evolutions as transitions, whose non-classical nature is caused by the strangeness of quantum behaviour. Moreover, the results in [1] hint at a representation theorem for Piron lattices using this kind of labelled transition systems, called quantum dynamic frames.

  In this talk, I will present an extension of the work of Baltag and Smets into a duality result. I will define four categories, two of Piron lattices and two of quantum dynamic frames, and show two dualities of two pairs from them. This result establishes, on one direction of the duality, that quantum dynamic frames capture many essentials of quantum systems; on the other direction, it justify a more dynamic and intuitive way of thinking about Piron lattices. Moreover, this result is very useful for developing a logic of quantum actions.

  This talk is based on an on-going, joint paper of Jort Bergfeld, Kohei Kishida, Joshua Sack and me.

  References:
  [1] Baltag, Alexandru, and Sonja Smets, `Complete axiomatizations for quantum actions', International Journal of Theoretical Physics, 44 (2005), 12, 2267-2282.
  [2] Piron, Constantin, Foundations of Quantum Physics, W.A. Benjamin Inc., 1976.

  ---

• Title: Many-valued modal logic over residuated lattices via duality (joint work with Andrew Craig - University of Johannesburg)
  Speaker: Umberto Rivieccio (Delft University of Technology)
  Date: Wednesday, 14 May, 2014.
  [abstract]

  ---

  One of the latest and most challenging trends of research in non-classical logic is the attempt of enriching many-valued systems with modal operators. This allows one to formalize reasoning about vague or graded properties in those contexts (e.g., epistemic, normative, computational) that require the additional expressive power of modalities. This enterprise is thus potentially relevant not only to mathematical logic, but also to philosophical logic and computer science. A very general method for introducing the (least) many-valued modal logic over a given finite residuated lattice is described in [1]. The logic is defined semantically by means of Kripke models that are many-valued in two different ways: the valuations as well as the accessibility relation among possible worlds are both many-valued. Providing complete axiomatizations for such logics, even if we enrich the propositional language with a truth-constant for every element of the given lattice, is a non-trivial problem, which has been only partially solved to date. In this presentation I report on ongoing research in this direction, focusing on the contribution that the theory of natural dualities can give to this enterprise. I show in particular that duality allows us to adapt the method used in [1] to prove completeness with respect to local modal consequence, obtaining completeness for global consequence, too (a problem that, in full generality, was left open in in [1]). Besides this, our study is also a contribution towards a better general understanding of quasivarieties of (modal) residuated lattices from a topological perspective.

  References [1] F. Bou, F. Esteva, L. Godo, and R. Rodrìguez. On the minimum many-valued modal logic over a finite residuated lattice. Journal of Logic and Computation, 21(5):739-790, 2011.

  ---

• Title: Using Admissible Rules to Characterise Logics
  Speaker: Jeroen Goudsmit (Utrecht University)
  Date: Wednesday, 30 April, 2014.
  [abstract]

  ---

  The admissible rules of a logic are those rules under which the set of its theorems are closed. A most straightforward example is the rule A ∨ B / {A,B}, which is admissible precisely if the logic enjoys the disjunction property. Iemhoff (2001) showed that IPC can be characterised in terms of its admissible rules, by showing that it is the sole intermediate logic which admits a certain set of rules.

  We will present a similar characterisation for the Gabbay-de Jongh logics, also known as the logics of bounded branching. Our reasoning is based on the characterisation of IPC by Skura (1989), who presented a refutation system for IPC. In particular we show how one can inductively define the set of formulae that are non-derivable in the Gabbay-de Jongh logics. This talk is based on the work described in "Admissibility and Refutation: Some Characterisations of Intermediate Logics".

  ---

• Title: Uniform Interpolation for Coalgebraic Fixpoint Logic
  Speaker: Fatemeh Seifan (ILLC, University of Amsterdam)
  Date: Wednesday, 30 April, 2014.
  [abstract]

  ---

  In this talk we will use the connection between automata and logic to prove that a wide class of coalgebraic fixpoint logics enjoy the uniform interpolation.To this aim, first we generalize one of the central results in coalgebraic automata theory, namely closure under projection, which is known to hold for weak-pullback preserving functors, to a more general class of functors, i.e.; functors with quasi-functorial lax extensions. Then we will show that closure under projection implies definability of the bisimulation quantifier in the language of coalgebraic fixpoint logic, and finally we prove the uniform interpolation theorem.

  ---

• Title: Free algebras for Gödel-Löb provability logic
  Speaker: Sam van Gool (LIAFA, Université Paris-Diderot & Radboud Universiteit Nijmegen)
  Date: Wednesday, 16 April, 2014.
  [abstract]

  ---

  We give a construction of finitely generated free algebras for Gödel-Löb provability logic, GL. On the semantic side, this construction yields a notion of canonical graded model for GL and a syntactic definition of those normal forms which are consistent with GL. Our two main techniques are incremental constructions of free algebras and finite duality for partial modal algebras. In order to apply these techniques to GL, we use a rule-based formulation of the logic GL by Avron (which we simplify slightly), and the corresponding semantic characterization that was recently obtained by Bezhanishvili and Ghilardi.

  ---

• Title: Canonical rules for modal logic
  Speaker: Nick Bezhanishvili (ILLC, University of Amsterdam)
  Date: Thursday, 20 March, 2014.
  [abstract]

  ---

  In this talk I will discuss how to transform the method of implication-free canonical formulas for intuitionistic logic into the setting of modal logic.

  ---

• Title: From free algebras to proof bounds.
  Speaker: Silvio Ghilardi (University of Milano)
  Date: Thursday, 20 February, 2014.
  [abstract]

  ---

  (This is joint work with Nick Bezhanishvili). In the first part of our contribution, we review and compare existing constructions of finitely generated free algebras in modal logic focusing on step-by-step methods. We discuss the notions of step algebras and step frames arising from recent investigations, as well as the role played by finite duality. A step frame is a two-sorted structure which admits interpretations of modal formulae without nested modal operators.

  In the second part of the contribution, we exploit the potential of step frames for investigating proof-theoretic aspects. This includes developing a method which detects when a specific rule-based calculus Ax axiomatizing a given logic L has the so-called bounded proof property. This property is a kind of an analytic subformula property limiting the proof search space. We prove that every finite conservative step frame for Ax is a p-morphic image of a finite Kripke frame for L iff Ax has the bounded proof property and L has the finite model property. This result, combined with a "step version" of the classical correspondence theory, turns out to be quite powerful in applications. For simple logics such as K, K4, S4, etc, establishing basic matatheoretical properties becomes a completely automatic task (the related proof obbligations can be instantaneously discharged by current first-order provers). For more complicated logics, some ingenuity is still needed, however we were able to successfully apply our uniform method to Avron's cut-free system for GL and to Goré's cut-free system for S4.3.

  ---

• Title: Cut-elimination in circular proofs.
  Speaker: Jérôme Fortier (UQAM / AMU)
  Date: Thursday, 20 February, 2014.
  [abstract]

  ---

  Circularly-defined objects (e.g. inductive and coinductive types) live in the world of mu-bicomplete categories, where they arise from the following operations: finite products and coproducts, initial algebras, and final coalgebras. In the spirit of the Curry-Howard correspondence, Santocanale (2002) introduced a formal proof system for denoting arrows in such categories. The proofs in this system can be circular and yet sound. That means that you can prove some formulas from themselves, given that the cycles satisfy some condition analogous to an acceptance condition for parity games. However, the system was not full, which means that some arrows that must exist in any mu-bicomplete category could not be represented. We recently filled the system by adding the cut rule and modifying the condition on cycles. Not only does the new system remain sound and becomes full, but it also enjoys an automatic cut-elimination procedure that models the natural computation that arises from circular definitions. Some natural questions from this point are about expressiveness of such computations, which I will talk about.
  (This is joint work with Luigi Santocanale.)

  ---

• Title: Open maps, small maps and final coalgebras.
  Speaker: Benno van den Berg (ILLC, University of Amsterdam)
  Date: Thursday, 6 February, 2014.
  [abstract]

  ---

  In his book on non-well-founded sets Aczel proves a general final coalgebra theorem, showing that a wide class of endofunctors on the category of classes has a final coalgebra. I will discuss generalisations of this result to the setting of algebraic set theory and try to motivate why it is interesting to look at results at this level of generality.

  ---

• Title: A coalgebraic view of characteristic formulas in equational modal fixed point logics.
  Speaker: Sebastian Enqvist (ILLC, University of Amsterdam)
  Date: Wednesday, 22 January, 2014.
  [abstract]

  ---

  The literature on process theory and structural operational semantics abounds with various notions of behavioural equivalence and, more generally, simulation preorders. An important problem in this area from the point of view of logic is to find formulas that characterize states in finite transition systems with respect to these various relations. Recent work by Aceto et al. shows how such characterizing formulas in equational modal fixed point logics can be obtained for a wide variety of behavioural preorders using a single method. In this paper, we apply this basic insight from the work by Aceto et al. to Baltag's ``logics for coalgebraic simulation'' to obtain a general result that yields characteristic formulas for a wide range of relations, including strong bisimilarity, simulation, as well as bisimulation and simulation on Markov chains and more. We also provide conditions that allow us to automatically derive characteristic formulas in the language of predicate liftings for a given finitary functor. These latter languages have the advantage of staying closer to the more conventional syntax of languages like Hennessy-Milner logic.

  ---

• Title: Coalgebriac Announcement Logics
  Speaker: Facundo Carreiro (ILLC, University of Amsterdam)
  Date: Wednesday, 4 December, 2013.
  [abstract]

  ---

  In epistemic logic, dynamic operators describe the evolution of the knowledge of participating agents through communication, one of the most basic forms of communication being public announcement. Semantically, dynamic operators correspond to transformations of the underlying model. While metatheoretic results on dynamic epistemic logic so far are largely limited to the setting of Kripke models, there is evident interest in extending its scope to non-relational modalities capturing, e.g., uncertainty or collaboration. We develop a generic framework for non-relational dynamic logic by adding dynamic operators to coalgebraic logic. We discuss a range of examples and establish basic results including bisimulation invariance, complexity, and a small model property.
  
  The talk is based on the paper published in ICALP 2013, available at: http://glyc.dc.uba.ar/facu/papers/coalg-announcements.pdf.
  

  ---

• Title: An algebraic approach to cut-elimination for substructural logics.
  Speaker: Sumit Sourabh (ILLC, University of Amsterdam)
  Date: Wednesday, 20 November, 2013.
  [abstract]

  ---

  Algebraic proof theory combines algebraic and proof theoretical techniques to prove results about substructural logics. In [1], the authors give an algebraic proof of cut-elimination theorem for substructural logics using quasi-completions of FL-algebras. It is also shown that quasi-completions of FL-algebras are isomorphic to their MacNeille completions. Another recent work [2], explores the connections between admissibility of cut rule on adding a structural rule to the calculus and preservation of the structural rule under MacNeille completion. In this talk, I will give an introduction to algebraic proof theory followed by an overview of preservation of equations under completion of algebras.
  
  [1] F. Belardinelli, P. Jipsen and H. Ono, Algebraic aspects of cut elimination, Studia Logica 77(2) (2004), 209-240.
  
  [2] A. Ciabattoni , N. Galatos and K. Terui, Algebraic proof theory for substructural logics: Cut-elimination and completions, Annals of Pure and Applied Logic, Volume 163, Issue 3, March 2012, pp. 266-290.
  

  ---

• Title: Terminal Sequences and Their Coalgebras.
  Speaker: Johannes Marti (ILLC, University of Amsterdam)
  Date: Wednesday, 31 October, 2013.
  [abstract]

  ---

  This talk starts with a review of the terminal sequence construction for an endofunctor. In nice cases the terminal sequence converges and yields the cofree coalgebras in the category of coalgebras for the endofunctor. These cofree coalgebras form a comonad whose category of Eilenberg-Moore coalgebras is isomorphic to the category of coalgebras for the original endofunctor. What is good about this comonads is that, under reasonable additional assumptions, we can use coequations to define subcomonads whose categories of Eilenberg-Moore coalgebras are covarieties of coalgebras.

  In not so nice cases the terminal sequence does not converge and we do not obtain a comonad to specify covarieties. This not so nice cases include the powerset functor whose coalgebras are Kripke frames where modally definable classes of frames could be studied as covarieties.

  I show that even in the not so nice cases we can define a category of coalgebras for a terminal sequence that plays an analogous role as the category of Eilenberg-Moore coalgebras for a comonad. Moreover, under the same additional assumptions as for comonads, the covarieties are categories of coalgebras for subsequences obtained from coequations.

  Comonads and terminal sequences are both colax functors from a small 2-category to the 2-category of categories. Interestingly, there is a notion of coalgebra for any such colax functor. I give examples of relevant categories of coalgebras that need this full generality.

  ---

• Title: Two isomorphism criteria for directed colimits.
  Speaker: Luca Spada (ILLC, Amsterdam and University of Salerno)
  Date: Wednesday, 9 October, 2013.
  [abstract]

  ---

  Using the general notions of finite presentable and finitely generated object introduced by Gabriel and Ulmer in 1971, we prove that, in any category, two sequences of finitely presentable objects and morphisms (or two sequences of finitely generated objects and monomorphisms) have isomorphic colimits (=direct limits) if, and only if, they are confluent. The latter means that the two given sequences can be connected by a back-and-forth sequence of morphisms that is cofinal on each side, and commutes with the sequences at each finite stage. We illustrate the criterion by applying the abstract results to varieties (=equationally definable classes) of algebras, and mentioning applications to non-equational examples.

  ---

• Title: A non-commutative Priestly duality
  Speaker: Sam van Gool (Radbound University, Nijmegen)
  Date: Wednesday February 13, 2013
  [abstract]

  ---

  In this talk on our recent paper*, I will describe a new Priestley-style duality for skew distributive lattices. Since its introduction in Stone's seminal papers from 1936 and 1937, duality theory has been important in the study of propositional logics beyond the classical, such as intuitionistic, modal, and substructural logics. It provides the mathematical framework for studying the intimate link between the syntax and semantics of a logic.

  The results that I describe in this talk form a generalization of duality theory beyond the commutative case. This opens the door to applications of duality theory to logical systems in which the basic operations of conjunction and disjunction are no longer assumed to be commutative. Such systems are of interest because of their possible relevance to both quantum logic and dynamic epistemic logic.

  *preprint available on http://arxiv.org/pdf/1206.5848

  ---

• Title: Bilattices with modal operators
  Speaker: Speaker: Umberto Rivieccio (University of Birmingham)
  Date: Wednesday May 30, 2012
  [abstract]

  ---

  Some authors have recently started to consider modal expansions of the well-known Belnap four-valued logic, either with implication (S. Odintsov, H. Wansing et al.) or without it (G. Priest). Given that some bilattice logics are four-valued (conservative) expansions of the Belnap logic, we may wonder whether it makes sense to consider modal expansions of bilattice logics and their algebraic counterpart, which would be bilattices with modal operators. I will present a few ideas on how this can be done.

  ---

• Title: Topological- and Neighborhood-Sheaf Semantics for First-Order Modal Logic
  Speaker: Kohei Kishida (ILLC, Amsterdam)
  Date: Wednesday May 23, 2012
  [abstract]

  ---

  This talk extends Tarski's classical topological semantics for propositional modal logic to first-order modal logic, with respect to the following two aspects: (i) It takes a sheaf over a topological space, and shows that such structures (or the category of them) model first-order modal logic by equipping points of the space with domains of individuals. (ii) It is also shown how topological semantics extends to the more general case of neighborhood semantics, at the level of sheaf semantics. These extensions provide semantics for the simple unions of first-order logic with S4 modal logic and with more general modal logics. Corresponding to the point-set and algebraic formulations of Tarski's topological semantics, the semantics of this paper will be presented in both point-set and topos-theoretic formulations.

  ---

The A|C-seminar, under the Institute for Logic, Language and Computing (ILLC), located at Science Park 107 1098 XG Amsterdam, is responsible for the processing of personal data as shown in this privacy statement.

The A|C seminar no longer processes personal data via this website (http://events.illc.uva.nl/alg-coalg/), because it is no longer possible to leave personal data behind. We also do not use social media plugins.

The A|C seminar does not take decisions based on automated processing related to this website on matters that can have (significant) consequences for individuals, e.g. decisions taken by computer programs or systems, without involving a person (for example an organiser of the A|C-seminar).

The A|C-seminar does not use cookies or similar techniques on this website.