Modal Logic and Stone Duality

Description

This workshop aims to bring together researchers working in modal logic, duality theory, algebra, point-free topology, domain theory and coalgebraic logic; fields which are all connected through logic and Stone duality.

Modal and intuitionistic logics are used to reason formally about a wide range of subjects, including possibility, belief, knowledge, the past and the future, interaction, behaviour and constructive mathematics. Stone duality connects different areas of mathematics which play a role in the study of modal logics, such as algebra, topology and coalgebra. Moreover, Stone duality plays a role in the study of computation and the foundations of mathematics, by connecting domain theory to logic, and by uniting logic and topology into point-free topology.

This workshop will coincide with the PhD defense of Jacob Vosmaer at the University of Amsterdam on 14 December 2010.

Abstracts

• Georges Hansoul, Université de Liège.
  The variable free fagment of K4 and primitive spaces.
  Consider the canonical model for K4 over the empty set of variables: M = (M, R) where R is some transitive relation.
  
  On the other hand, let us call primitive a Boolean space which has a basis of pi clopen subsets, where X is pi if X \cong X1+X2 implies X \cong X1 or X \cong X2. The set N of isomorphism types of pi primitive spaces can be endowed with the relation \triangleleft induced by X \triangleleft Y iff X+Y \cong Y, giving rise to a Kripke frame N =(N,\triangleleft).
  
  It has been observed that the sets of "finite" members of M and N are isomorphic (where m \in M is "finite" if R(m) is finite). This raises two questions that we shall debate:
  1. why is it so?
  2. can we extend this isomorphism to all of M, or N?
• Achim Jung, University of Birmingham
  The Hofmann-Mislove Theorem.
  The Hofmann-Mislove Theorem states that there is a bijection between Scott-open filters of open sets and compact saturated subsets of a sober space. What is to all appearances a technical result from Stone duality has over the years been found to play a central role in mathematical semantics. In this talk I plan to give an introduction to the theorem, its setting, its proof, its applications, and a more recent generalisation to four-valued logic.
• Alexander Kurz, University of Leicester
  Coalgebraic Logic via Stone Duality.
  In the same way as coalgebras are given wrt a functor on the category of sets, Stone Duality suggest that logics for coalgebras should be given by functors on the category of Boolean algebras (or related categories). I will survey how this approach allows to chart a considerable part of the work on coalgebras and modal logic and how it opens the way to further questions and generalisations.
• Alessandra Palmigiano, Universiteit van Amsterdam.
  Correspondence theory via Duality: Sahlqvist and beyond.
  Sahlqvist theory is among the most celebrated and useful results of the classical theory of modal logic, and one of the hallmarks of its success. Traditionally developed in a model-theoretic setting, it has been significantly extended over the years, both in syntactic ways, e.g. with the definition of inductive formulas, and in algorithmic ways, viz. e.g. the algorithm SQEMA.
  
  Via Stone-type dualities, Sahlqvist theory has also been developed in the algebraic setting of canonical extensions. Inparticular, non-classical counterparts of the Sahlqvist and inductive formulas and of the algorithm SQEMA have been identified for large classes of distributive lattice-based logics and even to (non distributive, non modal) lattice-based logics.
• Steve Vickers, University of Birmingham.
  The fibrewise Vietoris hyperspace.
  Suppose p: X -> B is a bundle (just a map - no other conditions). Can we apply the Vietoris hyperspace construction fibrewise? In other words, can we construct another bundle p': V_B(p) -> B such that its fibre over each b, b*(V_B(p)) is the Vietoris hyperspace V(b*X) applied to the corresponding fibre of X?
  
  Although this description tells us about the individual fibres, what it doesn't tell us is how they glue together topologically. This becomes even more important if (as we shall) we try to do this point-free, with the Vietoris powerlocale, so there may be too few fibres.
  
  I shall explain how these details are filled in automatically by constructive (in the sense of topos-valid) reasoning. As long as all our spaces are point-free, the bundles over B are equivalent to internal locales in the topos of sheaves over B, and then it all depends on the ability to construct the Vietoris powerlocale in a topos-valid way. For its "fibrewise" nature we also need the stronger constructive property of geometricity, and I shall explain how this relates to frame presentations by generators and relations, and how the powerlocale can be described in terms of them.
  
  Moral: reason geometrically for (point-free) spaces, and for free you get fibrewise constructions for bundles.
• Jacob Vosmaer, Universiteit van Amsterdam
  Canonical extensions in relation to their mathematical surroundings.
  Canonical extensions are an important technical tool in the representation theory of lattices and in completeness proofs for modal and other non-classical logics. We will discuss some properties of canonical extensions in relation to the following three subjects:

  • the filter and ideal completion functors;
  • profinite and Boolean topological algebras;
  • ultrafilter extensions of Kripke frames.

Programme

Venue

Location: Faculty of Science, Science Park, room A1.10.
Click here for directions.

Contact

Acknowledgments

This workshop is being made possible by financial support from the Netherlands Organisation for Scientfic Research and administrative support of the Institute for Logic, Language and Computation.