TACL 2019 Summer School

Île de Porquerolles,  10 - 15 June 2019

The summer school is an École thématique of the CNRS and a satellite event of the TACL 2019 conference. Both events focus on logic and the tools provided by topology, algebra, and category theory. Hence the name TACL, for Topology, Algebra, and Categories in Logic. TACL conferences and schools provide a healthy environment for interactions between computer scientists and mathematicians working in logic. The TACL conference has been held every two years since 2003 and since 2013 a summer school, such as the present one, has been associated to the conference.

The week is organized around four advanced lectures on central themes of TACL. Each lecture consists of five sessions of one hour and two exercise sessions of two hours each. Besides, one or two sessions of short presentations (15 minutes + questions) and a poster session will be organized.

Le Centre national de la recherche scientifique Université Côte d'Azur

Group picture


Maria Manuel Clementino
Coimbra University

Title: Category Theory


As stressed in the name of this series of conferences, Algebra, Category Theory, and Topology play important roles in the study of Logic. This course intends to introduce the basic notions and methods of Category Theory, illustrating them with applications to Algebra, Topology, and Logic. It is also meant as a warm-up to the following course in Categorical Logic.

The course is divided in 5 one-hour lectures, and 4 hours of exercises. The lectures will focus on:

  1. Categories, functors, and natural transformations
  2. Limits and colimits
  3. Presheaves and the Yoneda Lemma
  4. Adjoint functors
  5. Cartesian closed categories and elementary toposes.

André Joyal
University of Quebec - Montreal

Title: Topos Theory


What is first order logic? The answer depends on your philosophy and your purpose. My goal is to present the algebraic structure of first order logic. In three kinds: geometric, intuitionistic and classical. We shall use the notion of first-order logical doctrine for this purpose (it is a special case of the notion of hyper-doctrine by F.W. Lawvere). The notion of frames and topos theory will play an important role in the description (I will not suppose that the participants are familiar with topos theory). A pre-doctrine is defined to be a functor

P: FinPoset

where Fin denotes the category of finite sets and Poset denotes the category of partially ordered sets. A geometric doctrine is pre-doctrine satisfying a few more conditions; similarly for the notions of Heyting doctrine and of boolean doctrine. The latter constitute a complete algebraic description of classical first-order predicate logic (like the notion of boolean algebra for classical propositional logic). I will introduce the notion of model of a geometric doctrine, and the notion of morphism between models. If times permits, I will introduce the classifying topos of a geometric doctrine.

The course is divided into 5 sessions of 1 hour, with 4 hours of exercises.

  1. On frames, Heyting algebras and Boolean algebras;
  2. Presheaf toposes, algebra of relations in a topos;
  3. Pre-doctrines, quantifiers and the equality relation;
  4. The doctrines of geometric logic, of Heyting logic and of boolean logic;
  5. Models and classifying toposes.


  • B. Jacobs, Categorical logic and type theory, North-Holland, 1999.
  • P.T. Johnstone, Sketches of an Elephant, Oxford, 2002.
  • A. Kock & G. E. Reyes, Doctrines in Categorical Logic, Handbook of Math. Logic, 1977.
  • F.W. Lawvere, Equality in hyperdoctrines and the comprehension schema as an adjoint functors, AMS, 1970.
  • J. Picado & A. Pultr, Frames and Locales, Birkhäuser, 2012.
  • A. M. Pitts, Tripos theory in retrospect, Math. Struc. in Comp. Sci, 2002.
  • R.A.G. Seely, Hyperdoctrines, natural deduction and the Beck condition, Zeitschrift, 1983.
  • Todd Trimble, Notes on predicate logic, nLab.

George Metcalfe
University of Bern

Title: Bridges between Algebra and Logic
Slides: part 1, part 2, part 3, part 4


This course will be about building and crossing (in both directions) bridges between the fields of algebra — understood, crudely, as the study of structure — and logic, understood, again crudely, as the study of consequence. Such bridges can be beneficial for practitioners of both disciplines. Indeed, in favourable cases, results obtained in one domain can be imported directly into the other using so-called “bridge theorems”. For example, algebraic properties such as coherence, amalgamation, and the congruence extension property for a class of algebras are closely related to properties of equational consequence such as (uniform) interpolation and existence of a deduction theorem. In this course, we will consider these and other properties first in the setting of intuitionistic logic and Heyting algebras (including Pitts’ uniform interpolation theorem), and then in the more general setting of universal algebra. A wide range of examples and applications will be given throughout the course, spanning, in particular, classes of lattices and (ordered) groups, modal logics, and substructural logics.

Yde Venema
University of Amsterdam

Title: Duality Theory
Course notes: 1-introduction.pdf, 2-generalizations.pdf, 3-modal-duality.pdf, 4-duality-and-logic.pdf


Duality is a fundamental principle that reveals deep connections between algebraic and geometrical ways of approaching mathematics. As its manifestation in logic and computer science, duality theory builds bridges between syntax and the structures that interpret it, and between deductive systems and their relational/topological semantics. The term `duality’ is often used in a rather intuitive sense, but it can be made mathematically precise in category theory, where a duality is a contravariant equivalence between two categories.

The course will give a first introduction to the role of duality theory in propositional logic. We will focus on the structures that feature in algebraic logic, such as Boolean algebras, distributive or modal algebras, and the spatial (i.e., relational/topological) structures that provide the semantics of the corresponding logics. In the first part of the course we will discuss various examples of categorical dualities, starting with Stone’s duality for Boolean algebras. In the second part we will see how to use these dualities by connecting and comparing algebraic and spatial concepts. Examples include the notions of correspondence and canonicity, subdirect irreducibility, and the Vietoris construction.

Below is a tentative table of contents:

  1. Basis: Stone duality for Boolean algebras.
  2. Variations: distributive lattices, Heyting algebras and frames.
  3. Extensions: modal algebras
  4. Connections: correspondence and canonicity
  5. Transfer: subdirect irreducibility and the Vietoris construction.
Prerequisites: Some familiarity with (propositional) logic, (Boolean) algebras, and basic topology will be presupposed; prior exposure to modal logic will be useful, but not essential.