Title: Choicefree Stone duality
Speaker: Nick Bezhanishvili (ILLC)
Date: Wednesday, 17 April.
[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.
[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.
[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.
[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 mucalculus
Speaker: Yde Venema (ILLC)
Date: Wednesday, 26 October.
[abstract]
We discuss a number of semantic properties pertaining to formulas of the modal
mucalculus. For each of these properties we provide a corresponding syntactic
fragment, in the sense that a mucalculus formula \phi has the given property
iff it is equivalent to a formula \phi' in the corresponding fragment. Since
this formula \phi' will always be effectively obtainable from \phi, as a
corollary, for each of the properties under discussion, we prove that it is
decidable in elementary time whether a given mucalculus 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 \phi will be that \phi, 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.
[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.
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.
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
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.
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
