An algebraic generalization of Kripke
structures∗
Sérgio Marcelino and Pedro Resende
Abstract
The Kripke semantics of classical propositional normal modal logic
is made algebraic via an embedding of Kripke structures into the larger
class of pointed stably supported quantales. This algebraic semantics
subsumes the traditional algebraic semantics based on lattices with
unary operators, and it suggests natural interpretations of modal logic,
of possible interest in the applications, in structures that arise in ge-
ometry and analysis, such as foliated manifolds and operator algebras,
via topological groupoids and inverse semigroups. We study complete-
ness properties of the quantale based semantics for the systems K, T,
K4, S4, and S5, in particular obtaining an axiomatization for S5 which
does not use negation or the modal necessity operator. As additional
examples we describe intuitionistic propositional modal logic, the logic
of programs PDL, and the ramified temporal logic CTL.
1 Introduction
It is well known that the set ℘(W × W ) of all the binary relations on a
set W has the structure of a unital involutive quantale (see §2). Hence, a
Kripke structure (W,R) as it appears in the semantics of propositional normal
modal logic [3, 4], where W is the set of possible worlds and R ⊂W ×W is
the accessibility relation, can be regarded as an example of a pointed unital
involutive quantale (℘(W ×W ), R). This suggests a way of generalizing the
notion of Kripke structure, namely in terms of a more general pointed unital
involutive quantale (Q,α), and the purpose of this paper is to assess the
usefulness of this idea with respect to the semantics of modal logic.
∗Research supported in part by Fundação para a Ciência e a Tecnologia through pro-
gram POCI 2010/FEDER and project POCI/MAT/55958/2004.
http://arxiv.org/abs/0704.1886v1
Not every unital involutive quantale is suitable for this purpose, and in
this paper we restrict to the notion of stably supported quantale that has
been introduced in [14]. In order to motivate this let us consider again the
quantale ℘(W ×W ) of binary relations on W . Each relation R ⊂ W ×W
has a domain dom(R) = {x ∈ W | ∃y (x, y) ∈ R} and, since the diagonal
relation
∆W = {(x, y) ∈ W ×W | x = y}
is of course isomorphic to W , we can equivalently replace the domain of R
by the set
ςR = {(x, x) ∈ ∆W | x ∈ dom(R)} ,
which we refer to as the support of R. This defines an operation
ς : ℘(W ×W )→ ℘(W ×W )
that preserves unions and in addition satisfies the following properties, for
all R, S ⊂W ×W :
ςR ⊂ ∆W
ςR ⊂ RR∗
R ⊂ ςRR
ς(RS) ⊂ ςR
A stably supported quantale, or simply ssq, is defined to be a unital involutive
quantale Q equipped with a sup-lattice endomorphism ς : Q → Q which
satisfies these properties; that is, for all a, b ∈ Q we have
ςa ≤ e
ςa ≤ aa∗
a ≤ ςa a
ς(ab) ≤ ςa
For each a ∈ Q the element ςa is called the support of a, the operation ς itself
is referred to as the support of Q, and the set ςQ = {ςa | a ∈ Q} is necessarily
a locale whose binary meet operation coincides with the multiplication of the
quantale: a∧b = ab. For instance, if Q = ℘(W×W ) we have ςQ = ℘(∆W ) ∼=
℘(W ).
The formulas of propositional modal logic can be easily interpreted on
any pointed ssq (Q,α): there should be a valuation map v assigning to each
formula ϕ an element v(ϕ) ∈ ςQ. The properties that such a map must
satisfy are clear. For instance, conjunction of formulas should be interpreted
as multiplication in Q: v(ϕ∧ψ) = v(ϕ)v(ψ); and the remaining propositional
connectives are equally straightforward, both classically and intuitionistically
(see §3). As regards the modal operator ♦ of possibility, we impose
v(♦ϕ) = ς(αv(ϕ)) .
This is easily seen to yield the usual interpretation on Kripke structures:
v(♦ϕ) corresponds to the domain of the relation αv(ϕ), where α is the ac-
cessibility relation.
Algebraic semantics. If (Q,α) is a pointed ssq then ςQ becomes a locale
equipped with unary operators in a natural way (§§3, 5), and it will be seen
in this paper that from any such locale it is possible to obtain a pointed ssq,
in fact giving us an adjunction between two categories, and generalizing the
way in which a binary relation on W (i.e., an accessibility relation) corre-
sponds classically to a unary operator ♦ : ℘(W ) → ℘(W ). This leads to a
semantics that subsumes the classical algebraic semantics based on lattices
with operators.
The systems of modal logic that are characterized by special kinds of
accessibility relations can be characterized by subcategories of the category
StabQu∗ of pointed ssqs. For instance, the system S5, which is characterized
by accessibility being an equivalence relation, will correspond to the full
subcategory of StabQu∗ whose objects (Q,α) are those satisfying α
2 = α∗ =
α ≥ e. Moreover, it is easy to address multi-modal logics, such as dynamic
logic, logics of time and space, etc., in terms of the category whose objects
are ssqs equipped with more than one point, the various points satisfying
suitable relations.
The category StabQu of ssqs has pleasant properties [14]. For instance,
there is at most one support on any unital involutive quantale, and any
homomorphism of unital involutive quantales h : Q → Q′ between ssqs Q
and Q′ automatically preserves the support (hence, being stably supported
is a property rather than extra structure). The category StabQu is therefore
a full subcategory of the category of unital involutive quantales, and in fact
it is reflective. There are presentations of ssqs by generators and relations,
which play the role of “Lindenbaum algebras” in the context of the quantale-
based semantics. For instance, the “Lindenbaum quantale” for S5 is the
pointed ssq QS5 generated by the usual Lindenbaum algebra of S5 (with
defining relations ensuring that it is a bounded sublattice of ς QS5) with the
distinguished point α ∈ QS5 being subject to the relations α
2 = α∗ = α ≥ e.
The usual Kripke structure based models for S5 can be identified with the
relational representations of QS5, in other words the homomorphisms
h : QS5 → ℘(W ×W )
of unital involutive quantales (see [10] for some properties of such representa-
tions). The same identification of models with the relational representations
of a quantale applies to many other well known examples of modal logics.
Groupoids and inverse semigroups. An important aspect of the se-
mantics described in this paper is that there are plenty of examples of ssqs
besides the quantales of binary relations [14], arising from various geomet-
ric or analytic structures, and thus we are provided with a uniform way of
defining semantic interpretations of propositional normal modal logic based
on such structures. More precisely, let G be a groupoid (i.e., a small category
all of whose arrows are isomorphisms). Writing G also for the set of groupoid
arrows, ℘(G) is an ssq; the quantales of binary relations ℘(W ×W ) are pre-
cisely the quantales that arise from the so-called pair groupoid of W , which
hasW as set of objects andW ×W as set of arrows, with the two projections
W ×W → W being the domain and codomain maps of the groupoid. Even
more generally, the topology Ω(G) of any topological étale groupoid G is a
sub-ssq of ℘(G); and for localic étale groupoids, too, there is an ssq O(G)
associated to each groupoid G.
These facts are a part of the close relation [14] between the notions of étale
groupoid (either topological or localic), inverse semigroup, and quantale,
which can be summarized in the following diagram whose arrows denote
bijections of objects up to isomorphism, or even, in the case of I and L∨,
equivalences of categories:
Inverse
quantal
frames
Étale
groupoids bisections
Complete
infinitely
distributive
inverse
semigroups
germspp
The inverse quantal frames are the ssqs that arise from étale groupoids.
It follows that the quantale semantics automatically provides a bridge
between modal logic and those areas of mathematics where examples of étale
groupoids and inverse semigroups occur, such as operator algebras and dif-
ferential topology — see, e.g., [7, 8, 12]. As an example of the latter, foliated
manifolds can be associated to dynamical systems, and from a foliation it is
always possible to construct a topological étale groupoid [8]. We shall not
deal with any such examples in this paper, but we mention that if we replace
℘(W ×W ) by a more general groupoid quantale, hence taking as models
of propositional modal logic the homomorphisms Q → Ω(G) or Q → O(G)
instead of Q → ℘(W ×W ) (where Q is a Lindenbaum quantale), we are
led in a natural way to semantics which may be interesting, say, for applied
logicians or computer scientists dealing with hybrid systems, logics of real
time and space, etc.
Overview. Let (Q,α) be a pointed ssq. Then the locale ςQ is canonically
equipped with the two unary sup-latice endomorphisms ♦ and � defined by,
for each x ∈ ςQ,
♦x = ς(αx) (1)
�x = ς(α∗x) , (2)
which are easily seen to satisfy the following conjugacy conditions (see §5):
♦x ∧ y ≤ ♦(x ∧ �y)
�x ∧ y ≤ �(x ∧ ♦y) .
Such a structure (L,♦,�), where L is a locale and ♦ and � satisfy the
conjugacy conditions, will be called a bimodal frame, and there is a functor
from the category of pointed ssqs to the obvious category of bimodal frames.
A functor in the opposite direction can be easily obtained just from the
knowledge that ssqs can be presented by generators and relations; given a bi-
modal frame (L,♦,�) its associated quantale Q is generated by the elements
of L plus an element α, with relations imposing both that L is a unital invo-
lutive subquantale of Q and that (1) and (2) are satisfied. As we shall see,
this defines a functor which is left adjoint to ς, and in fact it is a coreflection;
hence, we always have an isomorphism of bimodal frames L ∼= ςQ.
We can interpret this isomorphism in a logical sense as saying that no
theorems are added in the process of interpreting ♦ and � in terms of the
quantale operations. Hence, if we think of the addition of the quantale
operations as a language extension then this extension is conservative — the
conjugacy conditions are a complete axiomatization for the modal operators
induced by α and α∗.
This of course suggests looking at several systems of modal logic and their
completeness theorems, which we shall do for K, T, K4, and S4, showing that
the usual conditions on ♦ (and here also on �), as taken from the standard
completeness theorems of modal logic, are precisely what is required for a
coreflection to be obtained when the pointed ssqs (Q,α) under consideration
satisfy the expected conditions, such as “reflexivity”, “transitivity”, etc., of
the point α. Hence, the theorems which we prove in this paper can be re-
garded as an algebraic generalization of the standard completeness theorems
for these systems of propositional normal modal logic. It is worth noting
that, as opposed to the classical theorems, these are now independent of the
axiom of choice (which is required in the proof of the classical theorems,
in the form of Zorn’s lemma). From our results we also obtain a complete
axiomatization of system S5, where to the axioms of S4 one adds the axiom
scheme
♦ϕ ∧ ψ → ♦(ϕ ∧ ♦ψ) .
This is obtained from the conjugacy conditions by making ♦ = � and, as
opposed to the usual axiom scheme ϕ→ �♦ϕ, it does not mention negation
or the modal necessity operator.
The remainder of this paper goes as follows. In §2 we provide some nec-
essary background and preliminary results on quantales, presentations by
generators and relations, etc. Then in §3 we describe in detail the quantale-
based semantics of propositional normal modal logic, including the systems
K, T, K4, S4, and S5. In order to illustrate the flexibility of this approach we
provide additional examples, namely propositional intuitionistic logic, propo-
sitional dynamic logic, and the ramified temporal logic CTL. Finally, after
some technical results in §4 about graded quantales (the quantale analogue
of graded rings), in §5 we address the adjunctions mentioned above. The
mere existence of the adjunctions is a consequence of the existence of pre-
sentations by generators and relations; in other words, it can be phrased in
terms of the existence of the Lindenbaum quantales. However, in order to
obtain additional information about the adjunctions and, in particular, in
order to prove that they are coreflections, we shall need an actual construc-
tion of the Lindenbaum quantales. This will be conveniently formulated in
terms of “tensor algebras” over bimodal frames, and it will take up most of
2 Preliminaries
Here we describe some background on sup-lattices, locales and quantales.
General references are [5, 6, 9, 11, 15].
Sup-lattices. We shall denote the category of sup-lattices by SL. The
objects are the complete lattices and the morphisms are the maps f : L→M
that preserve arbitrary joins: for all X ⊂ L
f(x) .
We shall write 1L or simply 1 for the lattice unit (the greatest element) of a
sup-lattice L, and 0L or simply 0 for the least element.
Let (Li) be a family of sup-lattices. Their cartesian product
Li is a
sup-lattice with pointwise order and joins, and it is a product in the category
SL. The products and the coproducts are isomorphic [6], similarly to abelian
groups (but, contrary to the latter, also in the case of infinitary coproducts).
We denote by
Li the categorical coproduct of a set-indexed family of
sup-lattices (Li), and call it direct sum.
The tensor product of L and M is denoted by L ⊗M , and similarly to
vector spaces, it is the image of a universal bi-morphism, where a sup-lattice
bi-morphism f : L ×M → N is a map that preserves joins in each variable
separately:
f(x, y)
f(x, y) .
Concretely, L⊗M can be identified with the set of those subsets I ⊂ L×M
such that
∈ I ⇐⇒ {x} × Y ⊂ I
∈ I ⇐⇒ X × {y} ⊂ I
for all x ∈ L, y ∈ M , X ⊂ L, and Y ⊂ M . The universal bi-morphism
L×M → L⊗M is defined by (x, y) 7→ x⊗ y, where x⊗ y is the least such
set that contains the pair (x, y), which is called the pure tensor generated by
(x, y). SL is a monoidal category with respect to this tensor product, with
the powerset ℘( 1) of the singleton set as the tensor unit. Similarly to the
category of abelian groups, the functor hom(N,−) has a left adjoint −⊗N
for each N ; that is, we have the familiar isomorphism
hom(M ⊗N,L) ∼= hom(M, hom(N,L)) ,
natural in the variables M and L, which in fact is an order isomorphism. As
a consequence of colimit preservation by left adjoints, ⊗ distributes over
Mi) ∼=
(L⊗Mi) .
Quotients of sup-lattices can be conveniently handled by means of closure
operators (monotone endomaps j that satisfy a ≤ j(a) and j(j(a)) = j(a)
for every element a). Let L be a sup-lattice and j a closure operator on L.
The set of j-closed elements
Lj = {x ∈ Q | x = j(x)}
is a sup-lattice closed under the formation of meets in L, with joins given by
(xi) = j(
xi), and the map j : L → Lj is a (surjective) homomorphism
of sup-lattices. Conversely, given a set S ⊂ L closed under meets in L, we
obtain a closure operator jS : L→ L by
jS(x) =
{y ∈ S | x ≤ y} .
These constructions are mutually inverse,
jLj = j LjS = S ,
and every sup-lattice quotient arises in this way up to isomorphism.
The relation to the usual description of quotients by means of congruence
relations (i.e., equivalence relations on L which are sub-sup-latttices of L×L)
is the following: from a closure operator j we obtain the congruence relation
θj ⊂ L× L defined by
(x, y) ∈ θj ⇐⇒ j(x) = j(y)
[in particular (x, j(x)) ∈ θj ] and from a congruence relation θ ⊂ L × L we
define a closure operator jθ by
jθ(x) =
where [x]θ is the congruence class of x; of course, we have jθj = j and θjθ = θ.
Stably supported quantales. A quantale is a sup-lattice equipped with
an associative multiplication, usually written (a, b) 7→ ab, which distributes
over arbitrary joins:
(abi) ,
(aib) .
Hence, a quantale is a semigroup in SL. A quantale Q is unital if the multi-
plication has a unit, which we denote by eQ, or simply e.
Example 2.1 A locale, or frame, L is a sup-lattice satisfying the following
distributivity property for all x ∈ L and Y ⊂ L:
x ∧ y .
Hence, a locale is a unital quantale whose multiplication is ∧ and whose
unit e coincides with 1. In particular, it is a commutative and idempotent
quantale. A quantale is a locale if and only if it is unital with e = 1 and it
is idempotent [6].
An involutive quantale Q is a quantale equipped with an involution
(−)∗ : Q→ Q ,
i.e., a join preserving operation that makes Q an involutive semigroup:
(ab)∗ = b∗a∗,
a∗∗ = a.
Any involutive quantale satisfies 1∗ = 1 and, if it is unital, e∗ = e.
Hence, a unital involutive quantale is an involutive monoid
℘( 1)
←− Q⊗Q
in the monoidal category of sup-lattices, with ab = m(a⊗ b).
Definition 2.2 Let Q be a unital involutive quantale. A support on Q is a
sup-lattice endomorphism ς : Q→ Q satisfying, for all a ∈ Q:
ςa ≤ e , (3)
ςa ≤ aa∗ , (4)
a ≤ ςaa . (5)
A supported quantale is a unital involutive quantale equipped with a spec-
ified support. On a supported quantale the set of supports ςQ coincides with
↓e = {x | x ≤ e} and it is a locale with ab = a ∧ b [14].
Definition 2.3 A support is stable if it satisfies ς(ab) = ς(aς(b)). A quantale
equipped with a specified stable support is stably supported, or simply an ssq.
Every homomorphism of unital involutive quantales preserves the support
of an ssq, and thus the category of ssqs, StabQu, is defined to be the full
subcategory of the category of unital involutive quantales Qu whose objects
are the ssqs. Moreover, if a quantale is stably supported then it can have
no other support, stable or not [14]. Hence, being stably supported should
be regarded as a property of unital involutive quantales rather than extra
structure. In [14] it has also been seen that the inclusion functor StabQu →
Qu has a left adjoint (i.e., StabQu is a reflective subcategory of Qu).
Any locale is an ssq with trivial involution and support:
x∗ = x ςx = x .
Nuclei and quotients. The quotients of ssqs are described in a similar
way to those of sup-lattices. We give here an overview and refer to [14] for
further details.
Definition 2.4 A (quantic) nucleus on an ssq Q is a closure operator
j : Q→ Q
that satisfies, for all x, y ∈ Q,
j(x)j(y) ≤ j(xy) ,
j(x)∗ ≤ j(x∗) ,
ς(j(x)) ≤ j(ς(x)) .
We remark that the second condition is equivalent to j(x)∗ = j(x∗).
The set of j-closed elements Qj = {x ∈ Q | x = j(x)} is an ssq with
joins
(xi) = j(
xi), multiplication x · y = j(xy), with the same involution
as Q, and support δx = j(ςx). The map j : Q → Qj is a (surjective)
homomorphism of ssqs:
j(xi)
j(xy) = j(x) · j(y)
j(x∗) = j(x)∗
j(ςx) = δx .
Furthermore, every quotient arises in this way up to isomorphism.
The set N(Q) of nuclei is a complete lattice under the pointwise order,
with meets being calculate pointwise: j ≤ k ⇔ ∀x∈Q(j(x) ≤ k(x)), and
jα(x) =
(jα(x)). Furthermore, we have j ≤ k ⇔ Qk ⊂ Qj, and
the join of nuclei corresponds to intersection of the respective sets of closed
elements: j =
jα if and only if Qj =
Qjα .
Definition 2.5 Let Q be an ssq, and R ⊂ Q×Q. The supported closure R
of the binary relation R is the smallest relation that contains R and is closed
for the quantale operations, i.e.:
R ⊂ R ;
(y, z) ∈ R ⇒ (ay, az) ∈ R, for all a ∈ Q ;
(y, z) ∈ R ⇒ (ya, za) ∈ R, for all a ∈ Q ;
(y, z) ∈ R ⇒ (ςy, ςz) ∈ R ;
(y, z) ∈ R ⇒ (y∗, z∗) ∈ R .
Contrarily to what is done in [13], we shall interpret each pair (y, z) ∈ R
as an inequality y ≤ z, rather than an equation y = z. It is easy to see that
there is a least quantic nucleus j such that j(y) ≤ j(z) for all (y, z) ∈ R:
{j ∈ N(Q) | j(y) ≤ j(z) for all (y, z) ∈ R}.
Analogously to the quotients of involutive quantales described in [13], the
quantale QjR has a very simple description:
QjR = {x ∈ Q | ∀(y,z)∈R (z ≤ x⇒ y ≤ x)}.
We stress that nuclei and quotients of unital involutive quantales equipped
with any sup-lattice endomorphism ς : Q → Q are handled in exactly the
same way as described above for ssqs (we shall use this in §5 when dealing
with quantales that are just “pre-supported”). The properties of ς pass to
the quotients one by one: if j is a nucleus on Q and δ : Qj → Qj is the
sup-lattice endomorphism defined by δ(a) = j(ςa), then if, say, the equation
ς(ab) = ς(aςb) holds in Q then δ(ab) = δ(aδb) holds in Qj , etc.
Generators and relations. Let G be a set (of “generators”). The con-
struction of the unital involutive quantale Qu〈G〉 freely generated by G is
described in [13]. Denoting by F : Qu → StabQu the left adjoint to the
inclusion StabQu → Qu (cf. paragraph after ¶2.3), it follows that F (Qu〈G〉)
is the free ssq generated by G, and we shall denote it by StabQu〈G〉.
Definition 2.6 Let G and R ⊂ StabQu〈G〉 × StabQu〈G〉 be sets. The ssq
presented by the generators in G and the relations in R is
StabQu〈G | R〉
= StabQu〈G〉
If x ∈ G, one denotes by [x] the image of the generator x in the quantale
being presented. This notation provides a useful way of describing the defin-
ing relations of a quantale presentation: we just write the conditions with
respect to which the injection of generators is universal, as in the following
example for unital involutive quantales.
Example 2.7 Let L be a sup-lattice. It follows from the universal proper-
ties of the tensor product and the direct sum of sup-lattices that the unital
involutive quantale freely generated by L with joins being preserved in the
presentation,
is isomorphic to the tensor quantale
where I is the free involutive monoid on one generator, whose words can be
concretely identified with the strings of symbols α and α∗ and whose unit we
shall denote by ε, and
L(d) = L⊗|d| = L⊗ · · · ⊗ L (|d| times) .
Note that L(ε) = ℘( 1) is the neutral element of the tensor product. The
multiplication is defined on pure tensors just by concatenation
(x0 ⊗ . . .⊗ xn)(y1 ⊗ . . .⊗ ym) = x0 ⊗ . . .⊗ xn ⊗ y1 ⊗ . . .⊗ ym ,
where in the case of concatenation with elements of ℘( 1) we use the identi-
fication ℘( 1) ⊗ L ∼= L ∼= L ⊗ ℘( 1), to produce the identity of the quantale
e = 1℘( 1). The involution
(−)∗ : TL→ TL
is obtained from the isomorphisms L(w)
→ L(w
∗) that are given by
x1 ⊗ · · · ⊗ xn 7→ xn ⊗ · · · ⊗ x1 .
The injection of generators is the α-coprojection of the coproduct
L = L(α) →
L(d).
3 Quantale semantics of modal logic
Propositional normal modal logic. In this section we describe the in-
terpretations of the classical systems of modal logic K, T, K4, S4, and S5.
For details on these we refer the reader to [3, 4].
We shall consider fixed a set Π of propositional symbols. The set Φ of
propositional formulas is defined to be the least set containing Π such that
for all ϕ, ψ ∈ Φ we have
¬ϕ ∈ Φ ,
ϕ ∨ ψ ∈ Φ ,
♦ϕ ∈ Φ ,
where as usual we may define other connectives, for conjunction ∧, implica-
tion →, and the necessity modal operator �, as abbreviations:
ϕ ∧ ψ = ¬(¬ϕ ∨ ¬ψ) ,
ϕ→ ψ = ¬ϕ ∨ ψ ,
�ϕ = ¬♦¬ϕ .
Definition 3.1 A generalized Kripke model consists of a triple (Q,α, v),
where Q is an ssq, α ∈ Q is an accessibility element, and v : Φ → ςQ is an
interpretation map satisfying the following properties for all ϕ, ψ ∈ Φ:
v(ϕ ∨ ψ) = v(ϕ) ∨ v(ψ)
v(ϕ)v(¬ϕ) = 0
v(ϕ) ∨ v(¬ϕ) = e
v(♦ϕ) = ς(αv(ϕ)) .
Remark 3.2 The above definition makes each element v(ϕ) be comple-
mented in ςQ, with v(¬ϕ) being its (unique) complement, and it also follows
that conjunction is interpreted as multiplication (equivalently, meet) in ςQ:
v(ϕ ∧ ψ) = v(ϕ)v(ψ) .
This means that we interpret the formulas inside a Boolean subalgebra of ςQ,
hence obtaining a classical semantics of propositional modal logic, a fact that
was already implicit in the definition of the conjunction and the implication
as derived connectives. However, we point out that it is easy to define a
(rather natural) semantics for intuitionistic modal logic. We shall describe
this at the end of §3.
As usual we say that a pointed ssq consists of an ssq Q together with a
specified “point” α ∈ Q. A homomorphism of pointed ssqs is a homomor-
phism of ssqs that preserves the point:
h : (Q,α) → (R, β)
α 7→ β.
From now on we shall denote by BK the Lindenbaum algebra of system
K (i.e., the set of formulas modulo equivalence, which is a Boolean algebra
equipped with a finite join preserving endomorphism ♦).
Definition 3.3 The Lindenbaum quantale for K is the pointed ssq QK which
is presented by generators and relations with BK as the set of generators and
with the following relations for all x, y ∈ BK, where we denote the selected
point by α:
[x ∨ y] = [x] ∨ [y]
[¬x][x] = 0
[¬x] ∨ [x] = e
[♦x] = ς(α[x]) .
From the universal property of ssqs presented by generators and relations
we immediately obtain:
Theorem 3.4 There is a bijective correspondence between abstract Kripke
models (Q,α, v) and homomorphims of unital involutive quantales
QK −→ Q .
In particular, if W is a set then a homomorphism
ρ : QK −→ ℘(W ×W )
is the same as a model for system K with set of possible worlds W and
accessibility relation ρ(α).
In order to obtain similar facts for other systems, such as T, K4, S4, S5,
one must define the appropriate Lindenbaum quantales.
Definition 3.5 The Lindenbaum quantales for T, K4, S4, and S5, are the
pointed ssqs QT, QK4, QS4, and QS5, respectively, which are presented by
generators and relations similarly to QK, with the following additional rela-
tions:
QT: e ≤ α
QK4: αα ≤ α
QS4: e ≤ α ≥ αα
QS5: e ≤ α = α
∗ ≥ αα
Hence, QT is the quotient of QK by the least nucleus j such that j(e) ≤
j(α), and QK4 is the quotient ofQK by the least nucleus j such that j(αα) ≤
j(α). Then we have QS4 = QT ∩QK4 and QS5 is the quotient of QS4 by the
least nucleus j such that j(α) = j(α∗).
Notice that the relational representations of these quantales correspond
to the expected classes of models:
Theorem 3.6 The relational representations Q → ℘(W ×W ) of the Lin-
denbaum quantales Q correspond bijectively to the Kripke models whose ac-
cessibility relations are:
• Reflexive, for Q = QT;
• Transitive, for Q = QK4;
• Preorders, for Q = QS4;
• Equivalence relations, for Q = QS5.
Propositional ramified temporal logic. Now we describe a similar se-
mantics for the ramified temporal logic known as Computational Tree Logic
(CTL), see [2]. As above, Π is a fixed set of propositional symbols. The set
Φ of CTL formulas is defined to be the least set containing Π such that for
all ϕ, ψ ∈ Φ we have
¬ϕ, ϕ ∨ ψ,EXϕ,EFϕ,EGϕ ∈ Φ ,
and we may define other modal operators as abbreviations:
AXϕ ≡ ¬EX¬ϕ ,
AGϕ ≡ ¬EF¬ϕ ,
AFϕ ≡ ¬EG¬ϕ .
Definition 3.7 The intuitive meaning of the various modalities is the fol-
lowing:
• EXϕ means that there is a possible future where ϕ will hold in the
next time instant;
• EFϕ means that there is a possible future where ϕ will eventually hold;
• EGϕ means that there is a possible future where ϕ will always hold
(including now);
• AXϕ means that ϕ will certainly hold in the next time instant;
• AGϕ means that ϕ will always hold (including now) in all possible
future paths;
• AFϕ means that in each possible future path ϕ will eventually hold.
A generalized CTL model consists of a triple (Q,α, v), where Q is an ssq,
α ∈ Q is an accessibility element that satisfies
ς(α) = e
(i.e., time never ends), and v : Φ → ςQ is an interpretation map satisfying
the following properties for all ϕ, ψ ∈ Φ:
v(ϕ ∨ ψ) = v(ϕ) ∨ v(ψ)
v(ϕ)v(¬ϕ) = 0
v(ϕ) ∨ v(¬ϕ) = e
v(EXϕ) = ς(αv(ϕ))
v(EFϕ) = ς
v(EGϕ) =
{a ∈ Q | a ≤ v(ϕ) ∧ ς(αa)} .
It is easy to see that this interpretation conveys the intended meaning to
the modal operators if we let Q = ℘(W ×W ) for some set W . Only the
last condition, for EG, deserves an explanation. This says that EGϕ may
be interpreted as the largest subset X ⊂ W such that every world x ∈ X
satisfies the following two conditions:
• x satisfies the formula ϕ;
• there is a world y ∈ X such that (x, y) ∈ α.
This guarantees that there is an infinite path (possibly with repetitions)
x0, x1, x2, x3, . . .
satisfying ϕ starting at any world x0 where EGϕ holds. Mathematically, the
definition of v(EGϕ) is clarified by the Knaster–Tarski fixed point theorem:
the set of all the lowerbounds of v(ϕ),
S = {a ∈ ςQ | a ≤ v(ϕ)} ,
is a complete lattice and thus the set of pre-fixed points of the monotone
operator f : S → S defined by
f(a) = v(ϕ) ∧ ς(α a)
has a join, which in fact is a fixed point; hence, v(EGϕ) is also the largest
element a ∈ ςQ such that a = v(ϕ) ∧ ς(α a).
Propositional dynamic logic. In the program logic of [1] there are modal-
ities indexed by programs, which themselves form a set with some algebraic
structure. Let Π be a fixed set of propositional symbols and Ξ a set of atomic
programs. The sets F , of formulas, and P , of programs, give us the PDL
language Φ = F ∪ P , and they are defined to be the least sets such that
Π ⊂ F ,
Ξ ⊂ P ,
if ϕ, ψ ∈ F then ¬ϕ, ϕ ∨ ψ ∈ F ,
if p, q ∈ P then p ∪ q, p; q, p∗ ∈ P ,
if ϕ ∈ F and p ∈ P then 〈p〉ϕ ∈ F ,
if ϕ ∈ F then ϕ? ∈ P .
Very briefly, the intuitive meaning of the program constructs is the following:
• p∪ q is the program that behaves in a nondeterministic way either like
p or like q (the choice is made at the beginning of the execution of the
program, once and for all);
• p; q is the program whose execution is that of p followed by q;
• p∗ is the iteration of p, to be thought of as p executed sequentially zero
or more times (not to be confused with the notation for the quantale
involution);
• ϕ? is the program that tests ϕ, succeeding if ϕ is found to be true, and
failing otherwise.
Definition 3.8 A generalized PDL model consists of a pair (Q, v), where Q
is an ssq and v : Φ → Q is an interpretation map satisfying the following
properties for all ϕ, ψ ∈ F and p, q ∈ P :
v(ϕ ∨ ψ) = v(ϕ) ∨ v(ψ)
v(ϕ)v(¬ϕ) = 0
v(ϕ) ∨ v(¬ϕ) = e
v(〈p〉ϕ) = ς(v(p)v(ϕ))
v(p ∪ q) = v(p) ∨ v(q)
v(p; q) = v(p)v(q)
v(p∗) =
v(p)n
v(ϕ?) = v(ϕ) .
This interpretation shows that to a large extent both the formulas and the
programs are treated on an equal footing. In particular, p; q can be regarded
as the (noncommutative) “conjunction” of p and q, and p ∪ q as their dis-
junction, while a formula is just a particular kind of program (ϕ is identified
with ϕ?).
Intuitionistic modal logic. It is easy to define a semantics for intuitionis-
tic propositional modal logic if we let ∧ and → be independent connectives.
This is because the support ςQ of any ssq Q is a locale and therefore a
Heyting algebra, and thus, denoting by \ the residuation operation of ςQ,
b\a =
{c ∈ ςQ | b ∧ c ≤ a} ,
the conditions on v can be simply replaced by the following:
v(ϕ ∨ ψ) = v(ϕ) ∨ v(ψ)
v(ϕ ∧ ψ) = v(ϕ)v(ψ)
v(ϕ→ ψ) = v(ϕ)\v(ψ)
v(¬ϕ) = v(ϕ)\0
v(♦ϕ) = ς(αv(ϕ)) .
This would entirely define the intuitionistic semantics if we contented our-
selves with defining � = ¬♦¬ as before. However, this is a bad interpretation
of �, as for instance it usually does not satisfy the axiom of distributivity
over meets
�(ϕ ∧ ψ)↔ �ϕ ∧�ψ .
Indeed, a much better interpretation, in particular one that satisfies distribu-
tivity of � over (arbitrary) meets, is obtained if we let � be an independent
connective interpreted as the right adjoint of a suitable sup-lattice endomor-
phism, as we now describe.
LetW be a set, let R ⊂W ×W be a binary relation, and let Q be the ssq
℘(W ×W ). Let ♦ and � be the sup-lattice endomorphisms of ςQ defined as
in §1:
♦X = ς(RX)
�X = ς(R∗X) .
Equivalently, taking into account the isomorphism ςQ ∼= ℘(W ) we may
consider ♦ and � to be endomorphisms of ℘(W ):
♦X = {y ∈ W | ∃x∈X (y, x) ∈ R}
�X = {y ∈ W | ∃x∈X (x, y) ∈ R} .
It is straightforward to verify that the usual necessity operator
� : ℘(W )→ ℘(W ) ,
which is defined by
�X = {y ∈ W | ∀x∈W (y, x) ∈ R⇒ x ∈ X} ,
is right adjoint to �, and we may take this as the natural definition of �
when such a “possibility in the past” operator � is available — similarly, a
“necessity in the past” operator � can be defined to be the right adjoint of
�x ≤ y ⇐⇒ x ≤ �y
♦x ≤ y ⇐⇒ x ≤ �y .
This leads to the following quantale-based intuitionistic semantics for propo-
sitional modal logic, where we assume that ∧, →, and � are independent
connectives:
Definition 3.9 A generalized intuitionistic Kripke model consists of a triple
(Q,α, v), where Q is an ssq, α ∈ Q is an accessibility element, and v : Φ→ ςQ
is an interpretation map satisfying the following properties for all ϕ, ψ ∈ Φ:
v(ϕ ∨ ψ) = v(ϕ) ∨ v(ψ)
v(ϕ ∧ ψ) = v(ϕ)v(ψ)
v(ϕ→ ψ) = v(ϕ)\v(ψ)
v(¬ϕ) = v(ϕ)\0
v(♦ϕ) = ς(αv(ϕ))
v(�ϕ) =
{x ∈ ςQ | ς(α∗x) ≤ v(ϕ)} .
This definition illustrates a canonical way in which to define intuitionistic
semantics for other propositional modal logics, including all the examples
seen earlier in this section. We stress the fact that involutive quantales are
essential for this, since without the involution we would neither have the �
operator, nor a canonical definition of �.
It is worth commenting on some aspects of the intuitionistic version of
system S5, which similarly to its classical counterpart is based on imposing
that the accessibility element α should be self-adjoint, and thus � = ♦. The
unit of the adjunction relating � and � is the inequality
x ≤ ��x ,
and thus for intuitionistic S5 we conclude that the axiom-scheme
ϕ→ �♦ϕ (6)
is always satisfied. It is well known that this scheme (together with those
for S4) characterizes the classical system S5. Another axiom-scheme which
is always satisfied by intuitionistic S5 is
♦�ϕ→ ϕ ,
which corresponds to the co-unit of the adjunction, and which classically
(i.e., with � = ¬♦¬) is equivalent to (6).
4 Graded unital involutive quantales
Basic definitions and properties. The usual notion of grading of a ring
has a straightforward counterpart for quantales, which will be useful in §5.
We shall study it now.
Definition 4.1 LetM be an involutive monoid. A unital involutive quantale
Q is graded over M if there is an M-indexed family of sub-sup-lattices Q(m)
of Q satisfying the following two properties.
1. For each a ∈ Q there is one, and only one, element
(am) ∈
such that
2. The following conditions hold for all m,n ∈ M :
Q(m)Q(n) ⊂ Q(mn)
1Q(ε) = e
⊂ Q(m
(The latter is equivalent to
= Q(m
For each m ∈M the set Q(m) is called the component of Q in degree m.
Example 4.2 Recall the tensor quantale of ¶2.7: if L is a sup-lattice and I
is the free involutive monoid on one generator α then the tensor quantale
has an obvious grading over I such that L(ε) ∼= ℘( 1) and L(α) ∼= L.
The following properties are immediate:
Proposition 4.3 Let Q be a unital involutive quantale graded over an invo-
lutive monoid M .
1. The map (am) 7→
m∈M am is an isomorphism of sup-lattices
(m) → Q .
2. If m 6= n then Q(m) ∩Q(n) = {0}.
3. The union
m∈M Q
(m) is join-dense in Q.
4. ↓Q(m) = Q(m) for all m ∈M .
There is a convenient alternative definition if the unital involutive quan-
tale Q is also a locale (an example is the quantale TL of ¶4.2 if L is a locale,
or the quantale T(L) of §5):
Proposition 4.4 Let M be an involutive monoid, and let Q be a unital
involutive quantale which is also a locale. Then Q is graded over M if and
only if there is an M-indexed family (e(m)) of elements of Q satisfying the
following properties:
1. 1Q =
m∈M e
(m) (i.e.,
covers Q);
2. e(m) ∧ e(n) = 0 if m 6= n;
3. e(m)e(n) ≤ e(mn);
4. e(ε) = e;
≤ e(m
∗) (equiv.,
= e(m
Proof. It is clear that if Q is graded then it satisfies 1–5 if we let e(m) be
1Q(m) for each m ∈M . For the converse we define the component Q
(m) to be
↓e(m): then any element a ∈ Q equals
a ∧ 1 = a ∧
e(m) =
a ∧ e(m)
where a∧ e(m) ∈ Q(m) by definition of Q(m); and if
bm then, for
each n ∈M we have
an = an ∧
am = an ∧
an ∧ bm = an ∧ bn ,
and in a similar way we obtain bn = bn ∧ an. Hence, we have an = bn, and
thus each element a ∈ Q can be obtained uniquely as a join
am. The rest
is straightforward.
Graded nuclei and quotients. The natural notion of quotient that re-
spects the grading of a quantale is provided by the following definition:
Definition 4.5 Let Q be a unital involutive quantale graded over an invo-
lutive monoid M . A nucleus j : Q→ Q is graded if it satisfies the following
two conditions for all (am) ∈
m∈M Q
⊂ Q(m);
m∈M am
m∈M j(am).
Proposition 4.6 Let j be a graded nucleus as in the definition above. Then,
1. j(0) = 0 (the nucleus is “dense”);
2. Qj is graded, with each component being defined by
(m) = j
Proof. The first condition is obvious from the fact that 0 ∈
m∈M Q
and thus j(0) ∈
m∈M Q
(m) = {0}. For the second condition notice that if
a ∈ Qj then on one hand we have a unique representation of a as a join
and, on the other hand,
a = j(a) = j
j(am) ,
and thus am = j(am) for all m ∈M ; that is, the element am is necessarily in
(m). The rest is straightforward.
The nucleus induced by a binary relation is graded provided the relation
respects the grading:
Proposition 4.7 Let Q be a unital involutive quantale graded over an invo-
lutive monoid M . Let also R ⊂ Q×Q be a binary relation that respects the
grading in the sense that R ⊂
Q(m)×Q(m). Then jR is a graded nucleus.
Proof. Let ⊏R ⊂ Q×Q be the preorder defined by
a ⊏R b ⇐⇒ jR(a) ≤ jR(b) .
Since this is also a sub-involutive-quantale of Q×Q, let us call it a congruence
preorder. By a simple adaptation of the comments at the end of the sup-
lattices section of §2, there is a bijection between congruence preorders and
nuclei on Q, and ⊏R is the least congruence preorder on Q which contains R.
It is clear that ⊏R respects the grading because R does, and thus if a ∈ Q
then jR(a) ∈ Q
(m), showing that jR satisfies the first of the properties of
graded nuclei. In order to prove that it also satisfies the second property let
k : Q→ Q be the map defined, for each (am) ∈
Q(m), as follows:
jR(am) .
Since jR is monotone we have k ≤ jR:
jR(am) = k
Now let us see that k is itself a nucleus. First, it is obvious that it is monotone
and that it satisfies a ≤ k(a) for all a ∈ Q. It is also idempotent because
jR(am)
and the fact that jR(am) ∈ Q
(m) allows us to conclude that the right hand
side of the above equation equals
jR(jR(am)) =
jR(am) = k
Now let us prove the condition relating k to the multiplication. For each pair
(am), (bm) ∈
Q(m) we have
jR(am)
jR(bm) =
jR(ap)jR(bq)
jR(apbq)
The condition relating k to the involution is equally simple and we omit
it. Finally, it is obvious that for (a, b) ∈ R we have k(a) ≤ k(b), since
jR(a) ≤ jR(b). But, by definition, jR is the least nucleus that satisfies this
condition, and therefore we conclude that k = jR. Hence, jR is graded.
5 Construction of the Lindenbaum quantales
The involutive tensor quantale of a frame. Let L be a frame, and
denote by I the free involutive monoid on one generator α, whose words are
the finite sequences of α and α∗, and whose unit we shall denote by ε.
For each w ∈ I we shall denote by L(w) the sup-lattice L⊗(|w|+1), where
|w| is the length of the word w (notice the difference with respect to ¶2.7):
L(ε) = L ,
L(α) = L(α
∗) = L⊗ L ,
L(αα) = L(αα
∗) = L(α
∗α) = L(α
∗α∗) = L⊗ L⊗ L ,
For each w,w′ ∈ I we define a map
ϕw,w′ : L
(w) × L(w
′) → L(ww
ϕw,w′(x1 ⊗ · · · ⊗ xn, y1 ⊗ · · · ⊗ ym) = x1 ⊗ · · · ⊗ (xn ∧ y1)⊗ · · · ⊗ ym .
It is easy to see that this preserves joins in each variable, and thus it defines
a sup-lattice homomorphism
ϕw,w′ : L
(w) ⊗ L(w
′) → L(ww
Defining
T(L) =
(not the same as TL, cf. ¶¶2.7 and 4.2), and using the distributivity of⊗ over
, we obtain the following sup-lattice homomorphism T(L)⊗T(L)→ T(L),
T(L)⊗ T(L)
∼= //
L(w) ⊗ L(w
ϕw,w′ //
// T(L) ,
where the rightmost homomorphism is the copairing of the family of sup-
lattice embeddings L(ww
′) → T(L) which is given by the universal property of
the sup-lattice coproduct
′). Hence, there is a bilinear multiplication
T(L)× T(L)→ T(L). It is defined on pure tensors by
(x1 ⊗ · · · ⊗ xn)(y1 ⊗ · · · ⊗ ym) = x1 ⊗ · · · ⊗ (xn ∧ y1)⊗ · · · ⊗ ym ,
and it is straightforward to see that it is associative, hence giving us a quan-
tale multiplication on T(L). This multiplication has a unit, which coincides
with 1L ∈ L
(ε) = L, and an involution
(−)∗ : T(L)→ T(L)
is obtained from the isomorphisms L(w)
→ L(w
∗) that are given by
x1 ⊗ · · · ⊗ xn 7→ xn ⊗ · · · ⊗ x1 .
Hence, T(L) is a unital involutive quantale, and it is clearly graded over I,
so that we can define:
Definition 5.1 The tensor involutive quantale of L is the graded unital
involutive quantale T(L).
There is an obvious homomorphism of involutive monoids (−) : I → T(L)
that sends each word w to 1L ⊗ · · · ⊗ 1L ∈ L
(w). Hence, in particular,
α = 1L ⊗ 1L ∈ L
(α) and α∗ = 1L ⊗ 1L ∈ L
(α∗).
The quantale T(L) has the following universal property:
Proposition 5.2 Let Q be a unital involutive quantale such that b = b2 = b∗
for all b ∈ ↓eQ (in particular, this implies that ↓eQ is a locale). Let also
h : L→ ↓eQ
be a homomorphism of locales, and let a ∈ Q. Then there is exactly one
homomorphism of unital involutive quantales
ϑ : T(L)→ Q
such that:
1. ϑ(x) = h(x) for all x ∈ L(ε) = L;
2. ϑ(α) = a.
Proof. By the universal property of the coproduct of sup-lattices, every
sup-lattice homomorphism ϑ with domain T(L) is uniquely determined by
its value on the pure tensors of T(L). Furthermore, every pure tensor
x1 ⊗ · · · ⊗ xn ∈ L
with wi = α, α
∗ can be written as a product of xi ∈ L, α ∈ L
α and α∗ ∈ Lα
and thus if ϑ is a homomorphism of unital involutive quantales that satisfies
1 and 2 then its value is uniquely determined on all the pure tensors. This
proves that if ϑ exists then it is unique. In order to prove existence, assign
to each pure tensor
x1 ⊗ · · · ⊗ xn ∈ L
the value h(x1)a1h(x2) . . . an−1h(xn) ∈ Q where ai = a or ai = a
∗ according
to whether wi is α or α
∗, respectively. This assignment preserves joins in
each variable xi separately and thus it defines a sup-lattice homomorphism
ϑw : L
(w) → Q. The copairing
ϑ = [ϑw]w∈I : T(L)→ Q
is easily seen to preserve the quantale multiplication, the unit and the invo-
lution, and it satisfies conditions 1 and 2.
For the following we denote by Frm the full subcategory of Qu whose
objects are the locales (this is usually called the category of frames [5]).
Corollary 5.3 Let Que be the full subcategory of Qu whose objects are those
unital involutive quantales Q such that b = b2 = b∗ for all b ≤ e in Q. Let
also Que∗ be the corresponding category of pointed quantales. There is an
obvious functor Que∗ → Frm that to each quantale Q assigns ↓e, and such
that h 7→ h|↓e for each homomorphism h. This functor has a left adjoint
which to each locale L assigns the pointed quantale (T(L), α).
Bimodal frames and pointed quantales. We have already mentioned
that for an ssq Q, ςQ = ↓e is a locale. It is also clear that, for α in Q, the
operators ♦x = ς(αx) and �x = ς(α∗x) preserve arbitrary joins, hence they
are sup-lattice endomorphisms of ςQ.
Definition 5.4 We say that two sup-lattice endomorphisms of L, ♦ and �,
are conjugate modalities if for all x, y ∈ L we have
♦x ∧ y ≤ ♦(x ∧ �y) ,
�x ∧ y ≤ �(x ∧ ♦y) .
A bimodal frame (L,♦,�) is a frame L equipped with two conjugate modal-
ities ♦ and �.
Proposition 5.5 Let Q be an ssq, and α ∈ Q. Then
(ςQ, ς(α−), ς(α∗−))
is a bimodal frame.
Proof. We only have to check that the two endomorphisms are conjugate
modalities. From the fact that ς is a support (4) we have:
ς(αx)y ≤ αxα∗y ,
and thus
♦x ∧ y = ς(αx)y = ς(ς(αx)y) ≤ ς(αxα∗y) = ς(αxς(α∗y)) = ♦(x ∧ �y) ,
using stability and the fact that x, y ∈ ςQ. The other conjugacy condition is
obtained by interchanging α and α∗.
From now on we shall refer to any sup-lattice endomorphism ς : Q→ Q on
a unital involutive quantale Q such that ςa ≤ e for all a ∈ Q as a pre-support
of Q.
Given a bimodal frame (L,♦,�), a pre-support can be easily defined on
pure tensors of T(L) (and then extended to joins of these in the obvious way):
if x = x0 ⊗ · · · ⊗ xn is in degree w = w1 . . . wn (with wi ∈ {α, α
∗}) then
ςx = x0 ∧ 〈w1〉(x1 ∧ 〈w2〉(. . .)) ,
where 〈wi〉 is ♦ or � according to whether wi = α or wi = α
∗, respectively.
Recursively, we have:
Definition 5.6 Let x = x0 ⊗ · · · ⊗ xn ∈ L
(w1...wn). Then,
• ςx = x, if n = 0;
• ςx = x0 ∧ 〈w1〉(ςx
′), if n ≥ 1, where x′ = x1 ⊗ · · · ⊗ xn ∈ L
(w2...wn).
Lemma 5.7 The following properties hold for all a, b, c ∈ T(L):
1. ςe = e and ςa ≤ e (condition 3 in the definition of support);
2. ς(ςab) = ςaςb (in particular, ςςa = ςa);
3. ς(ab) = ς(aςb) (we say the pre-support ς is stable);
4. If ♦ and � are conjugate we have
(a) ςa ≤ ς(aa∗);
(b) ς(ςab) ≤ ς(aa∗b);
(c) ς(cςab) ≤ ς(caa∗b).
Proof. 1. ς T(L) = L and e is 1L.
2. It suffices to prove this for all the pure tensors b ∈ L(v), where v is an
arbitrary degree. Let
b = y0 ⊗ · · · ⊗ yp ∈ L
(v1...vp) .
We have ςa ∈ L(ε), and thus from ¶5.6 we obtain
ς(ςab) = ς((ςa ∧ y0)⊗ · · · ⊗ yp)
= (ςa ∧ y0) ∧ 〈v1〉(ς(y1 ⊗ · · · ⊗ yp))
= ςa ∧ (y0 ∧ 〈v1〉(ς(y1 ⊗ · · · ⊗ yp)))
= ςaςb .
3. It suffices to prove this for all the pure tensors a ∈ L(w), where w is an
arbitrary degree. Let then
a = x0 ⊗ · · · ⊗ xn ∈ L
(w1...wn) .
The proof is done by induction on n. For the base case assume that
n = 0; that is, we have a = ςa = x0 ∈ L
(ε), and from 2 we obtain
ς(ab) = ς(ςab) = ςaςb = aςb ,
whence ς(ab) = ςς(ab) = ς(aςb).
Now for the induction step let n ≥ 1 and let
a′ = x0 ⊗ · · · ⊗ xn−1 ∈ L
(w1...wn−1) .
We have
a = a′wnxn
and thus
ς(ab) = ς(a′wnxnb)
= ς(a′ς(wnxnb)) (Induction hyp.)
= ς(a′〈wn〉(ς(xnb))) (Def. of ς)
= ς(a′〈wn〉(xnςb)) (By 2)
= ς(a′ς(wnxnςb))) (Def. of ς)
= ς(a′wnxnςb) (Induction hyp.)
= ς(aςb) .
4. First we remark that (4a) is an instance of (4b) (which in turn is an
instance of (4c)). Moreover, (4b) implies (4c) due to stability: if we
assume (4b) then
ς(cςab) = ς(cς(ςab)) ≤ ς(cς(aa∗b)) = ς(caa∗b) .
It now suffices to prove (4b). We shall prove ς(ςab) ≤ ς(aa∗b) for the
particular case where a is a pure tensor
a = x0 ⊗ · · · ⊗ xn
in degree w = w1 . . . wn (n ≥ 1), which implies the general case. The
proof is by induction on n.
Base: for n = 0, we have a = ςa = aa∗, and thus ς(ςab) = ς(aa∗b).
Step: for n ≥ 1, let r be x1 ⊗ · · · ⊗ xn ∈ L
(w2...wn); hence, we have
a = x0w1r, and thus using stability we obtain
ς(aa∗b) = ς(x0w1rr
∗w∗1x0b) = ς(x0w1rr
∗ς(w∗1x0ςb)) .
By the definition of ς (and making the symbol ∧ explicit for the mul-
tiplication in ς T(L)) this equals
x0 ∧ 〈w1〉ς(rr
∗〈w∗1〉(x0 ∧ ςb)) ,
which, by the induction hypothesis, is greater or equal to
x0 ∧ 〈w1〉ς(ςr ∧ 〈w
1〉(x0 ∧ ςb)) ,
which in turn equals
x0 ∧ 〈w1〉(ςr ∧ 〈w
1〉(x0 ∧ ςb))
(because the argument of the outermost occurrence of ς was in ς T(L)).
Finally, by conjugacy of the operators 〈w1〉 and 〈w
1〉 the latter is greater
or equal to
x0 ∧ 〈w1〉(ςr) ∧ x0 ∧ ςb = x0 ∧ 〈w1〉(ςr) ∧ ςb
= ς(x0w1r) ∧ ςb = ςa ∧ ςb = ς(ςab) .
The supported quantale of a bimodal frame. So far we have obtained,
from an arbitrary bimodal frame, a quantale with a stable pre-support. In
order to obtain an actual supported quantale we shall impose the missing
properties, namely ςa ≤ aa∗ (4) and a ≤ ςaa (5), by taking quotients of
T(L).
Definition 5.8 Let jς be the least nucleus j on T(L) such that
j(a) = j(ςaa) .
We define Tς(L,♦,�) to be T(L)jς . We also write Tς(L) if ♦ and � are clear
from the context.
From ¶4.7 it is clear that jς is a graded nucleus, and it is the identity on
L(ε) = L because for all a ∈ L we have ςaa = a. Hence, we have concluded,
just from the graded structure of T(L), that the injection of generators of L
into Tς(L,♦,�) is 1–1.
Proving a similar fact for the other axiom, ςa ≤ aa∗, is less easy, and we
shall address this now. Let (L,♦,�) be a bimodal frame and let
R = {(ςa, aa∗) | a ∈ Tς(L,♦,�)} .
Definition 5.9 TK(L,♦,�) is Tς(L,♦,�)jR. As in ¶5.8 we may write TK(L).
We shall denote the selected point jR(jς(α)) ∈ TK(L) by α.
Lemma 5.10 Recall the definition (2.5) of R. If (y, z) ∈ R then ςy ≤ ςz in
Tς(L,♦,�).
Proof. We have ςy ≤ ςz for all (y, z) ∈ R if and only if the following two
conditions hold for all (y, z) ∈ R and all a, b ∈ Tς(L):
ς(ayb) ≤ ς(azb) (7)
ς(ay∗b) ≤ ς(az∗b) . (8)
In order to prove these two conditions we shall show that they hold for all
(y, z) ∈ R and that they are preserved by the recursive rules of construction
of R.
Let (y, z) ∈ R; that is, let y and z be of the form y = ςt and z = tt∗. We
ς(ayb) = ς(aςtb) ≤ ς(att∗b) = ς(azb) ,
from ¶5.7. We similarly have ς(ay∗b) ≤ ς(az∗b) because y and z are self-
adjoint.
Now assume that (7)–(8) hold for some pair (y, z) ∈ Tς(L) × Tς(L). We
shall prove that they equally hold for the following pairs: (i) (ςy, ςz); (ii)
(y∗, z∗); (iii) (qy, qz); and (iv) (yq, zq), for all q ∈ Tς(L).
(i) Since (y, z) satisfies (7)–(8) we have ςy ≤ ςz (make a = b = 1L), and
thus ς(aςyb) ≤ ς(aςzb) for all a, b ∈ Tς(L), proving (7) for the pair (ςy, ςt).
Since ςy and ςz are self-adjoint, we also conclude (8) for the pair (ςy, ςt).
(ii), (iii) and (iv) are obvious.
Theorem 5.11 The unit of the adjunction L→ TK(L) is 1–1.
Proof. Equivalently, we want to prove that ς Tς(L) ⊂ QjR, or, in other
words, that for all (y, z) ∈ R and x ∈ L we have
z ≤ x⇒ y ≤ x . (9)
Let P ⊂ R be the subset of R consisting of all those (y, z) such that (9) holds
for all x ∈ L. We shall prove that R ⊂ P and that P is closed under the
recursive formation rules of R, hence showing that P = R because R is the
least subset of Tς(L)× Tς(L) satisfying these conditions.
Let (ςy, yy∗) ∈ R. If x ∈ L and yy∗ ≤ x we conclude that y = ςy = yy∗ ∈
L due to the grading of Tς(L) over the free involutive monoid I, and thus
ςy ≤ x, showing that R ⊂ P .
From now on let (y, z) be a fixed but arbitrary element of P . By ¶5.10 we
conclude ςy ≤ ςz. Hence, (9) holds for the pair (ςy, ςz), and thus (ςy, ςz) ∈ P .
Now let q ∈ Tς(L) and assume that qz ≤ x for some x ∈ L. Then z ≤ 1L
(again due to the grading over I), and thus y ≤ 1L because (y, z) ∈ P (make
x = 1L). Hence, again using the previous lemma we obtain
qy = qςy ≤ qςz = qz ≤ x ,
showing that (qy, qz) ∈ P . In a similar way we conclude that (yq, zq) ∈ P .
Finally, x ≤ 1L implies that x is self-adjoint, and thus the conditions y
∗ ≤ x
and z∗ ≤ x are equivalent to y ≤ x and z ≤ x, respectively, showing that
(y∗, z∗) ∈ P .
T, K4, S4, S5. Now let us extend our results to the systems of modal
logic T, K4, S4, and S5. As was explained in §3, we shall need to impose
additional conditions on the selected element α ∈ TK, such as reflexivity
(α ≥ 1L), transitivity (α
2 ≤ α), etc. In order to obtain again coreflections
we shall also have to impose additional axioms on the modalities ♦ and � of
L. As we mentioned in §1, we shall see that for T, K4 and S4 these coincide
with the well known axioms for the corresponding systems of modal logic
under consideration (in other words, the same axioms still produce complete
axiomatizations for the new semantics), whereas for S5 a new axiomatization
is defined just by imposing that ♦ should coincide with �.
The proof techniques are very similar to those employed in the previous
sections for the system K. In fact we could have already presented the theory
for K in such a generality so as to be able to directly reuse the results now,
but this would have obscured the main ideas, so for the sake of clarity we
shall single out the general results only now.
Lemma 5.12 Let ρ ⊂ Tς(L) × Tς(L) be any binary relation on Tς(L), and
let ρ be the closure of ρ under the rules
(y, z) ∈ ρ ⇒ (ςy, ςz) ∈ ρ
(y, z) ∈ ρ ⇒ (ayb, azb) ∈ ρ for all a, b ∈ Tς(L)
(y, z) ∈ ρ ⇒ (y∗, z∗) ∈ ρ .
Assume that for all (y, z) ∈ ρ and all a, b ∈ Tς(L) we have
ς(ayb) ≤ ς(azb)
ς(ay∗b) ≤ ς(az∗b) .
Then for all (y, z) ∈ ρ we have ςy ≤ ςz.
Proof. This follows from a simple adaptation of the proof of ¶5.10.
Lemma 5.13 Let P ⊂ Tς(L)×Tς(L) be the set of all those (y, z) satisfying
the following two conditions:
1. ςy ≤ ςz;
2. z ≤ x⇒ y ≤ x for all x ∈ L.
Then P is closed under the rules
(y, z) ∈ P ⇒ (ςy, ςz) ∈ P
(y, z) ∈ P ⇒ (ayb, azb) ∈ P for all a, b ∈ Tς(L)
(y, z) ∈ P ⇒ (y∗, z∗) ∈ P .
Proof. The proof of this lemma is contained in the proof of ¶5.11, where P
was defined to be a subset of R, but in fact the only property of R used in
order to prove the closure properties of P was the fact that for all (y, z) ∈ R
we have ςy ≤ ςz. The other key ingredient is the fact that ab ∈ L implies
a, b ∈ L for all a, b ∈ Tς(L), due to the grading of Tς(L) over I.
Theorem 5.14 Let ρ ⊂ Tς(L)×Tς(L) be a binary relation such that for all
(y, z) ∈ ρ and all a, b ∈ Tς(L) we have
ς(ayb) ≤ ς(azb) (10)
ς(ay∗b) ≤ ς(az∗b) , (11)
and let Q be the (supported) quotient of Tς(L) generated by ρ. Then the
injection of generators of L onto ςQ,
η : L→ ς Tς(L)→ ςQ ,
is an isomorphism.
Proof. This is an immediate consequence of the previous two lemmas, by a
reasoning analogous to that of ¶5.11.
Similarly to what we have done in §3 for the Lindenbaum quantales QT,
QK4, etc. (see ¶3.5), we define TT(L), TK4(L),TS4(L) and TS5(L) to be quo-
tients of TK(L) by analogous defining relations:
TT(L): e ≤ α
TK4(L): αα ≤ α
TS4(L): e ≤ α ≥ αα
TS5(L): e ≤ α = α
∗ ≥ αα
Corollary 5.15 Let L be a bimodal frame such that for all x ∈ L the condi-
tions x ≤ ♦x and x ≤ �x hold. Then the injection of generators L→ ς TT(L)
is an isomorphism.
Proof. The quantale TT(L) is the quotient of Tς(L) generated by the con-
ditions
ςa ≤ aa∗, for all a ∈ Tς(L) ,
α ≥ e .
Define RT ⊂ Tς(L)× Tς(L) as follows:
RT = {(ςy, yy
∗) | y ∈ Tς(L)}) ∪ {(1L,α)} .
All we have to do is, by the previous theorem, prove that for all (y, z) ∈ RT
the conditions (10)–(11) are satisfied for all a, b ∈ Tς(L). This has already
been done for the pairs of the form (ςy, yy∗) in ¶5.10, so we only have to
concern ourselves with the pair (1L,α). For a, b ∈ Q we have
ς(ab) = ς(aς(b)) ≤ ς(a♦(ς(b))) = ς(aς(αb)) = ς(aαb) ,
where we have used stability of ς twice and the inequality follows from x ≤ ♦x
and monotonicity of ς; this proves (10). Then (11) is proved in a similar way
using the inequality x ≤ �x.
Corollary 5.16 Let L be a bimodal frame such that for all x ∈ L the condi-
tions ♦♦(x) ≤ ♦(x) and ��(x) ≤ �(x) hold. Then the injection of generators
L→ TK4(L) is an isomorphism.
Proof. It remains to prove that the pair (y, z) = (α2,α) satisfies (10)–(11).
The first condition is proved as follows:
ς(aαb) = ς(aς(αb)) = ς(a♦(ς(b))) ≥ ς(a♦2(ς(b))) = ς(aα2b) .
(11) is proved in the same way once we replace α by α∗ and ♦ by � in the
previous argument.
Corollary 5.17 Let L be a bimodal frame such that for all x ∈ L the con-
ditions x ≤ ♦x, x ≤ �x, ♦♦(x) ≤ ♦(x) and ��(x) ≤ �(x) hold. Then the
injection of generators L→ TS4(L) is an isomorphism.
Proof. Immediate from the previous two corollaries.
Corollary 5.18 Let L be a bimodal frame such that for all x ∈ L the con-
ditions of the previous corollary and ♦x = �x hold. Then the injection of
generators L→ TS5(L) is an isomorphism.
Proof. It remains to show that the pairs (α,α∗) and (α∗,α) satisfy (10)
and (11), which is done as follows:
ς(aαb) = ς(aς(αb)) = ς(a♦(ς(b))) = ς(a�(ς(b))) = ς(aα∗b) .
The Lindenbaum quantales. Let BK be the Lindenbaum algebra for
system K, as in §3, and let BT, BK4, BS4, and BS5 be the Lindenbaum
algebras for systems T, K4, S4, and S5, respectively. These are modal lattices
in the following sense:
Definition 5.19 By a modal lattice is meant a bounded distributive lattice
L equipped with an endomap ♦ that preserves finite joins. A bimodal lattice
is a modal lattice equipped with another endomap � that preserves finite
joins and in addition satisfies conjugacy relations similar to those of bimodal
frames:
♦x ∧ y ≤ ♦(x ∧ �y) ,
�x ∧ y ≤ �(x ∧ ♦y) .
The category Lat♦ of modal lattices has the modal lattices as objects and
the homomorphisms of bounded lattices that preserve ♦ as morphisms. The
category Lat♦� of bimodal lattices is defined analogously, with objects being
the bimodal lattices and the morphisms being the homomorphisms of modal
lattices that also preserve �.
We shall also refer to a modal lattice as a
• T-modal lattice if x ≤ ♦x for all x;
• K4-modal lattice if ♦♦x ≤ ♦x for all x;
• S4-modal lattice if it is both a T-modal lattice and a K4-modal lattice;
• S5-modal lattice if it is an S4-modal lattice and ♦x∧ y ≤ ♦(x∧♦y) for
all x and y (i.e., ♦ is conjugate to itself).
The categories Lat♦T, Lat
K4, Lat
S4, and Lat
S5 are, respectively, the full sub-
categories of Lat♦ whose objects are the T-modal lattices, the K4-modal
lattices, the S4-modal lattices, and the S5-modal lattices.
For bimodal lattices we adopt a similar terminology: a bimodal lattice is
referred to as a
• T-bimodal lattice if x ≤ ♦x and x ≤ �x for all x;
• K4-bimodal lattice if ♦♦x ≤ ♦x and ��x ≤ �x for all x;
• S4-bimodal lattice if it is both a T-bimodal lattice and a K4-bimodal
lattice;
• S5-bimodal lattice if it is an S4-bimodal lattice and ♦x = �x for all x.
The categories Lat♦�T , Lat
K4, Lat
S4 , and Lat
S5 are, respectively, the full
subcategories of Lat♦� whose objects are the T-bimodal lattices, the K4-
bimodal lattices, the S4-bimodal lattices, and the S5-bimodal lattices.
By standard universal algebra the forgetful functor Lat♦� → Lat♦ has a
left adjoint which assigns to BK its “enveloping” bimodal lattice B
K. Simi-
larly, there are left adjoints
Lat♦T → Lat
Lat♦K4 → Lat
Lat♦S4 → Lat
and we write B′T, B
K4, and B
S4 for the respective images of BT, BK4, and
BS4 under the left adjoints. For S5 the situation is simpler because the
categories Lat♦S5 and Lat
S5 are obviously isomorphic, since any S5-modal
lattice becomes an S5-bimodal lattice just by defining � to coincide with ♦.
We shall also write B′S5 for BS5 thus regarded as a bimodal lattice.
Since ♦ and � preserve finite joins they can be extended canonically to
sup-lattice endomorphisms of the ideal completion Idl(B′K), which is a frame
because B′K is a distributive lattice. The conjugation relations are easily
seen to be inherited from those of B′K, and thus Idl(B
K) is a bimodal frame.
Similar remarks apply to the other Lindenbaum algebras, and in addition
Idl(B′T) satisfies the axioms of a T-bimodal lattice, Idl(B
K4) satisfies the
axioms of a K4-bimodal lattice, etc. (Hence, in particular, the propositions
in ¶¶5.15–5.18 can be applied to Idl(B′T), Idl(B
K4), Idl(B
S4), and Idl(B
respectively.)
Summarizing, we have described a way of constructing functors from
modal lattices to bimodal frames which are left adjoint to the obvious forget-
ful functors. Composing these functors with the left adjoints from bimodal
frames to pointed ssqs we obtain fromBK, BT, BK4, BS4, andBS5 pointed ssqs
TK(Idl(B
K)), TT(Idl(B
T)), TK4(Idl(B
K4)), TS4(Idl(B
S4)), and TS5(Idl(B
S5)),
respectively. For each system S ∈ {K,T,K4, S4, S5} the map obtained by
composing the following arrows (the leftmost one is just the natural quo-
tient),
BK → BS → B
S → Idl(B
S)→ TS(B
has the same universal property as the injection of generators BK → QS.
Hence, the quantale TS(B
S) is a particular construction of the Lindenbaum
quantale QS:
Theorem 5.20
∼= TK(Idl(B
∼= TT(Idl(B
∼= TK4(Idl(B
∼= TS4(Idl(B
∼= TS5(Idl(B
Since, as we have remarked above, S5-modal lattices and S5-bimodal
lattices are “the same”, our results immediately tell us that the unit of the
adjunction between S5-modal lattices and pointed ssqs,
BS5 → QS5 ,
is a monomorphism. In logical terms this means that a complete axiomati-
zation for the system S5 (with the advantage of making no use of negation
or the modal necessity operator) can be as follows:
Theorem 5.21 S5 is complete for the following axiom schemata:
ϕ → ♦ϕ
♦♦ϕ → ♦ϕ
♦ϕ ∧ ψ → ♦(ϕ ∧ ♦ψ) .
We have not verified whether the remaining canonical mappings
BK → B
BT → B
BK4 → B
BS4 → B
are monomorphisms (although we believe they are). This means that we
have not verified completeness for the classical axiomatizations of K, T, K4,
and S4. Of course, by this we mean we have not verified this in an arbitrary
topos, for otherwise we know, from the classical completeness theorems of
propositional normal modal logic, that the axiomatizations are complete:
using Zorn’s Lemma we can find a Kripke structure (W,R) that gives us a
monomorphism
BK → B
K → TK(Idl(B
∼= QK → ℘(W ×W )
implying that BK → B
K is 1–1, and the same applies to T, K4, and S4.
References
[1] D. Harel, D. Kozen, J. Tiuryn, Dynamic Logic, MIT Press, 2000.
[2] E.A. Emerson, Temporal and modal logic, in J. van Leeuwen (editor),
Handbook of Theoretical Computer Science, vol. B, MIT Press, 1990,
pp. 955–1072.
[3] G.E. Hughes, M.J. Cresswell, An Introduction to Modal Logic, Methuen
& Co. Ltd., London, 1968.
[4] G.E. Hughes, M.J. Cresswell, A Companion to Modal Logic, Methuen
& Co. Ltd., London, 1984.
[5] P.T. Johnstone, Stone Spaces, Cambridge Stud. Adv. Math., vol. 3,
Cambridge Univ. Press, 1982.
[6] A. Joyal, M. Tierney, An Extension of the Galois Theory of
Grothendieck, Mem. Amer. Math. Soc., vol. 309, American Mathemat-
ical Society, 1984.
[7] M.V. Lawson, Inverse Semigroups — The Theory of Partial Symmetries,
World Scientific, 1998.
[8] I. Moerdijk, J. Mrčun, Introduction to Foliations and Lie Groupoids,
Cambridge University Press, 2003.
[9] C.J. Mulvey, Quantales, in M. Hazewinkel (editor), The Encyclopaedia
of Mathematics, third supplement, Kluwer Academic Publishers, 2002,
pp. 312–314.
[10] C.J. Mulvey, P. Resende, A noncommutative theory of Penrose tilings,
Internat. J. Theoret. Phys. 44 (2005) 655–689.
[11] J. Paseka, J. Rosický, Quantales, in B. Coecke, D. Moore, A. Wilce,
(editors), Current Research in Operational Quantum Logic: Algebras,
Categories and Languages, Fund. Theories Phys., vol. 111, Kluwer Aca-
demic Publishers, 2000, pp. 245–262.
[12] A.L.T. Paterson, Groupoids, Inverse Semigroups, and Their Operator
Algebras, Birkhäuser, 1999.
[13] P. Resende, Tropological systems are points of quantales, J. Pure Appl.
Algebra 173 (2002) 87–120.
[14] P. Resende, Étale groupoids and their quantales, Adv. Math. 208 (2007)
147–209.
[15] K. Rosenthal, Quantales and Their Applications, Pitman Research
Notes in Mathematics Series 234, Longman Scientific & Technical, 1990.
Centro de Lógica e Computação
Instituto Superior Técnico
Universidade Técnica de Lisboa
Av. Rovisco Pais 1, 1049-001 Lisboa, Portugal
E-mail: sergiortm@gmail.com
Centro de Análise Matemática, Geometria e Sistemas Dinâmicos
Departamento de Matemática do Instituto Superior Técnico
Universidade Técnica de Lisboa
Av. Rovisco Pais 1, 1049-001 Lisboa, Portugal
E-mail: pmr@math.ist.utl.pt
	Introduction
	Preliminaries
	Quantale semantics of modal logic
	Graded unital involutive quantales
	Construction of the Lindenbaum quantales

  The Kripke semantics of classical propositional normal modal logic is made
algebraic via an embedding of Kripke structures into the larger class of
pointed stably supported quantales. This algebraic semantics subsumes the
traditional algebraic semantics based on lattices with unary operators, and it
suggests natural interpretations of modal logic, of possible interest in the
applications, in structures that arise in geometry and analysis, such as
foliated manifolds and operator algebras, via topological groupoids and inverse
semigroups. We study completeness properties of the quantale based semantics
for the systems K, T, K4, S4, and S5, in particular obtaining an axiomatization
for S5 which does not use negation or the modal necessity operator. As
additional examples we describe intuitionistic propositional modal logic, the
logic of programs PDL, and the ramified temporal logic CTL.

Introduction
It is well known that the set ℘(W × W ) of all the binary relations on a
set W has the structure of a unital involutive quantale (see §2). Hence, a
Kripke structure (W,R) as it appears in the semantics of propositional normal
modal logic [3, 4], where W is the set of possible worlds and R ⊂W ×W is
the accessibility relation, can be regarded as an example of a pointed unital
involutive quantale (℘(W ×W ), R). This suggests a way of generalizing the
notion of Kripke structure, namely in terms of a more general pointed unital
involutive quantale (Q,α), and the purpose of this paper is to assess the
usefulness of this idea with respect to the semantics of modal logic.
∗Research supported in part by Fundação para a Ciência e a Tecnologia through pro-
gram POCI 2010/FEDER and project POCI/MAT/55958/2004.
http://arxiv.org/abs/0704.1886v1
Not every unital involutive quantale is suitable for this purpose, and in
this paper we restrict to the notion of stably supported quantale that has
been introduced in [14]. In order to motivate this let us consider again the
quantale ℘(W ×W ) of binary relations on W . Each relation R ⊂ W ×W
has a domain dom(R) = {x ∈ W | ∃y (x, y) ∈ R} and, since the diagonal
relation
∆W = {(x, y) ∈ W ×W | x = y}
is of course isomorphic to W , we can equivalently replace the domain of R
by the set
ςR = {(x, x) ∈ ∆W | x ∈ dom(R)} ,
which we refer to as the support of R. This defines an operation
ς : ℘(W ×W )→ ℘(W ×W )
that preserves unions and in addition satisfies the following properties, for
all R, S ⊂W ×W :
ςR ⊂ ∆W
ςR ⊂ RR∗
R ⊂ ςRR
ς(RS) ⊂ ςR
A stably supported quantale, or simply ssq, is defined to be a unital involutive
quantale Q equipped with a sup-lattice endomorphism ς : Q → Q which
satisfies these properties; that is, for all a, b ∈ Q we have
ςa ≤ e
ςa ≤ aa∗
a ≤ ςa a
ς(ab) ≤ ςa
For each a ∈ Q the element ςa is called the support of a, the operation ς itself
is referred to as the support of Q, and the set ςQ = {ςa | a ∈ Q} is necessarily
a locale whose binary meet operation coincides with the multiplication of the
quantale: a∧b = ab. For instance, if Q = ℘(W×W ) we have ςQ = ℘(∆W ) ∼=
℘(W ).
The formulas of propositional modal logic can be easily interpreted on
any pointed ssq (Q,α): there should be a valuation map v assigning to each
formula ϕ an element v(ϕ) ∈ ςQ. The properties that such a map must
satisfy are clear. For instance, conjunction of formulas should be interpreted
as multiplication in Q: v(ϕ∧ψ) = v(ϕ)v(ψ); and the remaining propositional
connectives are equally straightforward, both classically and intuitionistically
(see §3). As regards the modal operator ♦ of possibility, we impose
v(♦ϕ) = ς(αv(ϕ)) .
This is easily seen to yield the usual interpretation on Kripke structures:
v(♦ϕ) corresponds to the domain of the relation αv(ϕ), where α is the ac-
cessibility relation.
Algebraic semantics. If (Q,α) is a pointed ssq then ςQ becomes a locale
equipped with unary operators in a natural way (§§3, 5), and it will be seen
in this paper that from any such locale it is possible to obtain a pointed ssq,
in fact giving us an adjunction between two categories, and generalizing the
way in which a binary relation on W (i.e., an accessibility relation) corre-
sponds classically to a unary operator ♦ : ℘(W ) → ℘(W ). This leads to a
semantics that subsumes the classical algebraic semantics based on lattices
with operators.
The systems of modal logic that are characterized by special kinds of
accessibility relations can be characterized by subcategories of the category
StabQu∗ of pointed ssqs. For instance, the system S5, which is characterized
by accessibility being an equivalence relation, will correspond to the full
subcategory of StabQu∗ whose objects (Q,α) are those satisfying α
2 = α∗ =
α ≥ e. Moreover, it is easy to address multi-modal logics, such as dynamic
logic, logics of time and space, etc., in terms of the category whose objects
are ssqs equipped with more than one point, the various points satisfying
suitable relations.
The category StabQu of ssqs has pleasant properties [14]. For instance,
there is at most one support on any unital involutive quantale, and any
homomorphism of unital involutive quantales h : Q → Q′ between ssqs Q
and Q′ automatically preserves the support (hence, being stably supported
is a property rather than extra structure). The category StabQu is therefore
a full subcategory of the category of unital involutive quantales, and in fact
it is reflective. There are presentations of ssqs by generators and relations,
which play the role of “Lindenbaum algebras” in the context of the quantale-
based semantics. For instance, the “Lindenbaum quantale” for S5 is the
pointed ssq QS5 generated by the usual Lindenbaum algebra of S5 (with
defining relations ensuring that it is a bounded sublattice of ς QS5) with the
distinguished point α ∈ QS5 being subject to the relations α
2 = α∗ = α ≥ e.
The usual Kripke structure based models for S5 can be identified with the
relational representations of QS5, in other words the homomorphisms
h : QS5 → ℘(W ×W )
of unital involutive quantales (see [10] for some properties of such representa-
tions). The same identification of models with the relational representations
of a quantale applies to many other well known examples of modal logics.
Groupoids and inverse semigroups. An important aspect of the se-
mantics described in this paper is that there are plenty of examples of ssqs
besides the quantales of binary relations [14], arising from various geomet-
ric or analytic structures, and thus we are provided with a uniform way of
defining semantic interpretations of propositional normal modal logic based
on such structures. More precisely, let G be a groupoid (i.e., a small category
all of whose arrows are isomorphisms). Writing G also for the set of groupoid
arrows, ℘(G) is an ssq; the quantales of binary relations ℘(W ×W ) are pre-
cisely the quantales that arise from the so-called pair groupoid of W , which
hasW as set of objects andW ×W as set of arrows, with the two projections
W ×W → W being the domain and codomain maps of the groupoid. Even
more generally, the topology Ω(G) of any topological étale groupoid G is a
sub-ssq of ℘(G); and for localic étale groupoids, too, there is an ssq O(G)
associated to each groupoid G.
These facts are a part of the close relation [14] between the notions of étale
groupoid (either topological or localic), inverse semigroup, and quantale,
which can be summarized in the following diagram whose arrows denote
bijections of objects up to isomorphism, or even, in the case of I and L∨,
equivalences of categories:
Inverse
quantal
frames
Étale
groupoids bisections
Complete
infinitely
distributive
inverse
semigroups
germspp
The inverse quantal frames are the ssqs that arise from étale groupoids.
It follows that the quantale semantics automatically provides a bridge
between modal logic and those areas of mathematics where examples of étale
groupoids and inverse semigroups occur, such as operator algebras and dif-
ferential topology — see, e.g., [7, 8, 12]. As an example of the latter, foliated
manifolds can be associated to dynamical systems, and from a foliation it is
always possible to construct a topological étale groupoid [8]. We shall not
deal with any such examples in this paper, but we mention that if we replace
℘(W ×W ) by a more general groupoid quantale, hence taking as models
of propositional modal logic the homomorphisms Q → Ω(G) or Q → O(G)
instead of Q → ℘(W ×W ) (where Q is a Lindenbaum quantale), we are
led in a natural way to semantics which may be interesting, say, for applied
logicians or computer scientists dealing with hybrid systems, logics of real
time and space, etc.
Overview. Let (Q,α) be a pointed ssq. Then the locale ςQ is canonically
equipped with the two unary sup-latice endomorphisms ♦ and � defined by,
for each x ∈ ςQ,
♦x = ς(αx) (1)
�x = ς(α∗x) , (2)
which are easily seen to satisfy the following conjugacy conditions (see §5):
♦x ∧ y ≤ ♦(x ∧ �y)
�x ∧ y ≤ �(x ∧ ♦y) .
Such a structure (L,♦,�), where L is a locale and ♦ and � satisfy the
conjugacy conditions, will be called a bimodal frame, and there is a functor
from the category of pointed ssqs to the obvious category of bimodal frames.
A functor in the opposite direction can be easily obtained just from the
knowledge that ssqs can be presented by generators and relations; given a bi-
modal frame (L,♦,�) its associated quantale Q is generated by the elements
of L plus an element α, with relations imposing both that L is a unital invo-
lutive subquantale of Q and that (1) and (2) are satisfied. As we shall see,
this defines a functor which is left adjoint to ς, and in fact it is a coreflection;
hence, we always have an isomorphism of bimodal frames L ∼= ςQ.
We can interpret this isomorphism in a logical sense as saying that no
theorems are added in the process of interpreting ♦ and � in terms of the
quantale operations. Hence, if we think of the addition of the quantale
operations as a language extension then this extension is conservative — the
conjugacy conditions are a complete axiomatization for the modal operators
induced by α and α∗.
This of course suggests looking at several systems of modal logic and their
completeness theorems, which we shall do for K, T, K4, and S4, showing that
the usual conditions on ♦ (and here also on �), as taken from the standard
completeness theorems of modal logic, are precisely what is required for a
coreflection to be obtained when the pointed ssqs (Q,α) under consideration
satisfy the expected conditions, such as “reflexivity”, “transitivity”, etc., of
the point α. Hence, the theorems which we prove in this paper can be re-
garded as an algebraic generalization of the standard completeness theorems
for these systems of propositional normal modal logic. It is worth noting
that, as opposed to the classical theorems, these are now independent of the
axiom of choice (which is required in the proof of the classical theorems,
in the form of Zorn’s lemma). From our results we also obtain a complete
axiomatization of system S5, where to the axioms of S4 one adds the axiom
scheme
♦ϕ ∧ ψ → ♦(ϕ ∧ ♦ψ) .
This is obtained from the conjugacy conditions by making ♦ = � and, as
opposed to the usual axiom scheme ϕ→ �♦ϕ, it does not mention negation
or the modal necessity operator.
The remainder of this paper goes as follows. In §2 we provide some nec-
essary background and preliminary results on quantales, presentations by
generators and relations, etc. Then in §3 we describe in detail the quantale-
based semantics of propositional normal modal logic, including the systems
K, T, K4, S4, and S5. In order to illustrate the flexibility of this approach we
provide additional examples, namely propositional intuitionistic logic, propo-
sitional dynamic logic, and the ramified temporal logic CTL. Finally, after
some technical results in §4 about graded quantales (the quantale analogue
of graded rings), in §5 we address the adjunctions mentioned above. The
mere existence of the adjunctions is a consequence of the existence of pre-
sentations by generators and relations; in other words, it can be phrased in
terms of the existence of the Lindenbaum quantales. However, in order to
obtain additional information about the adjunctions and, in particular, in
order to prove that they are coreflections, we shall need an actual construc-
tion of the Lindenbaum quantales. This will be conveniently formulated in
terms of “tensor algebras” over bimodal frames, and it will take up most of
2 Preliminaries
Here we describe some background on sup-lattices, locales and quantales.
General references are [5, 6, 9, 11, 15].
Sup-lattices. We shall denote the category of sup-lattices by SL. The
objects are the complete lattices and the morphisms are the maps f : L→M
that preserve arbitrary joins: for all X ⊂ L
f(x) .
We shall write 1L or simply 1 for the lattice unit (the greatest element) of a
sup-lattice L, and 0L or simply 0 for the least element.
Let (Li) be a family of sup-lattices. Their cartesian product
Li is a
sup-lattice with pointwise order and joins, and it is a product in the category
SL. The products and the coproducts are isomorphic [6], similarly to abelian
groups (but, contrary to the latter, also in the case of infinitary coproducts).
We denote by
Li the categorical coproduct of a set-indexed family of
sup-lattices (Li), and call it direct sum.
The tensor product of L and M is denoted by L ⊗M , and similarly to
vector spaces, it is the image of a universal bi-morphism, where a sup-lattice
bi-morphism f : L ×M → N is a map that preserves joins in each variable
separately:
f(x, y)
f(x, y) .
Concretely, L⊗M can be identified with the set of those subsets I ⊂ L×M
such that
∈ I ⇐⇒ {x} × Y ⊂ I
∈ I ⇐⇒ X × {y} ⊂ I
for all x ∈ L, y ∈ M , X ⊂ L, and Y ⊂ M . The universal bi-morphism
L×M → L⊗M is defined by (x, y) 7→ x⊗ y, where x⊗ y is the least such
set that contains the pair (x, y), which is called the pure tensor generated by
(x, y). SL is a monoidal category with respect to this tensor product, with
the powerset ℘( 1) of the singleton set as the tensor unit. Similarly to the
category of abelian groups, the functor hom(N,−) has a left adjoint −⊗N
for each N ; that is, we have the familiar isomorphism
hom(M ⊗N,L) ∼= hom(M, hom(N,L)) ,
natural in the variables M and L, which in fact is an order isomorphism. As
a consequence of colimit preservation by left adjoints, ⊗ distributes over
Mi) ∼=
(L⊗Mi) .
Quotients of sup-lattices can be conveniently handled by means of closure
operators (monotone endomaps j that satisfy a ≤ j(a) and j(j(a)) = j(a)
for every element a). Let L be a sup-lattice and j a closure operator on L.
The set of j-closed elements
Lj = {x ∈ Q | x = j(x)}
is a sup-lattice closed under the formation of meets in L, with joins given by
(xi) = j(
xi), and the map j : L → Lj is a (surjective) homomorphism
of sup-lattices. Conversely, given a set S ⊂ L closed under meets in L, we
obtain a closure operator jS : L→ L by
jS(x) =
{y ∈ S | x ≤ y} .
These constructions are mutually inverse,
jLj = j LjS = S ,
and every sup-lattice quotient arises in this way up to isomorphism.
The relation to the usual description of quotients by means of congruence
relations (i.e., equivalence relations on L which are sub-sup-latttices of L×L)
is the following: from a closure operator j we obtain the congruence relation
θj ⊂ L× L defined by
(x, y) ∈ θj ⇐⇒ j(x) = j(y)
[in particular (x, j(x)) ∈ θj ] and from a congruence relation θ ⊂ L × L we
define a closure operator jθ by
jθ(x) =
where [x]θ is the congruence class of x; of course, we have jθj = j and θjθ = θ.
Stably supported quantales. A quantale is a sup-lattice equipped with
an associative multiplication, usually written (a, b) 7→ ab, which distributes
over arbitrary joins:
(abi) ,
(aib) .
Hence, a quantale is a semigroup in SL. A quantale Q is unital if the multi-
plication has a unit, which we denote by eQ, or simply e.
Example 2.1 A locale, or frame, L is a sup-lattice satisfying the following
distributivity property for all x ∈ L and Y ⊂ L:
x ∧ y .
Hence, a locale is a unital quantale whose multiplication is ∧ and whose
unit e coincides with 1. In particular, it is a commutative and idempotent
quantale. A quantale is a locale if and only if it is unital with e = 1 and it
is idempotent [6].
An involutive quantale Q is a quantale equipped with an involution
(−)∗ : Q→ Q ,
i.e., a join preserving operation that makes Q an involutive semigroup:
(ab)∗ = b∗a∗,
a∗∗ = a.
Any involutive quantale satisfies 1∗ = 1 and, if it is unital, e∗ = e.
Hence, a unital involutive quantale is an involutive monoid
℘( 1)
←− Q⊗Q
in the monoidal category of sup-lattices, with ab = m(a⊗ b).
Definition 2.2 Let Q be a unital involutive quantale. A support on Q is a
sup-lattice endomorphism ς : Q→ Q satisfying, for all a ∈ Q:
ςa ≤ e , (3)
ςa ≤ aa∗ , (4)
a ≤ ςaa . (5)
A supported quantale is a unital involutive quantale equipped with a spec-
ified support. On a supported quantale the set of supports ςQ coincides with
↓e = {x | x ≤ e} and it is a locale with ab = a ∧ b [14].
Definition 2.3 A support is stable if it satisfies ς(ab) = ς(aς(b)). A quantale
equipped with a specified stable support is stably supported, or simply an ssq.
Every homomorphism of unital involutive quantales preserves the support
of an ssq, and thus the category of ssqs, StabQu, is defined to be the full
subcategory of the category of unital involutive quantales Qu whose objects
are the ssqs. Moreover, if a quantale is stably supported then it can have
no other support, stable or not [14]. Hence, being stably supported should
be regarded as a property of unital involutive quantales rather than extra
structure. In [14] it has also been seen that the inclusion functor StabQu →
Qu has a left adjoint (i.e., StabQu is a reflective subcategory of Qu).
Any locale is an ssq with trivial involution and support:
x∗ = x ςx = x .
Nuclei and quotients. The quotients of ssqs are described in a similar
way to those of sup-lattices. We give here an overview and refer to [14] for
further details.
Definition 2.4 A (quantic) nucleus on an ssq Q is a closure operator
j : Q→ Q
that satisfies, for all x, y ∈ Q,
j(x)j(y) ≤ j(xy) ,
j(x)∗ ≤ j(x∗) ,
ς(j(x)) ≤ j(ς(x)) .
We remark that the second condition is equivalent to j(x)∗ = j(x∗).
The set of j-closed elements Qj = {x ∈ Q | x = j(x)} is an ssq with
joins
(xi) = j(
xi), multiplication x · y = j(xy), with the same involution
as Q, and support δx = j(ςx). The map j : Q → Qj is a (surjective)
homomorphism of ssqs:
j(xi)
j(xy) = j(x) · j(y)
j(x∗) = j(x)∗
j(ςx) = δx .
Furthermore, every quotient arises in this way up to isomorphism.
The set N(Q) of nuclei is a complete lattice under the pointwise order,
with meets being calculate pointwise: j ≤ k ⇔ ∀x∈Q(j(x) ≤ k(x)), and
jα(x) =
(jα(x)). Furthermore, we have j ≤ k ⇔ Qk ⊂ Qj, and
the join of nuclei corresponds to intersection of the respective sets of closed
elements: j =
jα if and only if Qj =
Qjα .
Definition 2.5 Let Q be an ssq, and R ⊂ Q×Q. The supported closure R
of the binary relation R is the smallest relation that contains R and is closed
for the quantale operations, i.e.:
R ⊂ R ;
(y, z) ∈ R ⇒ (ay, az) ∈ R, for all a ∈ Q ;
(y, z) ∈ R ⇒ (ya, za) ∈ R, for all a ∈ Q ;
(y, z) ∈ R ⇒ (ςy, ςz) ∈ R ;
(y, z) ∈ R ⇒ (y∗, z∗) ∈ R .
Contrarily to what is done in [13], we shall interpret each pair (y, z) ∈ R
as an inequality y ≤ z, rather than an equation y = z. It is easy to see that
there is a least quantic nucleus j such that j(y) ≤ j(z) for all (y, z) ∈ R:
{j ∈ N(Q) | j(y) ≤ j(z) for all (y, z) ∈ R}.
Analogously to the quotients of involutive quantales described in [13], the
quantale QjR has a very simple description:
QjR = {x ∈ Q | ∀(y,z)∈R (z ≤ x⇒ y ≤ x)}.
We stress that nuclei and quotients of unital involutive quantales equipped
with any sup-lattice endomorphism ς : Q → Q are handled in exactly the
same way as described above for ssqs (we shall use this in §5 when dealing
with quantales that are just “pre-supported”). The properties of ς pass to
the quotients one by one: if j is a nucleus on Q and δ : Qj → Qj is the
sup-lattice endomorphism defined by δ(a) = j(ςa), then if, say, the equation
ς(ab) = ς(aςb) holds in Q then δ(ab) = δ(aδb) holds in Qj , etc.
Generators and relations. Let G be a set (of “generators”). The con-
struction of the unital involutive quantale Qu〈G〉 freely generated by G is
described in [13]. Denoting by F : Qu → StabQu the left adjoint to the
inclusion StabQu → Qu (cf. paragraph after ¶2.3), it follows that F (Qu〈G〉)
is the free ssq generated by G, and we shall denote it by StabQu〈G〉.
Definition 2.6 Let G and R ⊂ StabQu〈G〉 × StabQu〈G〉 be sets. The ssq
presented by the generators in G and the relations in R is
StabQu〈G | R〉
= StabQu〈G〉
If x ∈ G, one denotes by [x] the image of the generator x in the quantale
being presented. This notation provides a useful way of describing the defin-
ing relations of a quantale presentation: we just write the conditions with
respect to which the injection of generators is universal, as in the following
example for unital involutive quantales.
Example 2.7 Let L be a sup-lattice. It follows from the universal proper-
ties of the tensor product and the direct sum of sup-lattices that the unital
involutive quantale freely generated by L with joins being preserved in the
presentation,
is isomorphic to the tensor quantale
where I is the free involutive monoid on one generator, whose words can be
concretely identified with the strings of symbols α and α∗ and whose unit we
shall denote by ε, and
L(d) = L⊗|d| = L⊗ · · · ⊗ L (|d| times) .
Note that L(ε) = ℘( 1) is the neutral element of the tensor product. The
multiplication is defined on pure tensors just by concatenation
(x0 ⊗ . . .⊗ xn)(y1 ⊗ . . .⊗ ym) = x0 ⊗ . . .⊗ xn ⊗ y1 ⊗ . . .⊗ ym ,
where in the case of concatenation with elements of ℘( 1) we use the identi-
fication ℘( 1) ⊗ L ∼= L ∼= L ⊗ ℘( 1), to produce the identity of the quantale
e = 1℘( 1). The involution
(−)∗ : TL→ TL
is obtained from the isomorphisms L(w)
→ L(w
∗) that are given by
x1 ⊗ · · · ⊗ xn 7→ xn ⊗ · · · ⊗ x1 .
The injection of generators is the α-coprojection of the coproduct
L = L(α) →
L(d).
3 Quantale semantics of modal logic
Propositional normal modal logic. In this section we describe the in-
terpretations of the classical systems of modal logic K, T, K4, S4, and S5.
For details on these we refer the reader to [3, 4].
We shall consider fixed a set Π of propositional symbols. The set Φ of
propositional formulas is defined to be the least set containing Π such that
for all ϕ, ψ ∈ Φ we have
¬ϕ ∈ Φ ,
ϕ ∨ ψ ∈ Φ ,
♦ϕ ∈ Φ ,
where as usual we may define other connectives, for conjunction ∧, implica-
tion →, and the necessity modal operator �, as abbreviations:
ϕ ∧ ψ = ¬(¬ϕ ∨ ¬ψ) ,
ϕ→ ψ = ¬ϕ ∨ ψ ,
�ϕ = ¬♦¬ϕ .
Definition 3.1 A generalized Kripke model consists of a triple (Q,α, v),
where Q is an ssq, α ∈ Q is an accessibility element, and v : Φ → ςQ is an
interpretation map satisfying the following properties for all ϕ, ψ ∈ Φ:
v(ϕ ∨ ψ) = v(ϕ) ∨ v(ψ)
v(ϕ)v(¬ϕ) = 0
v(ϕ) ∨ v(¬ϕ) = e
v(♦ϕ) = ς(αv(ϕ)) .
Remark 3.2 The above definition makes each element v(ϕ) be comple-
mented in ςQ, with v(¬ϕ) being its (unique) complement, and it also follows
that conjunction is interpreted as multiplication (equivalently, meet) in ςQ:
v(ϕ ∧ ψ) = v(ϕ)v(ψ) .
This means that we interpret the formulas inside a Boolean subalgebra of ςQ,
hence obtaining a classical semantics of propositional modal logic, a fact that
was already implicit in the definition of the conjunction and the implication
as derived connectives. However, we point out that it is easy to define a
(rather natural) semantics for intuitionistic modal logic. We shall describe
this at the end of §3.
As usual we say that a pointed ssq consists of an ssq Q together with a
specified “point” α ∈ Q. A homomorphism of pointed ssqs is a homomor-
phism of ssqs that preserves the point:
h : (Q,α) → (R, β)
α 7→ β.
From now on we shall denote by BK the Lindenbaum algebra of system
K (i.e., the set of formulas modulo equivalence, which is a Boolean algebra
equipped with a finite join preserving endomorphism ♦).
Definition 3.3 The Lindenbaum quantale for K is the pointed ssq QK which
is presented by generators and relations with BK as the set of generators and
with the following relations for all x, y ∈ BK, where we denote the selected
point by α:
[x ∨ y] = [x] ∨ [y]
[¬x][x] = 0
[¬x] ∨ [x] = e
[♦x] = ς(α[x]) .
From the universal property of ssqs presented by generators and relations
we immediately obtain:
Theorem 3.4 There is a bijective correspondence between abstract Kripke
models (Q,α, v) and homomorphims of unital involutive quantales
QK −→ Q .
In particular, if W is a set then a homomorphism
ρ : QK −→ ℘(W ×W )
is the same as a model for system K with set of possible worlds W and
accessibility relation ρ(α).
In order to obtain similar facts for other systems, such as T, K4, S4, S5,
one must define the appropriate Lindenbaum quantales.
Definition 3.5 The Lindenbaum quantales for T, K4, S4, and S5, are the
pointed ssqs QT, QK4, QS4, and QS5, respectively, which are presented by
generators and relations similarly to QK, with the following additional rela-
tions:
QT: e ≤ α
QK4: αα ≤ α
QS4: e ≤ α ≥ αα
QS5: e ≤ α = α
∗ ≥ αα
Hence, QT is the quotient of QK by the least nucleus j such that j(e) ≤
j(α), and QK4 is the quotient ofQK by the least nucleus j such that j(αα) ≤
j(α). Then we have QS4 = QT ∩QK4 and QS5 is the quotient of QS4 by the
least nucleus j such that j(α) = j(α∗).
Notice that the relational representations of these quantales correspond
to the expected classes of models:
Theorem 3.6 The relational representations Q → ℘(W ×W ) of the Lin-
denbaum quantales Q correspond bijectively to the Kripke models whose ac-
cessibility relations are:
• Reflexive, for Q = QT;
• Transitive, for Q = QK4;
• Preorders, for Q = QS4;
• Equivalence relations, for Q = QS5.
Propositional ramified temporal logic. Now we describe a similar se-
mantics for the ramified temporal logic known as Computational Tree Logic
(CTL), see [2]. As above, Π is a fixed set of propositional symbols. The set
Φ of CTL formulas is defined to be the least set containing Π such that for
all ϕ, ψ ∈ Φ we have
¬ϕ, ϕ ∨ ψ,EXϕ,EFϕ,EGϕ ∈ Φ ,
and we may define other modal operators as abbreviations:
AXϕ ≡ ¬EX¬ϕ ,
AGϕ ≡ ¬EF¬ϕ ,
AFϕ ≡ ¬EG¬ϕ .
Definition 3.7 The intuitive meaning of the various modalities is the fol-
lowing:
• EXϕ means that there is a possible future where ϕ will hold in the
next time instant;
• EFϕ means that there is a possible future where ϕ will eventually hold;
• EGϕ means that there is a possible future where ϕ will always hold
(including now);
• AXϕ means that ϕ will certainly hold in the next time instant;
• AGϕ means that ϕ will always hold (including now) in all possible
future paths;
• AFϕ means that in each possible future path ϕ will eventually hold.
A generalized CTL model consists of a triple (Q,α, v), where Q is an ssq,
α ∈ Q is an accessibility element that satisfies
ς(α) = e
(i.e., time never ends), and v : Φ → ςQ is an interpretation map satisfying
the following properties for all ϕ, ψ ∈ Φ:
v(ϕ ∨ ψ) = v(ϕ) ∨ v(ψ)
v(ϕ)v(¬ϕ) = 0
v(ϕ) ∨ v(¬ϕ) = e
v(EXϕ) = ς(αv(ϕ))
v(EFϕ) = ς
v(EGϕ) =
{a ∈ Q | a ≤ v(ϕ) ∧ ς(αa)} .
It is easy to see that this interpretation conveys the intended meaning to
the modal operators if we let Q = ℘(W ×W ) for some set W . Only the
last condition, for EG, deserves an explanation. This says that EGϕ may
be interpreted as the largest subset X ⊂ W such that every world x ∈ X
satisfies the following two conditions:
• x satisfies the formula ϕ;
• there is a world y ∈ X such that (x, y) ∈ α.
This guarantees that there is an infinite path (possibly with repetitions)
x0, x1, x2, x3, . . .
satisfying ϕ starting at any world x0 where EGϕ holds. Mathematically, the
definition of v(EGϕ) is clarified by the Knaster–Tarski fixed point theorem:
the set of all the lowerbounds of v(ϕ),
S = {a ∈ ςQ | a ≤ v(ϕ)} ,
is a complete lattice and thus the set of pre-fixed points of the monotone
operator f : S → S defined by
f(a) = v(ϕ) ∧ ς(α a)
has a join, which in fact is a fixed point; hence, v(EGϕ) is also the largest
element a ∈ ςQ such that a = v(ϕ) ∧ ς(α a).
Propositional dynamic logic. In the program logic of [1] there are modal-
ities indexed by programs, which themselves form a set with some algebraic
structure. Let Π be a fixed set of propositional symbols and Ξ a set of atomic
programs. The sets F , of formulas, and P , of programs, give us the PDL
language Φ = F ∪ P , and they are defined to be the least sets such that
Π ⊂ F ,
Ξ ⊂ P ,
if ϕ, ψ ∈ F then ¬ϕ, ϕ ∨ ψ ∈ F ,
if p, q ∈ P then p ∪ q, p; q, p∗ ∈ P ,
if ϕ ∈ F and p ∈ P then 〈p〉ϕ ∈ F ,
if ϕ ∈ F then ϕ? ∈ P .
Very briefly, the intuitive meaning of the program constructs is the following:
• p∪ q is the program that behaves in a nondeterministic way either like
p or like q (the choice is made at the beginning of the execution of the
program, once and for all);
• p; q is the program whose execution is that of p followed by q;
• p∗ is the iteration of p, to be thought of as p executed sequentially zero
or more times (not to be confused with the notation for the quantale
involution);
• ϕ? is the program that tests ϕ, succeeding if ϕ is found to be true, and
failing otherwise.
Definition 3.8 A generalized PDL model consists of a pair (Q, v), where Q
is an ssq and v : Φ → Q is an interpretation map satisfying the following
properties for all ϕ, ψ ∈ F and p, q ∈ P :
v(ϕ ∨ ψ) = v(ϕ) ∨ v(ψ)
v(ϕ)v(¬ϕ) = 0
v(ϕ) ∨ v(¬ϕ) = e
v(〈p〉ϕ) = ς(v(p)v(ϕ))
v(p ∪ q) = v(p) ∨ v(q)
v(p; q) = v(p)v(q)
v(p∗) =
v(p)n
v(ϕ?) = v(ϕ) .
This interpretation shows that to a large extent both the formulas and the
programs are treated on an equal footing. In particular, p; q can be regarded
as the (noncommutative) “conjunction” of p and q, and p ∪ q as their dis-
junction, while a formula is just a particular kind of program (ϕ is identified
with ϕ?).
Intuitionistic modal logic. It is easy to define a semantics for intuitionis-
tic propositional modal logic if we let ∧ and → be independent connectives.
This is because the support ςQ of any ssq Q is a locale and therefore a
Heyting algebra, and thus, denoting by \ the residuation operation of ςQ,
b\a =
{c ∈ ςQ | b ∧ c ≤ a} ,
the conditions on v can be simply replaced by the following:
v(ϕ ∨ ψ) = v(ϕ) ∨ v(ψ)
v(ϕ ∧ ψ) = v(ϕ)v(ψ)
v(ϕ→ ψ) = v(ϕ)\v(ψ)
v(¬ϕ) = v(ϕ)\0
v(♦ϕ) = ς(αv(ϕ)) .
This would entirely define the intuitionistic semantics if we contented our-
selves with defining � = ¬♦¬ as before. However, this is a bad interpretation
of �, as for instance it usually does not satisfy the axiom of distributivity
over meets
�(ϕ ∧ ψ)↔ �ϕ ∧�ψ .
Indeed, a much better interpretation, in particular one that satisfies distribu-
tivity of � over (arbitrary) meets, is obtained if we let � be an independent
connective interpreted as the right adjoint of a suitable sup-lattice endomor-
phism, as we now describe.
LetW be a set, let R ⊂W ×W be a binary relation, and let Q be the ssq
℘(W ×W ). Let ♦ and � be the sup-lattice endomorphisms of ςQ defined as
in §1:
♦X = ς(RX)
�X = ς(R∗X) .
Equivalently, taking into account the isomorphism ςQ ∼= ℘(W ) we may
consider ♦ and � to be endomorphisms of ℘(W ):
♦X = {y ∈ W | ∃x∈X (y, x) ∈ R}
�X = {y ∈ W | ∃x∈X (x, y) ∈ R} .
It is straightforward to verify that the usual necessity operator
� : ℘(W )→ ℘(W ) ,
which is defined by
�X = {y ∈ W | ∀x∈W (y, x) ∈ R⇒ x ∈ X} ,
is right adjoint to �, and we may take this as the natural definition of �
when such a “possibility in the past” operator � is available — similarly, a
“necessity in the past” operator � can be defined to be the right adjoint of
�x ≤ y ⇐⇒ x ≤ �y
♦x ≤ y ⇐⇒ x ≤ �y .
This leads to the following quantale-based intuitionistic semantics for propo-
sitional modal logic, where we assume that ∧, →, and � are independent
connectives:
Definition 3.9 A generalized intuitionistic Kripke model consists of a triple
(Q,α, v), where Q is an ssq, α ∈ Q is an accessibility element, and v : Φ→ ςQ
is an interpretation map satisfying the following properties for all ϕ, ψ ∈ Φ:
v(ϕ ∨ ψ) = v(ϕ) ∨ v(ψ)
v(ϕ ∧ ψ) = v(ϕ)v(ψ)
v(ϕ→ ψ) = v(ϕ)\v(ψ)
v(¬ϕ) = v(ϕ)\0
v(♦ϕ) = ς(αv(ϕ))
v(�ϕ) =
{x ∈ ςQ | ς(α∗x) ≤ v(ϕ)} .
This definition illustrates a canonical way in which to define intuitionistic
semantics for other propositional modal logics, including all the examples
seen earlier in this section. We stress the fact that involutive quantales are
essential for this, since without the involution we would neither have the �
operator, nor a canonical definition of �.
It is worth commenting on some aspects of the intuitionistic version of
system S5, which similarly to its classical counterpart is based on imposing
that the accessibility element α should be self-adjoint, and thus � = ♦. The
unit of the adjunction relating � and � is the inequality
x ≤ ��x ,
and thus for intuitionistic S5 we conclude that the axiom-scheme
ϕ→ �♦ϕ (6)
is always satisfied. It is well known that this scheme (together with those
for S4) characterizes the classical system S5. Another axiom-scheme which
is always satisfied by intuitionistic S5 is
♦�ϕ→ ϕ ,
which corresponds to the co-unit of the adjunction, and which classically
(i.e., with � = ¬♦¬) is equivalent to (6).
4 Graded unital involutive quantales
Basic definitions and properties. The usual notion of grading of a ring
has a straightforward counterpart for quantales, which will be useful in §5.
We shall study it now.
Definition 4.1 LetM be an involutive monoid. A unital involutive quantale
Q is graded over M if there is an M-indexed family of sub-sup-lattices Q(m)
of Q satisfying the following two properties.
1. For each a ∈ Q there is one, and only one, element
(am) ∈
such that
2. The following conditions hold for all m,n ∈ M :
Q(m)Q(n) ⊂ Q(mn)
1Q(ε) = e
⊂ Q(m
(The latter is equivalent to
= Q(m
For each m ∈M the set Q(m) is called the component of Q in degree m.
Example 4.2 Recall the tensor quantale of ¶2.7: if L is a sup-lattice and I
is the free involutive monoid on one generator α then the tensor quantale
has an obvious grading over I such that L(ε) ∼= ℘( 1) and L(α) ∼= L.
The following properties are immediate:
Proposition 4.3 Let Q be a unital involutive quantale graded over an invo-
lutive monoid M .
1. The map (am) 7→
m∈M am is an isomorphism of sup-lattices
(m) → Q .
2. If m 6= n then Q(m) ∩Q(n) = {0}.
3. The union
m∈M Q
(m) is join-dense in Q.
4. ↓Q(m) = Q(m) for all m ∈M .
There is a convenient alternative definition if the unital involutive quan-
tale Q is also a locale (an example is the quantale TL of ¶4.2 if L is a locale,
or the quantale T(L) of §5):
Proposition 4.4 Let M be an involutive monoid, and let Q be a unital
involutive quantale which is also a locale. Then Q is graded over M if and
only if there is an M-indexed family (e(m)) of elements of Q satisfying the
following properties:
1. 1Q =
m∈M e
(m) (i.e.,
covers Q);
2. e(m) ∧ e(n) = 0 if m 6= n;
3. e(m)e(n) ≤ e(mn);
4. e(ε) = e;
≤ e(m
∗) (equiv.,
= e(m
Proof. It is clear that if Q is graded then it satisfies 1–5 if we let e(m) be
1Q(m) for each m ∈M . For the converse we define the component Q
(m) to be
↓e(m): then any element a ∈ Q equals
a ∧ 1 = a ∧
e(m) =
a ∧ e(m)
where a∧ e(m) ∈ Q(m) by definition of Q(m); and if
bm then, for
each n ∈M we have
an = an ∧
am = an ∧
an ∧ bm = an ∧ bn ,
and in a similar way we obtain bn = bn ∧ an. Hence, we have an = bn, and
thus each element a ∈ Q can be obtained uniquely as a join
am. The rest
is straightforward.
Graded nuclei and quotients. The natural notion of quotient that re-
spects the grading of a quantale is provided by the following definition:
Definition 4.5 Let Q be a unital involutive quantale graded over an invo-
lutive monoid M . A nucleus j : Q→ Q is graded if it satisfies the following
two conditions for all (am) ∈
m∈M Q
⊂ Q(m);
m∈M am
m∈M j(am).
Proposition 4.6 Let j be a graded nucleus as in the definition above. Then,
1. j(0) = 0 (the nucleus is “dense”);
2. Qj is graded, with each component being defined by
(m) = j
Proof. The first condition is obvious from the fact that 0 ∈
m∈M Q
and thus j(0) ∈
m∈M Q
(m) = {0}. For the second condition notice that if
a ∈ Qj then on one hand we have a unique representation of a as a join
and, on the other hand,
a = j(a) = j
j(am) ,
and thus am = j(am) for all m ∈M ; that is, the element am is necessarily in
(m). The rest is straightforward.
The nucleus induced by a binary relation is graded provided the relation
respects the grading:
Proposition 4.7 Let Q be a unital involutive quantale graded over an invo-
lutive monoid M . Let also R ⊂ Q×Q be a binary relation that respects the
grading in the sense that R ⊂
Q(m)×Q(m). Then jR is a graded nucleus.
Proof. Let ⊏R ⊂ Q×Q be the preorder defined by
a ⊏R b ⇐⇒ jR(a) ≤ jR(b) .
Since this is also a sub-involutive-quantale of Q×Q, let us call it a congruence
preorder. By a simple adaptation of the comments at the end of the sup-
lattices section of §2, there is a bijection between congruence preorders and
nuclei on Q, and ⊏R is the least congruence preorder on Q which contains R.
It is clear that ⊏R respects the grading because R does, and thus if a ∈ Q
then jR(a) ∈ Q
(m), showing that jR satisfies the first of the properties of
graded nuclei. In order to prove that it also satisfies the second property let
k : Q→ Q be the map defined, for each (am) ∈
Q(m), as follows:
jR(am) .
Since jR is monotone we have k ≤ jR:
jR(am) = k
Now let us see that k is itself a nucleus. First, it is obvious that it is monotone
and that it satisfies a ≤ k(a) for all a ∈ Q. It is also idempotent because
jR(am)
and the fact that jR(am) ∈ Q
(m) allows us to conclude that the right hand
side of the above equation equals
jR(jR(am)) =
jR(am) = k
Now let us prove the condition relating k to the multiplication. For each pair
(am), (bm) ∈
Q(m) we have
jR(am)
jR(bm) =
jR(ap)jR(bq)
jR(apbq)
The condition relating k to the involution is equally simple and we omit
it. Finally, it is obvious that for (a, b) ∈ R we have k(a) ≤ k(b), since
jR(a) ≤ jR(b). But, by definition, jR is the least nucleus that satisfies this
condition, and therefore we conclude that k = jR. Hence, jR is graded.
5 Construction of the Lindenbaum quantales
The involutive tensor quantale of a frame. Let L be a frame, and
denote by I the free involutive monoid on one generator α, whose words are
the finite sequences of α and α∗, and whose unit we shall denote by ε.
For each w ∈ I we shall denote by L(w) the sup-lattice L⊗(|w|+1), where
|w| is the length of the word w (notice the difference with respect to ¶2.7):
L(ε) = L ,
L(α) = L(α
∗) = L⊗ L ,
L(αα) = L(αα
∗) = L(α
∗α) = L(α
∗α∗) = L⊗ L⊗ L ,
For each w,w′ ∈ I we define a map
ϕw,w′ : L
(w) × L(w
′) → L(ww
ϕw,w′(x1 ⊗ · · · ⊗ xn, y1 ⊗ · · · ⊗ ym) = x1 ⊗ · · · ⊗ (xn ∧ y1)⊗ · · · ⊗ ym .
It is easy to see that this preserves joins in each variable, and thus it defines
a sup-lattice homomorphism
ϕw,w′ : L
(w) ⊗ L(w
′) → L(ww
Defining
T(L) =
(not the same as TL, cf. ¶¶2.7 and 4.2), and using the distributivity of⊗ over
, we obtain the following sup-lattice homomorphism T(L)⊗T(L)→ T(L),
T(L)⊗ T(L)
∼= //
L(w) ⊗ L(w
ϕw,w′ //
// T(L) ,
where the rightmost homomorphism is the copairing of the family of sup-
lattice embeddings L(ww
′) → T(L) which is given by the universal property of
the sup-lattice coproduct
′). Hence, there is a bilinear multiplication
T(L)× T(L)→ T(L). It is defined on pure tensors by
(x1 ⊗ · · · ⊗ xn)(y1 ⊗ · · · ⊗ ym) = x1 ⊗ · · · ⊗ (xn ∧ y1)⊗ · · · ⊗ ym ,
and it is straightforward to see that it is associative, hence giving us a quan-
tale multiplication on T(L). This multiplication has a unit, which coincides
with 1L ∈ L
(ε) = L, and an involution
(−)∗ : T(L)→ T(L)
is obtained from the isomorphisms L(w)
→ L(w
∗) that are given by
x1 ⊗ · · · ⊗ xn 7→ xn ⊗ · · · ⊗ x1 .
Hence, T(L) is a unital involutive quantale, and it is clearly graded over I,
so that we can define:
Definition 5.1 The tensor involutive quantale of L is the graded unital
involutive quantale T(L).
There is an obvious homomorphism of involutive monoids (−) : I → T(L)
that sends each word w to 1L ⊗ · · · ⊗ 1L ∈ L
(w). Hence, in particular,
α = 1L ⊗ 1L ∈ L
(α) and α∗ = 1L ⊗ 1L ∈ L
(α∗).
The quantale T(L) has the following universal property:
Proposition 5.2 Let Q be a unital involutive quantale such that b = b2 = b∗
for all b ∈ ↓eQ (in particular, this implies that ↓eQ is a locale). Let also
h : L→ ↓eQ
be a homomorphism of locales, and let a ∈ Q. Then there is exactly one
homomorphism of unital involutive quantales
ϑ : T(L)→ Q
such that:
1. ϑ(x) = h(x) for all x ∈ L(ε) = L;
2. ϑ(α) = a.
Proof. By the universal property of the coproduct of sup-lattices, every
sup-lattice homomorphism ϑ with domain T(L) is uniquely determined by
its value on the pure tensors of T(L). Furthermore, every pure tensor
x1 ⊗ · · · ⊗ xn ∈ L
with wi = α, α
∗ can be written as a product of xi ∈ L, α ∈ L
α and α∗ ∈ Lα
and thus if ϑ is a homomorphism of unital involutive quantales that satisfies
1 and 2 then its value is uniquely determined on all the pure tensors. This
proves that if ϑ exists then it is unique. In order to prove existence, assign
to each pure tensor
x1 ⊗ · · · ⊗ xn ∈ L
the value h(x1)a1h(x2) . . . an−1h(xn) ∈ Q where ai = a or ai = a
∗ according
to whether wi is α or α
∗, respectively. This assignment preserves joins in
each variable xi separately and thus it defines a sup-lattice homomorphism
ϑw : L
(w) → Q. The copairing
ϑ = [ϑw]w∈I : T(L)→ Q
is easily seen to preserve the quantale multiplication, the unit and the invo-
lution, and it satisfies conditions 1 and 2.
For the following we denote by Frm the full subcategory of Qu whose
objects are the locales (this is usually called the category of frames [5]).
Corollary 5.3 Let Que be the full subcategory of Qu whose objects are those
unital involutive quantales Q such that b = b2 = b∗ for all b ≤ e in Q. Let
also Que∗ be the corresponding category of pointed quantales. There is an
obvious functor Que∗ → Frm that to each quantale Q assigns ↓e, and such
that h 7→ h|↓e for each homomorphism h. This functor has a left adjoint
which to each locale L assigns the pointed quantale (T(L), α).
Bimodal frames and pointed quantales. We have already mentioned
that for an ssq Q, ςQ = ↓e is a locale. It is also clear that, for α in Q, the
operators ♦x = ς(αx) and �x = ς(α∗x) preserve arbitrary joins, hence they
are sup-lattice endomorphisms of ςQ.
Definition 5.4 We say that two sup-lattice endomorphisms of L, ♦ and �,
are conjugate modalities if for all x, y ∈ L we have
♦x ∧ y ≤ ♦(x ∧ �y) ,
�x ∧ y ≤ �(x ∧ ♦y) .
A bimodal frame (L,♦,�) is a frame L equipped with two conjugate modal-
ities ♦ and �.
Proposition 5.5 Let Q be an ssq, and α ∈ Q. Then
(ςQ, ς(α−), ς(α∗−))
is a bimodal frame.
Proof. We only have to check that the two endomorphisms are conjugate
modalities. From the fact that ς is a support (4) we have:
ς(αx)y ≤ αxα∗y ,
and thus
♦x ∧ y = ς(αx)y = ς(ς(αx)y) ≤ ς(αxα∗y) = ς(αxς(α∗y)) = ♦(x ∧ �y) ,
using stability and the fact that x, y ∈ ςQ. The other conjugacy condition is
obtained by interchanging α and α∗.
From now on we shall refer to any sup-lattice endomorphism ς : Q→ Q on
a unital involutive quantale Q such that ςa ≤ e for all a ∈ Q as a pre-support
of Q.
Given a bimodal frame (L,♦,�), a pre-support can be easily defined on
pure tensors of T(L) (and then extended to joins of these in the obvious way):
if x = x0 ⊗ · · · ⊗ xn is in degree w = w1 . . . wn (with wi ∈ {α, α
∗}) then
ςx = x0 ∧ 〈w1〉(x1 ∧ 〈w2〉(. . .)) ,
where 〈wi〉 is ♦ or � according to whether wi = α or wi = α
∗, respectively.
Recursively, we have:
Definition 5.6 Let x = x0 ⊗ · · · ⊗ xn ∈ L
(w1...wn). Then,
• ςx = x, if n = 0;
• ςx = x0 ∧ 〈w1〉(ςx
′), if n ≥ 1, where x′ = x1 ⊗ · · · ⊗ xn ∈ L
(w2...wn).
Lemma 5.7 The following properties hold for all a, b, c ∈ T(L):
1. ςe = e and ςa ≤ e (condition 3 in the definition of support);
2. ς(ςab) = ςaςb (in particular, ςςa = ςa);
3. ς(ab) = ς(aςb) (we say the pre-support ς is stable);
4. If ♦ and � are conjugate we have
(a) ςa ≤ ς(aa∗);
(b) ς(ςab) ≤ ς(aa∗b);
(c) ς(cςab) ≤ ς(caa∗b).
Proof. 1. ς T(L) = L and e is 1L.
2. It suffices to prove this for all the pure tensors b ∈ L(v), where v is an
arbitrary degree. Let
b = y0 ⊗ · · · ⊗ yp ∈ L
(v1...vp) .
We have ςa ∈ L(ε), and thus from ¶5.6 we obtain
ς(ςab) = ς((ςa ∧ y0)⊗ · · · ⊗ yp)
= (ςa ∧ y0) ∧ 〈v1〉(ς(y1 ⊗ · · · ⊗ yp))
= ςa ∧ (y0 ∧ 〈v1〉(ς(y1 ⊗ · · · ⊗ yp)))
= ςaςb .
3. It suffices to prove this for all the pure tensors a ∈ L(w), where w is an
arbitrary degree. Let then
a = x0 ⊗ · · · ⊗ xn ∈ L
(w1...wn) .
The proof is done by induction on n. For the base case assume that
n = 0; that is, we have a = ςa = x0 ∈ L
(ε), and from 2 we obtain
ς(ab) = ς(ςab) = ςaςb = aςb ,
whence ς(ab) = ςς(ab) = ς(aςb).
Now for the induction step let n ≥ 1 and let
a′ = x0 ⊗ · · · ⊗ xn−1 ∈ L
(w1...wn−1) .
We have
a = a′wnxn
and thus
ς(ab) = ς(a′wnxnb)
= ς(a′ς(wnxnb)) (Induction hyp.)
= ς(a′〈wn〉(ς(xnb))) (Def. of ς)
= ς(a′〈wn〉(xnςb)) (By 2)
= ς(a′ς(wnxnςb))) (Def. of ς)
= ς(a′wnxnςb) (Induction hyp.)
= ς(aςb) .
4. First we remark that (4a) is an instance of (4b) (which in turn is an
instance of (4c)). Moreover, (4b) implies (4c) due to stability: if we
assume (4b) then
ς(cςab) = ς(cς(ςab)) ≤ ς(cς(aa∗b)) = ς(caa∗b) .
It now suffices to prove (4b). We shall prove ς(ςab) ≤ ς(aa∗b) for the
particular case where a is a pure tensor
a = x0 ⊗ · · · ⊗ xn
in degree w = w1 . . . wn (n ≥ 1), which implies the general case. The
proof is by induction on n.
Base: for n = 0, we have a = ςa = aa∗, and thus ς(ςab) = ς(aa∗b).
Step: for n ≥ 1, let r be x1 ⊗ · · · ⊗ xn ∈ L
(w2...wn); hence, we have
a = x0w1r, and thus using stability we obtain
ς(aa∗b) = ς(x0w1rr
∗w∗1x0b) = ς(x0w1rr
∗ς(w∗1x0ςb)) .
By the definition of ς (and making the symbol ∧ explicit for the mul-
tiplication in ς T(L)) this equals
x0 ∧ 〈w1〉ς(rr
∗〈w∗1〉(x0 ∧ ςb)) ,
which, by the induction hypothesis, is greater or equal to
x0 ∧ 〈w1〉ς(ςr ∧ 〈w
1〉(x0 ∧ ςb)) ,
which in turn equals
x0 ∧ 〈w1〉(ςr ∧ 〈w
1〉(x0 ∧ ςb))
(because the argument of the outermost occurrence of ς was in ς T(L)).
Finally, by conjugacy of the operators 〈w1〉 and 〈w
1〉 the latter is greater
or equal to
x0 ∧ 〈w1〉(ςr) ∧ x0 ∧ ςb = x0 ∧ 〈w1〉(ςr) ∧ ςb
= ς(x0w1r) ∧ ςb = ςa ∧ ςb = ς(ςab) .
The supported quantale of a bimodal frame. So far we have obtained,
from an arbitrary bimodal frame, a quantale with a stable pre-support. In
order to obtain an actual supported quantale we shall impose the missing
properties, namely ςa ≤ aa∗ (4) and a ≤ ςaa (5), by taking quotients of
T(L).
Definition 5.8 Let jς be the least nucleus j on T(L) such that
j(a) = j(ςaa) .
We define Tς(L,♦,�) to be T(L)jς . We also write Tς(L) if ♦ and � are clear
from the context.
From ¶4.7 it is clear that jς is a graded nucleus, and it is the identity on
L(ε) = L because for all a ∈ L we have ςaa = a. Hence, we have concluded,
just from the graded structure of T(L), that the injection of generators of L
into Tς(L,♦,�) is 1–1.
Proving a similar fact for the other axiom, ςa ≤ aa∗, is less easy, and we
shall address this now. Let (L,♦,�) be a bimodal frame and let
R = {(ςa, aa∗) | a ∈ Tς(L,♦,�)} .
Definition 5.9 TK(L,♦,�) is Tς(L,♦,�)jR. As in ¶5.8 we may write TK(L).
We shall denote the selected point jR(jς(α)) ∈ TK(L) by α.
Lemma 5.10 Recall the definition (2.5) of R. If (y, z) ∈ R then ςy ≤ ςz in
Tς(L,♦,�).
Proof. We have ςy ≤ ςz for all (y, z) ∈ R if and only if the following two
conditions hold for all (y, z) ∈ R and all a, b ∈ Tς(L):
ς(ayb) ≤ ς(azb) (7)
ς(ay∗b) ≤ ς(az∗b) . (8)
In order to prove these two conditions we shall show that they hold for all
(y, z) ∈ R and that they are preserved by the recursive rules of construction
of R.
Let (y, z) ∈ R; that is, let y and z be of the form y = ςt and z = tt∗. We
ς(ayb) = ς(aςtb) ≤ ς(att∗b) = ς(azb) ,
from ¶5.7. We similarly have ς(ay∗b) ≤ ς(az∗b) because y and z are self-
adjoint.
Now assume that (7)–(8) hold for some pair (y, z) ∈ Tς(L) × Tς(L). We
shall prove that they equally hold for the following pairs: (i) (ςy, ςz); (ii)
(y∗, z∗); (iii) (qy, qz); and (iv) (yq, zq), for all q ∈ Tς(L).
(i) Since (y, z) satisfies (7)–(8) we have ςy ≤ ςz (make a = b = 1L), and
thus ς(aςyb) ≤ ς(aςzb) for all a, b ∈ Tς(L), proving (7) for the pair (ςy, ςt).
Since ςy and ςz are self-adjoint, we also conclude (8) for the pair (ςy, ςt).
(ii), (iii) and (iv) are obvious.
Theorem 5.11 The unit of the adjunction L→ TK(L) is 1–1.
Proof. Equivalently, we want to prove that ς Tς(L) ⊂ QjR, or, in other
words, that for all (y, z) ∈ R and x ∈ L we have
z ≤ x⇒ y ≤ x . (9)
Let P ⊂ R be the subset of R consisting of all those (y, z) such that (9) holds
for all x ∈ L. We shall prove that R ⊂ P and that P is closed under the
recursive formation rules of R, hence showing that P = R because R is the
least subset of Tς(L)× Tς(L) satisfying these conditions.
Let (ςy, yy∗) ∈ R. If x ∈ L and yy∗ ≤ x we conclude that y = ςy = yy∗ ∈
L due to the grading of Tς(L) over the free involutive monoid I, and thus
ςy ≤ x, showing that R ⊂ P .
From now on let (y, z) be a fixed but arbitrary element of P . By ¶5.10 we
conclude ςy ≤ ςz. Hence, (9) holds for the pair (ςy, ςz), and thus (ςy, ςz) ∈ P .
Now let q ∈ Tς(L) and assume that qz ≤ x for some x ∈ L. Then z ≤ 1L
(again due to the grading over I), and thus y ≤ 1L because (y, z) ∈ P (make
x = 1L). Hence, again using the previous lemma we obtain
qy = qςy ≤ qςz = qz ≤ x ,
showing that (qy, qz) ∈ P . In a similar way we conclude that (yq, zq) ∈ P .
Finally, x ≤ 1L implies that x is self-adjoint, and thus the conditions y
∗ ≤ x
and z∗ ≤ x are equivalent to y ≤ x and z ≤ x, respectively, showing that
(y∗, z∗) ∈ P .
T, K4, S4, S5. Now let us extend our results to the systems of modal
logic T, K4, S4, and S5. As was explained in §3, we shall need to impose
additional conditions on the selected element α ∈ TK, such as reflexivity
(α ≥ 1L), transitivity (α
2 ≤ α), etc. In order to obtain again coreflections
we shall also have to impose additional axioms on the modalities ♦ and � of
L. As we mentioned in §1, we shall see that for T, K4 and S4 these coincide
with the well known axioms for the corresponding systems of modal logic
under consideration (in other words, the same axioms still produce complete
axiomatizations for the new semantics), whereas for S5 a new axiomatization
is defined just by imposing that ♦ should coincide with �.
The proof techniques are very similar to those employed in the previous
sections for the system K. In fact we could have already presented the theory
for K in such a generality so as to be able to directly reuse the results now,
but this would have obscured the main ideas, so for the sake of clarity we
shall single out the general results only now.
Lemma 5.12 Let ρ ⊂ Tς(L) × Tς(L) be any binary relation on Tς(L), and
let ρ be the closure of ρ under the rules
(y, z) ∈ ρ ⇒ (ςy, ςz) ∈ ρ
(y, z) ∈ ρ ⇒ (ayb, azb) ∈ ρ for all a, b ∈ Tς(L)
(y, z) ∈ ρ ⇒ (y∗, z∗) ∈ ρ .
Assume that for all (y, z) ∈ ρ and all a, b ∈ Tς(L) we have
ς(ayb) ≤ ς(azb)
ς(ay∗b) ≤ ς(az∗b) .
Then for all (y, z) ∈ ρ we have ςy ≤ ςz.
Proof. This follows from a simple adaptation of the proof of ¶5.10.
Lemma 5.13 Let P ⊂ Tς(L)×Tς(L) be the set of all those (y, z) satisfying
the following two conditions:
1. ςy ≤ ςz;
2. z ≤ x⇒ y ≤ x for all x ∈ L.
Then P is closed under the rules
(y, z) ∈ P ⇒ (ςy, ςz) ∈ P
(y, z) ∈ P ⇒ (ayb, azb) ∈ P for all a, b ∈ Tς(L)
(y, z) ∈ P ⇒ (y∗, z∗) ∈ P .
Proof. The proof of this lemma is contained in the proof of ¶5.11, where P
was defined to be a subset of R, but in fact the only property of R used in
order to prove the closure properties of P was the fact that for all (y, z) ∈ R
we have ςy ≤ ςz. The other key ingredient is the fact that ab ∈ L implies
a, b ∈ L for all a, b ∈ Tς(L), due to the grading of Tς(L) over I.
Theorem 5.14 Let ρ ⊂ Tς(L)×Tς(L) be a binary relation such that for all
(y, z) ∈ ρ and all a, b ∈ Tς(L) we have
ς(ayb) ≤ ς(azb) (10)
ς(ay∗b) ≤ ς(az∗b) , (11)
and let Q be the (supported) quotient of Tς(L) generated by ρ. Then the
injection of generators of L onto ςQ,
η : L→ ς Tς(L)→ ςQ ,
is an isomorphism.
Proof. This is an immediate consequence of the previous two lemmas, by a
reasoning analogous to that of ¶5.11.
Similarly to what we have done in §3 for the Lindenbaum quantales QT,
QK4, etc. (see ¶3.5), we define TT(L), TK4(L),TS4(L) and TS5(L) to be quo-
tients of TK(L) by analogous defining relations:
TT(L): e ≤ α
TK4(L): αα ≤ α
TS4(L): e ≤ α ≥ αα
TS5(L): e ≤ α = α
∗ ≥ αα
Corollary 5.15 Let L be a bimodal frame such that for all x ∈ L the condi-
tions x ≤ ♦x and x ≤ �x hold. Then the injection of generators L→ ς TT(L)
is an isomorphism.
Proof. The quantale TT(L) is the quotient of Tς(L) generated by the con-
ditions
ςa ≤ aa∗, for all a ∈ Tς(L) ,
α ≥ e .
Define RT ⊂ Tς(L)× Tς(L) as follows:
RT = {(ςy, yy
∗) | y ∈ Tς(L)}) ∪ {(1L,α)} .
All we have to do is, by the previous theorem, prove that for all (y, z) ∈ RT
the conditions (10)–(11) are satisfied for all a, b ∈ Tς(L). This has already
been done for the pairs of the form (ςy, yy∗) in ¶5.10, so we only have to
concern ourselves with the pair (1L,α). For a, b ∈ Q we have
ς(ab) = ς(aς(b)) ≤ ς(a♦(ς(b))) = ς(aς(αb)) = ς(aαb) ,
where we have used stability of ς twice and the inequality follows from x ≤ ♦x
and monotonicity of ς; this proves (10). Then (11) is proved in a similar way
using the inequality x ≤ �x.
Corollary 5.16 Let L be a bimodal frame such that for all x ∈ L the condi-
tions ♦♦(x) ≤ ♦(x) and ��(x) ≤ �(x) hold. Then the injection of generators
L→ TK4(L) is an isomorphism.
Proof. It remains to prove that the pair (y, z) = (α2,α) satisfies (10)–(11).
The first condition is proved as follows:
ς(aαb) = ς(aς(αb)) = ς(a♦(ς(b))) ≥ ς(a♦2(ς(b))) = ς(aα2b) .
(11) is proved in the same way once we replace α by α∗ and ♦ by � in the
previous argument.
Corollary 5.17 Let L be a bimodal frame such that for all x ∈ L the con-
ditions x ≤ ♦x, x ≤ �x, ♦♦(x) ≤ ♦(x) and ��(x) ≤ �(x) hold. Then the
injection of generators L→ TS4(L) is an isomorphism.
Proof. Immediate from the previous two corollaries.
Corollary 5.18 Let L be a bimodal frame such that for all x ∈ L the con-
ditions of the previous corollary and ♦x = �x hold. Then the injection of
generators L→ TS5(L) is an isomorphism.
Proof. It remains to show that the pairs (α,α∗) and (α∗,α) satisfy (10)
and (11), which is done as follows:
ς(aαb) = ς(aς(αb)) = ς(a♦(ς(b))) = ς(a�(ς(b))) = ς(aα∗b) .
The Lindenbaum quantales. Let BK be the Lindenbaum algebra for
system K, as in §3, and let BT, BK4, BS4, and BS5 be the Lindenbaum
algebras for systems T, K4, S4, and S5, respectively. These are modal lattices
in the following sense:
Definition 5.19 By a modal lattice is meant a bounded distributive lattice
L equipped with an endomap ♦ that preserves finite joins. A bimodal lattice
is a modal lattice equipped with another endomap � that preserves finite
joins and in addition satisfies conjugacy relations similar to those of bimodal
frames:
♦x ∧ y ≤ ♦(x ∧ �y) ,
�x ∧ y ≤ �(x ∧ ♦y) .
The category Lat♦ of modal lattices has the modal lattices as objects and
the homomorphisms of bounded lattices that preserve ♦ as morphisms. The
category Lat♦� of bimodal lattices is defined analogously, with objects being
the bimodal lattices and the morphisms being the homomorphisms of modal
lattices that also preserve �.
We shall also refer to a modal lattice as a
• T-modal lattice if x ≤ ♦x for all x;
• K4-modal lattice if ♦♦x ≤ ♦x for all x;
• S4-modal lattice if it is both a T-modal lattice and a K4-modal lattice;
• S5-modal lattice if it is an S4-modal lattice and ♦x∧ y ≤ ♦(x∧♦y) for
all x and y (i.e., ♦ is conjugate to itself).
The categories Lat♦T, Lat
K4, Lat
S4, and Lat
S5 are, respectively, the full sub-
categories of Lat♦ whose objects are the T-modal lattices, the K4-modal
lattices, the S4-modal lattices, and the S5-modal lattices.
For bimodal lattices we adopt a similar terminology: a bimodal lattice is
referred to as a
• T-bimodal lattice if x ≤ ♦x and x ≤ �x for all x;
• K4-bimodal lattice if ♦♦x ≤ ♦x and ��x ≤ �x for all x;
• S4-bimodal lattice if it is both a T-bimodal lattice and a K4-bimodal
lattice;
• S5-bimodal lattice if it is an S4-bimodal lattice and ♦x = �x for all x.
The categories Lat♦�T , Lat
K4, Lat
S4 , and Lat
S5 are, respectively, the full
subcategories of Lat♦� whose objects are the T-bimodal lattices, the K4-
bimodal lattices, the S4-bimodal lattices, and the S5-bimodal lattices.
By standard universal algebra the forgetful functor Lat♦� → Lat♦ has a
left adjoint which assigns to BK its “enveloping” bimodal lattice B
K. Simi-
larly, there are left adjoints
Lat♦T → Lat
Lat♦K4 → Lat
Lat♦S4 → Lat
and we write B′T, B
K4, and B
S4 for the respective images of BT, BK4, and
BS4 under the left adjoints. For S5 the situation is simpler because the
categories Lat♦S5 and Lat
S5 are obviously isomorphic, since any S5-modal
lattice becomes an S5-bimodal lattice just by defining � to coincide with ♦.
We shall also write B′S5 for BS5 thus regarded as a bimodal lattice.
Since ♦ and � preserve finite joins they can be extended canonically to
sup-lattice endomorphisms of the ideal completion Idl(B′K), which is a frame
because B′K is a distributive lattice. The conjugation relations are easily
seen to be inherited from those of B′K, and thus Idl(B
K) is a bimodal frame.
Similar remarks apply to the other Lindenbaum algebras, and in addition
Idl(B′T) satisfies the axioms of a T-bimodal lattice, Idl(B
K4) satisfies the
axioms of a K4-bimodal lattice, etc. (Hence, in particular, the propositions
in ¶¶5.15–5.18 can be applied to Idl(B′T), Idl(B
K4), Idl(B
S4), and Idl(B
respectively.)
Summarizing, we have described a way of constructing functors from
modal lattices to bimodal frames which are left adjoint to the obvious forget-
ful functors. Composing these functors with the left adjoints from bimodal
frames to pointed ssqs we obtain fromBK, BT, BK4, BS4, andBS5 pointed ssqs
TK(Idl(B
K)), TT(Idl(B
T)), TK4(Idl(B
K4)), TS4(Idl(B
S4)), and TS5(Idl(B
S5)),
respectively. For each system S ∈ {K,T,K4, S4, S5} the map obtained by
composing the following arrows (the leftmost one is just the natural quo-
tient),
BK → BS → B
S → Idl(B
S)→ TS(B
has the same universal property as the injection of generators BK → QS.
Hence, the quantale TS(B
S) is a particular construction of the Lindenbaum
quantale QS:
Theorem 5.20
∼= TK(Idl(B
∼= TT(Idl(B
∼= TK4(Idl(B
∼= TS4(Idl(B
∼= TS5(Idl(B
Since, as we have remarked above, S5-modal lattices and S5-bimodal
lattices are “the same”, our results immediately tell us that the unit of the
adjunction between S5-modal lattices and pointed ssqs,
BS5 → QS5 ,
is a monomorphism. In logical terms this means that a complete axiomati-
zation for the system S5 (with the advantage of making no use of negation
or the modal necessity operator) can be as follows:
Theorem 5.21 S5 is complete for the following axiom schemata:
ϕ → ♦ϕ
♦♦ϕ → ♦ϕ
♦ϕ ∧ ψ → ♦(ϕ ∧ ♦ψ) .
We have not verified whether the remaining canonical mappings
BK → B
BT → B
BK4 → B
BS4 → B
are monomorphisms (although we believe they are). This means that we
have not verified completeness for the classical axiomatizations of K, T, K4,
and S4. Of course, by this we mean we have not verified this in an arbitrary
topos, for otherwise we know, from the classical completeness theorems of
propositional normal modal logic, that the axiomatizations are complete:
using Zorn’s Lemma we can find a Kripke structure (W,R) that gives us a
monomorphism
BK → B
K → TK(Idl(B
∼= QK → ℘(W ×W )
implying that BK → B
K is 1–1, and the same applies to T, K4, and S4.
References
[1] D. Harel, D. Kozen, J. Tiuryn, Dynamic Logic, MIT Press, 2000.
[2] E.A. Emerson, Temporal and modal logic, in J. van Leeuwen (editor),
Handbook of Theoretical Computer Science, vol. B, MIT Press, 1990,
pp. 955–1072.
[3] G.E. Hughes, M.J. Cresswell, An Introduction to Modal Logic, Methuen
& Co. Ltd., London, 1968.
[4] G.E. Hughes, M.J. Cresswell, A Companion to Modal Logic, Methuen
& Co. Ltd., London, 1984.
[5] P.T. Johnstone, Stone Spaces, Cambridge Stud. Adv. Math., vol. 3,
Cambridge Univ. Press, 1982.
[6] A. Joyal, M. Tierney, An Extension of the Galois Theory of
Grothendieck, Mem. Amer. Math. Soc., vol. 309, American Mathemat-
ical Society, 1984.
[7] M.V. Lawson, Inverse Semigroups — The Theory of Partial Symmetries,
World Scientific, 1998.
[8] I. Moerdijk, J. Mrčun, Introduction to Foliations and Lie Groupoids,
Cambridge University Press, 2003.
[9] C.J. Mulvey, Quantales, in M. Hazewinkel (editor), The Encyclopaedia
of Mathematics, third supplement, Kluwer Academic Publishers, 2002,
pp. 312–314.
[10] C.J. Mulvey, P. Resende, A noncommutative theory of Penrose tilings,
Internat. J. Theoret. Phys. 44 (2005) 655–689.
[11] J. Paseka, J. Rosický, Quantales, in B. Coecke, D. Moore, A. Wilce,
(editors), Current Research in Operational Quantum Logic: Algebras,
Categories and Languages, Fund. Theories Phys., vol. 111, Kluwer Aca-
demic Publishers, 2000, pp. 245–262.
[12] A.L.T. Paterson, Groupoids, Inverse Semigroups, and Their Operator
Algebras, Birkhäuser, 1999.
[13] P. Resende, Tropological systems are points of quantales, J. Pure Appl.
Algebra 173 (2002) 87–120.
[14] P. Resende, Étale groupoids and their quantales, Adv. Math. 208 (2007)
147–209.
[15] K. Rosenthal, Quantales and Their Applications, Pitman Research
Notes in Mathematics Series 234, Longman Scientific & Technical, 1990.
Centro de Lógica e Computação
Instituto Superior Técnico
Universidade Técnica de Lisboa
Av. Rovisco Pais 1, 1049-001 Lisboa, Portugal
E-mail: sergiortm@gmail.com
Centro de Análise Matemática, Geometria e Sistemas Dinâmicos
Departamento de Matemática do Instituto Superior Técnico
Universidade Técnica de Lisboa
Av. Rovisco Pais 1, 1049-001 Lisboa, Portugal
E-mail: pmr@math.ist.utl.pt
	Introduction
	Preliminaries
	Quantale semantics of modal logic
	Graded unital involutive quantales
	Construction of the Lindenbaum quantales
