Dominique Duval
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 adjunctions [Kan 1958], categories of fractions [Gabriel-Zisman 1967] and limit sketches [Ehresmann 1968] [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 L, and an inference step as a composition of fractions. A morphism from a logic L to a logic L' is a pair of left adjoint functors which form a commutative square with L and L', induced by a commutative square of limit sketches. This yields the category of DIAgrammatic LOGics.

A major role is played by pleomorphisms: for a given logic L:S->T, a pleomorphism is "half-way" between a general morphism and an isomorphism; it is a (generally non-reversible) morphism in the category S which is mapped by the functor L to an invertible morphism in the category T. In biology, a pleomorphism is the occurrence of several structural forms during the life cycle of a plant; in diagrammatic logic, a pleomorphism refers to the occurrence of several presentations of a given logical theory during a proof: various lemmas are progressively added to the given axioms until the required theorem is obtained.