A Kripke-Joyal Semantics for Noncommutative Logic in Quantales
A structural semantics is developed for a first-order logic, with infinite
disjunctions and conjunctions, that is characterised algebraically by quantales.
The model structures involved combine the ``covering systems'' approach of
Kripke-Joyal intuitionistic semantics from topos theory with the ordered
groupoid structures used to model various connectives in substructural logics.
The latter are used to interpret the noncommutative quantal
conjunction & (``and then'') and its residual implication connectives.
The completeness proof uses the MacNeille completion and the theory of
quantic nuclei to first embed a residuated semigroup into a quantale, and
then represent the quantale as an algebra of subsets of a model structure.
The final part of the paper makes some observations about quantal modal logic,
giving in particular a structural modelling of the logic of closure operators on quantales.