 Title: : Fixedpoint elimination in the Intuitionistic Propositional Calculus (Slides)
Speaker: Luigi Santocanale (AixMarseille Université)
Date: Wednesday, 26 May, 2021.
Time: 16:00 (CEST)
Location: Online (Zoom Meeting ID 92250640302)
[abstract]
That fixedpoints can be eliminated from mucalculus based on the Intuitionistic Propositional Calculus (muIPC) is a consequence of Ruitenburg theorem. In this talk I'll present the elimination procedure of fixed points in the muIPC devised by Ghilardi, Gouveia, and myself, which also also yields a decision procedure for muIPC 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 mucalculi, 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 fixedpoints.
 Title: Distributive latticeordered 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 92250640302)
[abstract]
Latticeordered groups (lgroups) form natural algebraic structures and have been studied extensively. Holland's embedding theorem shows that every lgroup can be embedded in the order automorphisms of a chain, while lgroups play an important role in the algebraic semantics of substructural logics (for example in relation to abelian relevance logic, MValgebras, BLalgebras, cancellative residuated lattices). We study the subreducts of lgroups where the inverse operation is dropped; the resulting structures are distributive latticeordered 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 inversefree equation is valid in all lgroups 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 lgroup equation is equivalent to an inversefree equation, a fact that allows the reduction of the full equational theory of lgroups to that of DLMs. This further leads to a hybrid sequent/hypersequent calculus for lgroups, 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 orderautomorphisms 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 92250640302)
[abstract]
The classical HennessyMilner theorem says that two states of an imagefinite 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 mucalculus
Speaker: David FernándezDuque (Gent University)
Date: Wednesday, 21 April, 2021.
Time: 16:00 (CEST)
Location: Online (Zoom Meeting ID 92250640302)
[abstract]
Joint work with Alexandru Baltag and Nick Bezhanishvili
The language of the unimodal mucalculus 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 TDspaces, but the generalization to arbitrary topological spaces poses some challenges. In this talk we will show that the topological mucalculus 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 (ENSLyon)
Date: Wednesday, 14 April, 2021.
Time: 16:00 (CEST)
Location: Online (Zoom Meeting ID 92250640302)
[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 CUTelimination theorem greatly reduces the search space. In this talk I will present some recent developments in this direction.
 Title: Measuretheoretic semantics for quantitative lineartime logics
Speaker: Corina Cirstea (University of Southampton)
Date: Wednesday, 31 March, 2021.
Time: 16:00 (CEST)
Location: Online (Zoom Meeting ID 92250640302)
[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 automatatheoretic semantics, a measuretheoretic 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 prooftheoretic 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 92250640302)
[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: welldeveloped 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 cutelimination 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 92250640302)
[abstract]
We are going to examine a sequent calculus for the Grzegorczyk modal logic Grz with nonwellfounded proofs and discuss the cutelimination theorem for it. In order to avoid nested coinductive and inductive reasoning in the proof of cutelimination, we adopt an approach from denotational semantics of computer languages, where program types are interpreted as ultrametric spaces and fixedpoint combinators are encoded using fixedpoint theorems. We consider the set of nonwellfounded proofs of Grz and various sets of operations acting on these proofs as ultrametric spaces and define the cutelimination operator following the lines of the PriessCrampe fixedpoint theorem. If time permits, we will also discuss how this approach to cutelimination 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 92250640302)
[abstract]
In the topological semantics for modal logic, S4 is wellknown
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
denseinitself 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
denseinitself 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 92250640302)
[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 socalled 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 QuasiEquational 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 92250640302)
[abstract]
In [2], my PhD supervisors (Pieter Hofstra and Philip Scott) and I studied the new topostheoretic phenomenon of isotropy (as introduced in [1]) in the context of singlesorted 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 (multisorted) quasiequational 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 quasiequational 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 setvalued 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, 660709, 2012.
[2] P. Hofstra, J. Parker, P.J. Scott. Isotropy of algebraic theories. Electronic Notes in Theoretical Computer Science 341, 201217, 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 92250640302)
[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 highercategorical 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 92250640302)
[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) SecondOrder Theory of Infinite Trees
Speaker: Colin Riba (ENS de Lyon)
Date: Wednesday, 21 October, 2020.
Time: 16:00 (CEST)
Location: Online (Zoom Meeting ID 92250640302)
[abstract]
We present a complete axiomatization of Monadic SecondOrder Logic (MSO) over infinite trees. By a complete axiomatization we mean a complete deduction system with a polynomialtime 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 secondorder logic seen as twosorted firstorder 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) SecondOrder 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 92250640302)
[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" (predicateguarded) versions. This makes GKAT especially suited to reason about flow control in imperative programs. In contrast with KAT, where the equivalence problem is PSPACEcomplete, 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 Salomaastyle axiomatization, both of which require us to develop a coalgebraic theory of GKAT.
AC seminar in 2019/2020
 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 92250640302)
[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 coalgebralike 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 Setcoalgebras. Finally, we investigate a categorical notion of completeness, obtain a general completeness result, and instantiate this to our example.
 Title: ChoiceFree 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 92250640302)
[abstract]
The aim of this talk is to outline our ongoing research in which we are developing a choicefree 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, UVOspaces). Our techniques combine the choicefree spectral space approach to the topological duality theory of Boolean algebras developed by Bezhanishvili and Holliday with the choicedependent 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 UVOspace concepts. Lastly, we discuss how our duality relates to other dualities and what applications we hope to explore.
 Title: From choicefree Stone duality to choicefree 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 92250640302)
[abstract]
In a recent paper, "Choicefree Stone duality" (JSL, March 2020), Nick Bezhanishvili and I developed a choicefree duality theory for Boolean algebras using special spectral spaces, called upper Vietoris spaces (UVspaces). In this talk, I will cover the basics of this duality and explain how it leads to “possibility semantics” for classical firstorder logic. While the completeness theorem for firstorder logic for uncountable languages with respect to traditional Tarskian models requires a nonconstructive choice principle unprovable in ZF set theory, I will sketch a choicefree proof of the completeness theorem for firstorder logic for arbitrary languages with respect to possibility models. This result raises the prospect of a program of “choicefree 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 92250640302)
[abstract]
In this talk, we broach an algebraic canonicity theorem for normal LElogics of arbitrary signature in the generalized setting of slanted algebras, i.e. lattices expansions in which the nonlattice operations map tuples of elements of the given lattice to closed or open elements of its canonical extension. Interestingly, the syntactic shape of LEinequalities which guarantees canonicity in this generalized setting turns out to coincide with the shape of analytic inductive inequalities, which guarantees LEinequalities 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 nonsymmetry 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 MValgebras (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 MValgebras.
 Title: Are locally finite MValgebras 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 MValgebras equivalent to an equational class? We prove:
 The category of locally finite MValgebras is not equivalent to any finitary variety of algebras. More is true: the category of locally finite MValgebras is not equivalent to any finitelysorted finitary quasivariety of algebras.
 The category of locally finite MValgebras is equivalent to a variety of infinitary algebras (with operations of countable arity).
 The category of locally finite MValgebras is equivalent to a countablysorted variety of finitary algebras.
Our proofs rest upon the duality between locally finite MValgebras and the category of multisets by Cignoli, Dubuc and Mundici, and categorical characterisations of varieties and quasivarieties proved by Lawvere, Duskin and many others.
 Title: Describable Nuclea, Negative Translations and Extension Stability
Speaker: Tadeusz Litak (FAU ErlangenNürnberg)
Date: Tuesday, 12 May, 2020.
Time: 14:00 (CEST)
Location: Online (see the TULIPS webpage note: preregistration 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 Kripkestyle or neighourhoodstyle 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 pointfree topologies (latticecomplete 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. LuceroBryan, and J. van Mill
 Title: Circular proofs for the hybrid mucalculus
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 cutfree sequent calculus for the modal mucalculus. 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 mucalculus, extending the modal mucalculus 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 mucalculus that lack the tree model property, like guarded fixpoint logic and twoway mucalculus. 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 onestep 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 onestep coalgebras that are dual to the onestep algebras
approximating the free algebra. The advantage of this approach is that
in many interesting cases the points of onestep coalgebras are finite
treelike objects and the unification problem becomes a combinatorial
problem about these trees.
We consider three instances of this characterization:
 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.
 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.
 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 multiagent 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 multiagent 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 ProofTheoretic Semantics
Speaker: Gabriele Pulcini (ILLC)
Date: Wednesday, 4 March, 2020.
Time: 16:00
Location: Room F1.15, Science Park 107, Amsterdam.
[abstract]
Two proofsystems P and P* are said to be complementary
when one proves exactly the nontheorems 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 cutelimination
algorithm. In particular, two facts will be highlighted:
1) for any given provable sequent, complementary
cutelimination 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 multivaluedness and prooftheoretic semantics for
classical logic.
 Title: One step to admissibility in intuitionistic GödelLö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ödelLö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 HigherOrder 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 nonprobabilistic programming successfully by
using coinductive types and coiteration. Vákár et al. (POPL'19)
introduced semantics for a higherorder probabilistic programming
language with full recursion in types and programs based on quasiBorel
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 socalled coinductive types and programmed via
socalled guarded recursion, which ensures that the programs describing
random walks etc. are terminating. Central to guarded recursion is the
socalled later modality, which allows one to express that the
computation of an element of a type is delayed. This allows one to use
typechecking 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 pointfree theories of space is to deliver a plausible definition of points, entities which are assumed as primitives in pointbased 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 ongoing 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 NonClassical 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 2category. 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 MartinLö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
socalled Spatial Logics. We present a topologybased approach to model checking
for spatial and spatiotemporal 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 stateoftheart 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 stateoftheart accuracy, competing with bestinclass
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.
AC seminar in 2018/2019
 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 PDLstyle 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 cutfree 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 validitypreserving 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 metaproperties. 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 Oadjoints.
 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 statebased reasoning. Its versatility is witnessed in its robustness when extended by nonlocal 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 reinterpreting 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 longterm behavior of transition systems. These are discrete, possibly nondeterministic 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 longterm 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 nonframes 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 algebravalued 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
algebravalued 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 wellknown 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 StoneWeierstrass Theorem
Speaker: Luca Reggio (Czech Academy of Sciences)
Date: Wednesday, 28 November, 2018.
[abstract]
Weierstrass approximation theorem states that any continuous realvalued 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 StoneWeierstrass theorem, this is a fundamental result of functional analysis with farreaching consequences. We show, through duality theory, that the StoneWeierstrass 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 mucalculus
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 mucalculus:
as its length (number of symbols), as its subformula size (number of subformulas) or as
its closuresize (the size of its FischerLadner closure set). While it is wellknown 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 mucalculus. 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 meetsemilattices, 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: Pointfree geometries  foundations and systems
Speaker: Rafał Gruszczyński (Nicolaus Copernicus University)
Date: Wednesday, 10 October, 2018.
[abstract]
In a nutshell, pointfree 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 pointfree
geometry and present two such systems: first, due to Polish
mathematician Aleksander Śniatycki, based on the notion of halfplane,
and second, due to Giangiacomo Gerla and the speaker, based on the
notion of oval (a pointfree counterpart of the notion of convex set). Slides.
 Title: HyperMacNeille completions of Heyting algebras
Speaker: Frederik M. Lauridsen (ILLC)
Date: Wednesday, 26 September, 2018.
[abstract]
Many intermediate logics for which no cutfree Gentzenstyle sequent calculus is known may be captured by socalled hypersequent calculi without the cutrule. For a large class of such hypersequent calculi a uniform algebraic proof of cutadmissibility may be given (Ciabattoni, Galatos, and Terui, 2017). The central construction of this proof gives rise to a new type of completion; the, socalled, hyperMacNeille completion.
We will briefly review the connection between the algebraic proof of cutadmissibility and MacNeille completions of Heyting algebras. We will then focus on describing the hyperMacNeille completion of Heyting algebras. In particular, we will discuss the relationship between the MacNeille and the hyperMacNeille completion.
This is ongoing work with John Harding.
 Title: A perspective on noncommutative 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 noncommutative 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 wellestablished class of nonregular 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.
AC seminar in 2017/2018
 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: FineGrained 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 difficulttodecide
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 pointfree geometry, pointfree 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, selfcontained 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, 6977 (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: LongTerm 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 longterm 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 longterm 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 syntaxfree 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 AC seminar will consist of five 25minute 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 Firstorder Logic (2016), presented by Kristoffer Kalavainen.
There will be some time for discussion and Q&A after each presentation.
 Title: StonePriestley 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 conceptuallysimilar 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, AguzzoliFlaminioUgolini and MontagnaUgolini have provided similar triples decompositions for large classes of monoidal tnorm (MTL) algebras, the algebraic semantics for monoidal tnorm based logic. Here we provide a duality theoretic perspective on these recent innovations, and see that the StonePriestley duality offers a clarifying framework that sheds light on these constructions
This is joint work with Sara Ugolini.
AC seminar in 2016/2017
 Title: Choicefree Stone duality
Speaker: Nick Bezhanishvili (ILLC)
Date: Wednesday, 17 April, 2017.
[abstract]
In this talk I will discuss a Stonelike 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 mucalculus 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 automatatheoretic 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 VanBenthemtype characterizations
Speaker: Grigory Olkhovikov (RuhrUniversitaet 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 firstorder
classical logic.
We generalize bisimulations so as to get a modeltheoretic
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.
AC seminar in 2015/2016
 Title: Bitopology and fourvalued logic
Speaker: Tomáš Jakl (Charles University, Prague and University of Birmingham)
Date: Wednesday, 4 May, 2016.
[abstract]
Bilattices and dframes are two different kinds of structures with a fourvalued interpretation. Whereas dframes 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 fourvalued logic.
 Title: MValgebras and the PierceBirkhoff conjecture
Speaker: Serafina Lapenta (University of Salerno)
Date: Wednesday, 20 April, 2016.
[abstract]
In this talk, we present a new class of MValgebras, namely fMValgebras. They are obtained when we endow an MValgebra with a “ringlike” 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 PierceBirkhoff conjecture, that aims to characterize the free latticeordered algebra (free latticeordered 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 PierceBirkhoff conjecture became a normal form problem for the logic of fMValgebras. Finally, we use the tensor product of MValgebras – 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 firstorder definable sets of finite Alabelled linear orders (“Awords”).
Therefore, elements of this semigroup can be viewed as elementary equivalence classes of models of
the theory of finite Awords, in the sense of classical firstorder model theory. We exploit this
view of the free profinite aperiodic semigroup and use modeltheoretic 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 soloquantifiers 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 soloquantifiers 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 longstanding 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. 217274.
5. H. Andréka, M. Ferenczi and I. Németi (2013). Cylindriclike 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., antimonotonicity). We
define a cutfree 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 firstorder
description of the models where all solvable systems of equations
and nonequations have solutions. We newly apply this modeltheoretic
framework in the realm of monadic secondorder and
temporal logic.
(This is joint work with Sam van Gool)
 Title: Duality for Nonmonotonic Consequence Relations and Antimatroids
Speakers: Joahnnes Marti and Riccardo Pinosio (ILLC)
Date: Wednesday, 2 December, 2015.
[abstract]
We present a duality between nonmonotonic consequence relations over Boolean algebras
and antimatroids over Stone spaces that extends the Stone duality. Nonmonotonic consequence relations over Boolean algebras provide an abstract
algebraic setting for the study of conditional logics and KLMstyle nonmonotonic consequence relations.
Antimatroids over Stone spaces are a generalization of the usual order semantics for
conditional logics and KLMstyle 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 KLMstyle 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 secondorder logic
interpreted on coalgebras. Our main results provided conditions under which the coalgebraic modal mucalculus 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 firstorder languages,
L2 and its fragment Lt, to talk about topological spaces. Unlike L2, Lt enjoys several properties 'typical' of firstorder
logics such as compactness and Löwenheim Skolem Theorem; moreover Lt can express 'nontrivial' 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 firstorder 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 manyvalued 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 manyvalued, 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 manyvalued 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 Vcategories. In the second case we are still able to provide a relationlifting theorem.
This is joint work with Matej Dostal.
AC seminar in 2014/2015
 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 wellfoundedness 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 multiconclusion 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
MValgebras 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 wellknown 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 alternationfree coalgebraic mucalculus
Speaker: Daniel Hausmann (FriedrichAlexander 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 socalled coalgebraic mucalculus [1], generalizing the
wellknown (propositional) mucalculus. We consider the satisfiability
problem of its alternationfree fragment; in order to decide the
problem, we introduce a global caching algorithm (generalizing ideas
from [2] and [3]) which employs a nontrivial process of socalled
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 FischerLadner closure
of the target formula, however, the model construction in the
accompanying completeness proof yields socalled 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 alternationfree mucalculus (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 wellbehaved logical account of dependencies.
 Title: Upto 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. Upto 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 `upto contextual closure'. However, the upto technique at issue has to be sound, in the sense that any bisimulation upto 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 upto techniques for coinductive unary predicates, as well as for bisimulations. The specific upto 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 upto 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 Iterationfree Coalgebraic Dynamic Logics.
Speaker: Helle Hansen (TU Delft)
Date: Wednesday, 18 February, 2015.
[abstract]
We present a (co)algebraic treatment of iterationfree 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 PDLlike
logics for Tcoalgebras 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 Gentzenstyle 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
YatSen 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: Nonselfreferential 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 selfreferential meaning, i.e., t is a justification of assertion F about t itself. This kind of selfreferential 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 selfreferentiality 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 StonePriestley dual space of the lattice of subpolyhedra of a compact polyhedron, with motivations coming from geometry, topology, orderedalgebra, and nonclassical 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 infinitevalued 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 Ghilardistyle 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 starformulas 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 higherorder 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: fixedpoint logics of computation.
Lit. http://www.illc.uva.nl/Research/Publications/Reports/PP201410.text.pdf
AC seminar in 2013/2014
 Title: Axiomatizations of intermediate logics via the pseudocomplemented 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 meetimplication reduct and the meetjoin 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 meetjoinnegation reduct of Heyting algebras can be used in a
similar way. Moreover, we investigate new classes of intermediate logics that the meetjoinnegation 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
2element 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 pmorphisms. 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 nonclassical 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 ongoing, 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, 22672282.
[2] Piron, Constantin, Foundations of Quantum Physics, W.A. Benjamin Inc., 1976.
 Title: Manyvalued 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 nonclassical logic is the attempt of enriching manyvalued 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) manyvalued modal logic over a given finite residuated lattice is described in [1]. The logic is defined semantically by means of Kripke models that are manyvalued in two different ways: the valuations as well as the accessibility relation among possible worlds are both manyvalued. Providing complete axiomatizations for such logics, even if we enrich the propositional language with a truthconstant for every element of the given lattice, is a nontrivial 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 manyvalued modal logic over a finite residuated lattice. Journal of Logic and Computation, 21(5):739790, 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 Gabbayde 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 nonderivable in the Gabbayde 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 weakpullback preserving functors, to a more general class of functors, i.e.; functors with quasifunctorial 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ödelLöb provability logic
Speaker: Sam van Gool (LIAFA, Université ParisDiderot & Radboud Universiteit Nijmegen)
Date: Wednesday, 16 April, 2014.
[abstract]
We give a construction of finitely generated free algebras
for GödelLö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 rulebased 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 implicationfree 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 stepbystep 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 twosorted 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 prooftheoretic aspects. This includes developing a method which detects when a specific rulebased calculus Ax axiomatizing a given logic L has the socalled 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 pmorphic 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 firstorder provers). For more complicated logics, some ingenuity is still needed, however we were able to successfully apply our uniform method to Avron's cutfree system for GL and to Goré's cutfree system for S4.3.
 Title: Cutelimination in circular proofs.
Speaker: Jérôme Fortier (UQAM / AMU)
Date: Thursday, 20 February, 2014.
[abstract]
Circularlydefined objects (e.g. inductive and coinductive types) live in the world of mubicomplete categories, where they arise from the following operations: finite products and coproducts, initial algebras, and final coalgebras. In the spirit of the CurryHoward 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 mubicomplete 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 cutelimination 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 nonwellfounded 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 HennessyMilner 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 nonrelational modalities capturing, e.g., uncertainty or collaboration. We develop a generic framework for nonrelational 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/coalgannouncements.pdf.
 Title: An algebraic approach to cutelimination 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 cutelimination theorem for substructural logics using quasicompletions of FLalgebras. It is also shown that quasicompletions of FLalgebras 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), 209240.
[2] A. Ciabattoni , N. Galatos and K. Terui, Algebraic proof theory for substructural logics: Cutelimination and completions, Annals of Pure and Applied Logic, Volume 163, Issue 3, March 2012, pp. 266290.
 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 EilenbergMoore 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 EilenbergMoore 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 EilenbergMoore 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 2category to the 2category 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 backandforth 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 nonequational examples.
AC seminar in 2012/2013
 Title: A noncommutative 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 Priestleystyle 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 wellknown Belnap fourvalued logic, either with implication (S. Odintsov, H. Wansing et al.) or without it (G. Priest). Given that some bilattice logics are fourvalued (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 NeighborhoodSheaf Semantics for FirstOrder 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 firstorder 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 firstorder 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 firstorder logic with S4 modal
logic and with more general modal logics. Corresponding to the pointset
and algebraic formulations of Tarski's topological semantics, the semantics
of this paper will be presented in both pointset and topostheoretic
formulations.
AC seminar in 2009/2010
AC seminar in 2008/2009
AC seminar in 2007/2008
AC seminar in 2006/2007
