DIAgrammatic LOGic

Diagrammatic Logic provides a new algebraic point of view about logic, which is well suited for studying computational effects in programming languages. Some aspects of theoretical computer science require the collaboration of several logics. For instance, the computational effects in a language can be described with the help of three related logics. The collaboration of several logics can be expressed thanks to morphisms in a relevant category of logics.

Diagrammatic logics are defined in terms of categories of fractions, limit sketches and locally presentable categories [Duval-Lair 2002, Duval 2003]

A **diagrammatic logic** is defined as a functor L with a
full and faithful right adjoint R,
induced by a morphism of limit sketches.
The target of L is the category of **theories** and
the source of L is the category of **specifications**;
a specification Σ is a **presentation** of the theory L(Σ).
There can be several descriptions of such a functor L,
providing several deduction systems for generating a theory
from a specification.

A **model** of a specification Σ with values in a theory Θ
is a morphism of theories from L(Σ) to Θ, or equivalently
a morphism of specifications from Σ to R(Θ).
Instances and inference rules
are defined as fractions with respect to the localization functor L,
and an inference step as a composition of fractions.
The definition of **morphisms of logics** follows easily, so that we get
the category of DIAgrammatic LOGics.

See my Publications with César Domínguez, Jean-Guillaume Dumas, Laurent Fousse and Jean-Claude Reynaud and the short paper:

- Dominique Duval. Logical rules as fractions and logics as sketches (2018). arXiv:1807.01620.