Logic Enriched over a Quantale

Abstract

Many-valued logics have a long history in mathematical logic as well as in applications to the semantics of programming languages and to engineering more generally. Typically these logics are rich with features motivated by the particular applications they stem from. In his 1973 article “Metric Spaces, Generalized Logic, and Closed Categories”, Lawvere argued that any quantale $\mathrm{\Omega }$ gives rise to a generalized $\mathrm{\Omega }$-valued logic that has as its models the categories enriched over the quantale. This suggests developing a uniform framework for many-valued logics parameterized in a quantale. In this talk we will review some previous and ongoing work in that direction. In particular, we will address (not necessarily answer) the following questions.

• $\mathrm{■}$

  If we take as our starting point, generalizing from 2-valued lattice logic, a logical language that comprises not only meets and joins (limits and colimits) but also tensor and power (weighted limits and colimits), what laws do these operations satisfy?

• $\mathrm{■}$

  This question can be investigated for different types of semantics, generalizing the set-theoretic and the polarity-based semantics known from the 2-valued setting.

• $\mathrm{■}$

  Which additional properties obtain if the quantale is integral or commutative or finite or distributive, etc?

• $\mathrm{■}$

  On the other hand, quantale logics can also be investigated from a purely proof theoretic point of view, leading us to consider sequent calculi with turnstiles ${⊢}_{\omega }$ labelled by elements $\omega \in \mathrm{\Omega }$.

• $\mathrm{■}$

  As Galatos and Jipsen showed, there are 1662 “Residuated Lattices of Size up to 6”. Each of them generates a different and potentially interesting logic.

• $\mathrm{■}$

  The adjunction ${\mathrm{\Omega }}^{-}⊣{\mathrm{\Omega }}^{-}:\mathrm{\Omega }{\text{-cat}}^{\text{op}}\to \mathrm{\Omega }\text{-cat}$ exists for any quantale $\mathrm{\Omega }$. What is the logic enshrined in the monad of that adjunction? How far can one extend this to a theory of Stone duality for quantale logics parametric in the quantale?

• $\mathrm{■}$

  The Dedekind-MacNeille completion generalizes to quantale categories. Similarly, the theory of canonical extensions originating with Jonsson and Tarski (and important for completeness proofs of modal logics) can be extended to quantale logics.

• $\mathrm{■}$

  Since the discrete functor $\text{Set}\to \mathrm{\Omega }\text{-cat}$ is dense in the sense of Kelly, set-functors (equipped with an $\mathrm{\Omega }\text{-cat}$ structure or not) can be extended to quantale categories via enriched left Kan extensions. This gives rise to a uniform variety of type constructors (endofunctors) on quantale categories parameterised by the quantale.

• $\mathrm{■}$

  Each endofunctor on $\mathrm{\Omega }\text{-cat}$ gives rise to a category of coalgebras with their own notion of behavioural equivalence. How many of the existing notions of many-valued (probabilistic, metric, fuzzy, etc) bisimulation can be accounted for in this uniform framework?

• $\mathrm{■}$

  Morphism between quantales gives rise to change-of-base principles between categories of (co)algebras. Which transfer principles can be obtained from a systematic investigation of change of base for quantale categories?

• $\mathrm{■}$

  Exploiting the duality of coalgebras (as models of computation) and algebras (as modal logics), which general logical theory of computation arises from putting the items in this list together?