Two-dimensional Kripke Semantics II:
Stability and Completeness
G. A. Kavvos
(March 2024)
Abstract
We revisit the duality between Kripke and algebraic semantics of
intuitionistic and intuitionistic modal logic. We find that there is a certain
mismatch between the two semantics, which means that not all algebraic models
can be embedded into a Kripke model. This leads to an alternative proposal for
a relational semantics, the stable semantics. Instead of an arbitrary partial
order, the stable semantics requires a distributive lattice of worlds. We
constructively show that the stable semantics is exactly as complete as the
algebraic semantics. Categorifying these results leads to a 2-duality between
two-dimensional stable semantics and categories of product-preserving
presheaves, i.e. models of algebraic theories in the style of Lawvere.
1 Introduction
In a previous paper I revisited the relationship between the Kripke and
algebraic semantics of intuitionistic logic and (intuitionistic) modal logic
[35]. Kripke frames (i.e. partial orders) correspond to a certain
class of complete Heyting algebras, the prime algebraic lattices. This
entails a duality , which may be
refined to ‘truth-preserving’ morphisms on one side, and implication-preserving
on the other.
What is curious is that this duality can be reproduced at the level of
categories, which model proofs. Replacing a Kripke frame by a category
leads to an evident definition of a proof-relevant two-dimensional Kripke
semantics. This amounts to taking presheaves over the category, yielding a
bicartesian closed category, i.e. a model of intuitionistic proofs. The
interpretation of formulas is then a direct categorification of Kripke
semantics. This is a duality
between Cauchy-complete categories (qua two-dimensional Kripke frames) and
presheaf categories (qua prime algebraic lattices).
Moreover, this story can be adapted to intuitionistic modal logic. There
is no widespread agreement on what the latter is. However, in [35]
I showed that a relation that is compatible with a partial order, i.e. a
bimodule, canonically induces two adjoint modalities by Kan extension. This provides a canonical proposal as to what
an intuitionistic modal logic should be. Its corresponding Kripke semantics is
(1)
While is indeed the expected modality, uses in the
opposite variance to the more common modality. Conversely, any
adjunction on a prime algebraic lattice uniquely
corresponds to a bimodule, giving a duality
between bimodules on a partial order and prime algebraic lattices equipped
with an operation, i.e. a meet-preserving .
The modal picture can also be categorified, by replacing bimodules with
profunctors. Left Kan extension then induces an adjunction on
. By unfolding the definition of these adjoints we obtain a
remarkable proof-relevant version of (1).
This amounts to a duality between
profunctors on a Cauchy-complete category, and presheaf categories equipped with
a continuous , which
automatically has a left adjoint (by local finite
presentability). This is consistent with what we have come to regard in the last
few years as the categorical semantics of modal logic, i.e. an adjunction on a
bicartesian closed category [14].
Completeness
These dualities also come with theorems relating validity in the Kripke
semantics to validity in the induced algebraic and categorical semantics.
Consequently, we are able to use them to prove completeness of the algebraic
semantics from completeness of the Kripke semantics. Suppose that a formula of
intuitionistic logic is valid in all Heyting algebras; it is then valid in all
prime algebraic lattices, and hence valid in all Kripke frames. Therefore, if
the Kripke semantics is complete, this formula must be provable. As a result,
completeness of the Kripke semantics implies completeness of the algebraic
semantics.
Surprisingly, the converse implication is also provable. An old construction,
whose origins we can trace at least as far as the book by Fitting [23, §1.6], gives a recipe for inducing a Kripke semantics from a
general Heyting algebra, by taking all prime filters. The resulting
structure is richer than an ordinary frame: it is a descriptive frame
[13, §8.4]. This is part of a duality between Heyting algebras
and descriptive frames, which is known as Esakia duality
[22]. It is then possible to relate validity in the descriptive
frame to validity in the Heyting algebra. A categorical version of this
construction for coherent toposes has been shown by Joyal: see [45, Theorem
6.3.5]. When simplified, Joyal’s result amounts to an embedding of
every Heyting algebra into a prime algebraic lattice that preserves all
connectives [28, §3.2] [44] [25].
However, the part of this result that relates validity in the descriptive frame
to validity in the Heyting algebra requires the prime filter existence
theorem [17, §10] [32, §I.2.3], which is a
weak form of the axiom of choice. Similarly, the result of Joyal quoted above
uses highly non-constructive reasoning.
This paper is about trying to avoid this particular reasoning step.
Unlike other streams of work [11], this is not due to a
predilection for constructivity. Instead, we are looking for a construction that
we can categorify, so that it applies to models of intuitionistic (modal)
proofs as well. This will in turn provide interesting information about the
completeness of various classes of models of typed (modal) -calculi.
Stable semantics
However, relating Kripke and algebraic semantics appears impossible without
using prime filters. In an attempt to overcome this I will introduce a new
relational semantics for intuitionistic logic, which I call stable
semantics. The essence can summarised as replacing upper sets, which play a
central rôle in Kripke semantics [35], with filters.
This inescapably leads to the use of distributive lattices as ‘Kripke frames,’
as well as a different interpretation of disjunction, which is reminiscent of
Beth semantics [9] and Kripke-Joyal semantics [37, §II.9] [43, §VI.6] [12, §6.6].
The attendant duality, which is now between distributive lattices and
spectral locales (aka coherent frames), is already well-known from Stone
duality [32, §II.3.2]. Furthermore, the coherent semantics
can be straightforwardly extended to modalities.
The advantage of stable semantics is that we can constructively show an
equi-completeness result. Every Heyting algebra is a distributive
lattice, and so can be used as the ‘possible worlds’ of a stable semantics.
Moreover, every distributive lattice can be interpreted into a complete Heyting
algebra—in fact a spectral locale—in a way that preserves all logical
structure. Thus, the completeness of the stable semantics directly follows from
the completeness of the algebraic semantics.
Two-dimensional stable semantics and algebraic theories
Categorifying the above story engenders a pleasant surprise. The most
technically expedient categorification of the filter construction for our
purposes is the sifted colimit completion. The very same completion plays
a decisive rôle in the algebraic theories in the style of Lawvere
[3]: every category of algebras is a sifted completion of the
opposite of its theory, which is just a cartesian category (i.e. has
finite products).
If we assume that the opposite of a theory is a distributive category
[15], the results on stable semantics can be directly
categorified. This shows that the class of product-preserving presheaves (cf.
filters) on that distributive category (cf. stable frame) is a complete model of
the typed -calculus with sums and an empty type. These results can be
readily adapted to the proofs of intuitionistic modal logic.
Thus, the results herein bear a striking kinship with those of categorical
algebra. I am not yet certain what the long-term impact of this observation is,
but it seems far too compelling to ignore.
Roadmap
In §2 I discuss what it means to regard a
Heyting algebra as a set of possible worlds, as well as the technical issues
that arise when we try to embed that representation into a prime algebraic
lattice. This leads to the introduction of stable semantics in
§3, which is proved equi-complete with Heyting algebras.
Moreover, the relevant duality is discussed. In §4 I
show that the stable semantics can be effortlessly adapted to interpret adjoint
modalities. Then, in §5 I categorify them; this requires a
recap of the elements of Lawvere’s approach to algebraic theories. I give an an
equi-completeness proof, and discuss the resultant syntax-semantics duality.
Finally, this approach is extended to intuitionistic modal proofs in
§6.
2 Heyting algebras as possible worlds
It is a folklore fact that every Kripke frame induces a prime
algebraic lattice , which consists of its upper sets ordered by
inclusion; see e.g. [35, §2]. Looking at this lattice as a Heyting
algebra, i.e. an algebraic semantics for intuitionistic logic, we see that every
formula is interpreted as the set of
worlds in which it is true. This set is upper because Kripke semantics is
monotonic: can be read as saying that world has
potentially more information than world . Thus, the passage from to
may force more formulas to be true, but will not invalidate formulas that were
previously known to be true.
It is interesting to consider a Heyting algebra in the capacity of a Kripke
frame itself. The most evident way of doing so is by taking the opposite of its
order, yielding the partial order , where
is just in . Thinking of as a Tarski-Lindenbaum algebra of an
intuitionistic theory, we see that
Roughly, each element can be thought of as a formula that
specifies what we currently know. The relation holds
just when implies , i.e. when potentially contains more
information.
The order-embedding
then takes to ,
i.e. the set of formulas that imply . It is well-known that
preserves finite meets and exponentials, so that
However, famously does not preserve disjunction: sometimes
. Thus, we
can only embed the fragment of the logic into a prime algebraic
lattice in this manner.
These facts are perhaps better known at the two-dimensional level. Suppose that
is a bicartesian closed category, i.e. a model of intuitionistic proofs.
It is a basic fact of category theory that the Yoneda functor is an embedding, i.e. full, faithful, and
injective on objects. It is also well-known that preserves finite products
and exponentials [7], i.e. that
For a totally unrelated purpose, Dana Scott [49] noticed that this
induces a useful isomorphism:
Lemma 2.1(Scott).
If uses neither disjunction nor falsity then
.
Here is the interpretation of as an object of
, and is the interpretation of
as an object of the category of presheaves ,
both defined following the respective cartesian closed structure. In the second
instance basic propositions are interpreted by the representable
.
It is not difficult to extend this to the categorical models of modal logic.
Following the work of Clouston on Fitch-style -calculi
[14], these are generally understood to be endo-adjunctions
(2)
on a bicartesian closed category . Given such a model, take the left Kan
extension of along Yoneda:
(3)
is then a colimit-preserving functor on the presheaf category,
and has a right adjoint . Thus, we obtain a categorical model of modal
logic on the presheaf category. It is easy to calculate that the action of these
adjoint functors on representables is essentially the same as that of
and , in that (3) commutes:
Consequently, Scott’s lemma directly extends to the categorical semantics of the
fragment of intuitionistic modal logic. Notice
that the diagram (3) witnesses as a (weak)
morphism of categorical models of modal logic without disjunction: is a
cartesian closed functor that preserves the adjunction. Of course, this result
can be de-categorified to one for Heyting algebras equipped with an adjunction.
This leaves the mystery of disjunction. One might think that sheaves are the
answer. However, we will do something far more radical instead.
3 Stable semantics of intuitionistic logic
Given an arbitrary Kripke frame, i.e. a partial order , Kripke
semantics interprets every formula as an upper set of worlds, i.e. a set
for which and implies . The
stable semantics will instead revolve around the notion of a filter over
.
Definition 3.1.
A filter over is a non-empty subset
which is
•
upper, in that and implies ; and
•
filtered, in that whenever there exists a with and .
We write for the set of filters over . is a poset
under inclusion—in fact it is a directed complete partial order
(dcpo) (without a bottom element) [27, §O-2.8].
When has more structure the definition of a filter can be somewhat
simplified.
Proposition 3.2.
Let be a meet-semilattice. A subset is a
filter if and only if it is
•
upper, in that and implies ; and
•
a sub-meet-semilattice, in that and
implies
A stable frame is a partial order which is a
distributive lattice. This means that it has both finite joins and meets,
and that they also satisfy the distributive law . Consequently, they also satisfy the dual law [32, §I.1.5], which
we will use heavily.
A stable frame has much more structure than a good old fashioned Kripke frame.
To begin, any two worlds have a meet and a join (we use the same notation as the logic, but rely on context for
disambiguation). If we think of each world as containing information—in
particular about which variables have become true—then these two operators
tell us that it is possible to find least and greatest upper bounds of
information. The fact the distributive law holds means that the interpretation
of these bounds as ‘intersection of information’ and ‘union of information’ is
tenable.
Furthermore, has a bottom element and a top element . The bottom
element represents the baseline level of information, i.e. the fewest
facts we may regard as true. The top element represents a supernova of
information. This amount of information implies all formulae—even false ones.
A stable model consists of a stable
frame and a function . The
valuation assigns to each propositional variable a
filter , to be thought of as the set of worlds in which is
true. The fact this is a filter leads to the following intuitions:
Upper set
A proposition that is true remains true as information
increases.
Top element
Every proposition is true at the supernova world .
Meets
If then both and
contain the information that is true. Therefore, their greatest lower
bound should also contain that information, so that .
Notice that if then , as filters are upper sets. Thus, a
variable that is true at the baseline world is true throughout a stable
frame.
The stable semantics is defined through a relation
with the meaning that is true in world
of model . When it is clear which model we are using we will skip
it, writing simply . The clauses for
are much like those for the Kripke semantics,
with the characteristic clause for :
The only clauses that change are the ones for falsity and
disjunction:111One of the reviewers pointed out that the clause for
disjunction can be simplified to . However, that version of
the clause does not seem immediately amenable to categorification, unlike this
one.
There are a number of things to notice about this definition.
First, the falsity can now be a true formula; but it is only true at , which is top element for the information order . In fact,
every formula is true at . In that sense, is a world that contains so
much information that it forces everything—even falsity!—to be true. A
similar concept of exploding, fallible or inconsistent
worlds is common in the context of intuitionistically-provable completeness
proofs for intuitionistic logic and associated realizability models
[51, 20, 50, 28, 40].
Second, the clause for the disjunction at world requires
that both and are true at some worlds and
respectively. However, the common information between and , i.e. , must be less than the information at . When we say that fans into and . But what if one
of the two formulas is a contradiction? This is not a cause for worry, due to
the existence of the supernova world: as , we have that
if and only if .
Third, note that the definition does not mention the joins of worlds
of , even though such joins exist. While joins do not appear explicitly in
the semantic clauses, they are used in the following lemma to show that the
stable semantics is monotonic—in particular in the case of implication.
Strictly speaking, we do not need joins: we could just as well reproduce this
result even in the weaker setting of a distributive semilattice, i.e. a
meet-semilattice with the property that implies that
for some and . However,
we prefer having joins, as their categorification is well-understood.
Lemma 3.3(Filtering).
1.
and imply
.
2.
for any .
3.
and
imply .
Proof.
We prove (iii), and only show the cases for implication and disjunction.
Suppose that , ,
and . As and we know that and by (i), and hence that , for . Hence, by the IH, . But by distributivity.
Suppose that and . Then there exist with and . Then , with .
∎
Both (i) and (iii) of this lemma require the existence of disjunctions; in fact,
they make essential use of the dual distributive law .
It now remains to show how the stable semantics induce an algebraic semantics.
Given a stable frame consider the set
of monotonic functions which preserve finite meets. This is a
partial order under the pointwise order. This poset has a number of curious
properties.
First, the monotonicity of implies that if and , then . Hence, the subset of is
an upper set. As , we know that . Moreover, if and , then , so is closed
under finite meets. In short, is a filter. It is not difficult to show that
every filter gives rise to a map which is
monotonic and finite-meet-preserving. Consequently, there is an order-bijection
. I will keep using the somewhat
cumbersome notation for reasons that will become clear
later.
Second, the poset is a complete lattice, with
meets given by intersection [27, §O-1.15, O-2.8]. The bottom
element is , while the binary join is [27, §O-1.15]. Infinitary joins are given by . In fact, as
is distributive, infinite joins and finite meets satisfy the infinite
distributive law, making a locale, or
complete Heyting algebra (cHA) [32, §II.2.11]. The
exponential is given by , which one can readily
check is a filter whenever and are—as long as is distributive.
Third, given any its principal filter is
. As iff , this gives an order-embedding . The key to this paper is the
following lemma.
Lemma 3.4.
preserves finite and infinite
meets, finite joins, and exponentials.
(The dual of) most of this lemma can be found in [27, §O-2.15];
the rest is elementary—at least if one notices that the domain of is
the opposite of .
Fourth, the principal upper sets are special, as they are
compact. Let be a dcpo. An element is compact just if implies that for some , for any directed set . Like (completely) prime elements, this says
that contains a small, indivisible fragment of information: as soon as it
approximates a directed supremum, i.e. a ‘recursively defined element,’
it must approximate some ‘finite unfolding’ of it. We write for
the set of compact elements of . It is not hard to show that the compact
elements of are exactly the principal upper sets
for some [27, §I-4.10] [1, Prop.
2.2.2]. Due to the finitary cases of Lemma
3.4 this means that the sub-poset of compact elements
is in fact a sub-lattice of
. This fact will prove very important.
Fifth, the complete lattice is algebraic [27, §I-4.10] [1, §2.2]. This means that all its
elements can be reconstructed as directed suprema of compact ones. In symbols,
is algebraic just if
In summary, if is distributive, is a frame which is
(i) algebraic, and (ii) whose compact elements form a sub-lattice. Such lattices
are referred to as spectral locales (or coherent frames), and play
an important rôle in Stone duality. In fact, every such locale arises as the
partial order of filters of a distributive lattice [32, §II.3.2]:
Theorem 3.5.
A frame is coherent iff it is isomorphic to for a
distributive lattice .
This theorem says that a coherent frame is isomorphic to the
filters of its compact elements.
Finally, the fact that every element can be reconstructed as a supremum of
compact elements means that it is possible to canonically extend any monotonic
that preserves finite joins to a monotonic,
join-preserving , as long as is a complete
lattice. Diagrammatically, in the situation
(4)
there exists a unique which preserves all joins and satisfies
. It is given by
We call the Scott-continuous extension of along .
This follows from a much more general theorem: if is merely a poset and
a dcpo, then is a dcpo, and there is a unique
Scott-continuous that makes (4)
commute [1, Prop. 2.2.24]. However, if already has finite
joins, then is a complete lattice. The reason is every join
can be written as a directed supremum of non-empty finite ones. Then, if
preserves finite joins, preserves all of them.
As is complete, it has a right adjoint ,
by the adjoint functor theorem [17, §7.34] [32, §I.4.2].
Suppose then that we start with a stable model . By taking
its filters we then obtain a spectral locale . Defining
we obtain a model of intuitionistic logic which interprets
every formula as a filter ,
namely the filter of worlds in which it is true:
Proposition 3.6.
if and only if .
In view of this proposition,
Theorem 3.7(Soundness).
The stable semantics is sound for intuitionistic logic.
3.1 Completeness
Revisiting the remarks of §2 we can prove
that completeness of the stable semantics implies completeness of the algebraic
semantics and vice versa. One direction works exactly as it would for Kripke
semantics:
Theorem 3.8.
Completeness of the stable semantics implies completeness of the algebraic
semantics.
Proof.
Suppose for every Heyting algebra and any
interpretation of the propositions. Hence, given any stable
model we have that where . But Prop.
3.6 then implies that for
all . By completeness of the stable semantics, .
∎
However, the filter construction enables a proof of the other direction as well.
We have an embedding
of any Heyting algebra into the cHA of filters of which is a
Heyting homomorphism by Lemma 3.4. It is worth pausing
for a moment to ponder that a filter on is in fact an ideal of
, viz. a lower set that is a sub-join-semilattice. Thus,
sends to the principal ideal
of in .
Suppose we have a Heyting algebra , and some interpretation of propositional
variables . Define an interpretation into
starting from . Then, by Lemma
3.4,
Proposition 3.9.
We are now in a position to prove that
Theorem 3.10.
Completeness of the algebraic semantics implies completeness of the stable
semantics.
Proof.
Suppose is valid in every stable model. By completeness of the
algebraic semantics, it suffices to show that for any
Heyting algebra , and any interpretation , as this implies
. Consider then the stable model
where . As is valid in this
model, for every . By Proposition
3.6 and Proposition
3.9 we get that .
∎
3.2 Morphisms
We briefly consider what it means to have a morphism of stable
frames. We would like such morphisms to induce a map by . To conclude that is a filter we need to know that
is monotonic, and that it preserves finite meets. Such maps warrant their
own name, which we borrow from the literature on stable domain theory
[8]:
Definition 3.11.
A monotonic map is stable just if it preserves finite
meets. We define Stable to be the category of distributive lattices and
stable maps.
Unlike the category DLatt of distributive lattices, the morphisms
of Stable need not preserve disjunctions.
It is straightforward to show that when preserves finite meets, is
Scott-continuous and preserves arbitrary meets. This defines a functor
, where Coh is the category of
coherent frames and Scott-continuous, meet-preserving morphisms. Note that this
is not the usual category that is used in Stone duality, whose morphisms
are frame maps that preserve compact elements [32, §II.3.3].
It is not difficult to see that is an equivalence. On
objects this is guaranteed by Theorem 3.5. On morphisms, it
suffices to spot that every preserves meets, and hence has a left adjoint
by the adjoint functor theorem. It is then simple to show that left adjoints
preserve compact elements, so that can be extracted by restricting
to . This leads to a duality
(5)
Weaker versions of this duality are well-known, see e.g. [27, §IV-1.16] for a duality between meet-semilattices and algebraic
lattices, as well as references to it in the literature.
However, stable morphisms do not preserve truth. For that, we need to refine the
above duality to maps that are stable, open, surjective, and also
L-morphisms in the sense of Bezhanishvili et al. [10, §2], which appropriately preserve disjunction. The details
are similar to those in [35].
4 Stable semantics of modal logic
In [35] I argued that a canonical Kripke semantics for
intuitionistic modal logic is given by a bimodule, i.e. a monotonic
function over a Kripke frame .
In this section we adapt this to the case where is a stable
frame.
Definition 4.1.
A stable bimodule on is a bimodule
that additionally satisfies the following stability conditions:
1.
2.
3.
4.
A bimodule is a relation with the property that
implies .
This automatically implies the converses of (i) and (iii). Condition (ii) is
redundant, as it is implied by (iv) and the bimodule conditions, but we keep it
for symmetry. A modal stable frame comprises a
stable frame and a stable bimodule .
Stability conditions (i) and (ii) ensure that abstracting the second variable
yields a monotonic map . Moreover,
stability conditions (iii) and (iv) ensure that preserves finite
joins. Then induces the following adjunction by Scott-continuous
extension:
(6)
Like in the Kripke case [35] it can be shown that these maps are
given by
It is easy to show that both and are filters
whenever is; the proof of the first uses stability conditions (i) and (iv),
and the second uses stability conditions (iii) and (iv).
This directly leads to the following clauses of a stable semantics of the two
modalities:
to which Proposition 3.6 readily extends. I
have neglected to mention what a modal stable model is: is a modal stable frame, and
the valuation maps propositions into filters.
4.1 Completeness
In [35] I argued that applying Kan extension to a bimodule
inescapably leads us to an intuitionistic modal logic with two adjoint
modalities, and , as studied by Dzik et al.
[21]. The two clauses of the stable semantics are identical to the
Kripke semantics in loc. cit. But is the logic the same? To answer that
we have to reach for its algebraic models, which are Heyting algebras
equipped with two operators that form an
adjunction . We have just seen that stable
bimodules on correspond precisely to such adjunctions on the cHA
. As Proposition 3.6
remains true if we include and , we have that the stable
semantics is sound for the logic of Dzik et al. Furthermore,
Theorem 4.2.
Completeness of the modal stable semantics implies completeness of the modal
algebraic semantics.
The proof is the same as that of Theorem 3.8. For the
other direction we have to combine our work from intuitionistic logic, and the
argument from §2. Given a Heyting algebra
and an adjunction on it, the map preserves
finite joins, as both and do. Take its Scott-continuous
extension, :
(7)
The map corresponds to a stable
, which maps to iff in . This is by definition stable, but in any case that
is easy to verify manually—as long as one is careful about variance. For
example, to prove (iii), we need to show that whenever there exist with and
and . It suffices to
take and use distributivity.
Diagram (7) commutes. For we
have that by definition. For the we have
Proposition 3.9 extends to the modal case. We
therefore have
Theorem 4.3.
Completeness of the modal algebraic semantics implies completeness of the
modal stable semantics.
The proof is also like that of Theorem 3.10. Thus, the
modal stable semantics is sound and complete for the intuitionistic modal logic
of Dzik et al. [21].
4.2 Morphisms
Like in [35], the duality (5) of
§3.2 can be restricted to a duality
The category on the left has distributive lattices equipped with a stable
bimodule as objects; and stable morphisms that preserve the bimodule as
morphisms. The category on the right has coherent frames equipped with a
meet-preserving operation as objects; and Scott-continuous,
meet-preserving maps for which . In analogy with previous results this can be further refined to a duality
where the morphisms preserve truth on the left, and the operator and implication
on the right.
5 Two-dimensional stable semantics of intuitionistic logic
Following the programme of [35], we look for categorifications of
the stable semantics. Thus, we exchange stable frames for
arbitrary categories with finite products; we could call these
stable categories. The first thing we must categorify is the notion of
filter. Surprisingly, there are two possible choices:
1.
the Ind-completion , which adds all filtered
colimits to [32, §VI.1] [3, §4.17]; and
2.
the Sind-completion , which adds all sifted
colimits to [2, 4, 3].
All filtered colimits are sifted, so the latter involves adding strictly more
colimits to . However, for a poset we have that [2, §2.3]. Thus, these two
completions are indistinguishable at the order-theoretic level. As an
aside, note that the former completion is related to essentially algebraic
theories [5], while the latter to simpler algebraic
theories of Lawvere [3].
We will work with the sifted completion, for several reasons. The most important
one is that, when has finite coproducts, is cocomplete. This
is just enough to allow us to embed any bicartesian closed category (which
has coproducts) into a cocomplete category , adapting the story of
§3. The cocompleteness is absolutely essential in the
semantics of modalities given in §6. Second, the
conditions required on for to be a cartesian closed
category—and hence a model of intuitionistic proofs—are rather weak. Third,
there is an analogy to working with filters as elements of
: the classic Lawverean move of replacing by
[39] leads us to consider product-preserving presheaves
, which coincide with whenever
has products, mirroring Proposition 3.2.
The following proposition collects various well-known facts about the sifted
completion [2, 3]. These are analogous to well-known
facts about presheaf categories [35], and mirror those of
given in §3.
Proposition 5.1.
Let be the sifted completion of .
1.
If has coproducts then is isomorphic to the
category of product-preserving
presheaves and natural transformations. It is a complete and cocomplete
category.
For the rest of this proposition we assume that has coproducts.
2.
Representable presheaves are product-preserving, so is an embedding.
3.
preserves products and
coproducts.
4.
is perfectly presentable, i.e. preserves sifted colimits.
5.
A category is equivalent to for some
if and only if it is cocomplete and has a strong generator
consisting of perfectly presentable objects. Moreover, there is a unique
idempotent-complete category for which this is true (up to
equivalence): the subcategory of perfectly presentable objects.
Proof.
(i) is shown in [2, §2.8] [3, §1.22, 4.5,
4.13].
(ii) is shown in [3, §1.12] and (iii) in [3, §1.13]. (iv) follows from the fact representables are tiny,
and that is closed under sifted colimits in
presheaves [3, §5.5]. (v) is shown in [2]
[3, §6.9, 8.12].
∎
Categories satisfying (v) above are called algebraic categories by
Lawvere [38]. They are essentially categories of models of
algebraic theories: see the textbook by Adamek et al. [3].
One might wonder whether
preserves exponentials. It would, were to have
them; and it has them exactly when is a distributive category, i.e.
whenever the canonical morphism is an isomorphism [15]. The following result is quoted on the
nLab.
Proposition 5.2.
Let have both products and coproducts. Then, the following are
equivalent:
1.
is distributive.
2.
in
3.
is cartesian closed.
In that case preserves
exponentials.
Proof.
(i) (ii): Write as
a colimit of representables. As is product-preserving, its category of
elements is sifted [3, §4.2]. Hence, it does not
matter if this colimit is in presheaves or product-preserving presheaves, as
the latter are closed under sifted colimits within the former [3, §2.5]. Noticing also that is the same operation in both
and we may calculate
now in presheaves
as is left adjoint
now back in
where is now in
colims comm. with colims
(ii) (iii): We only need to prove that the usual exponential
is a product-preserving presheaf. But this easily follows from the observation
that and (ii).
(iii) (i): Then is a bicartesian
closed category, and hence it is distributive. But is an embedding that
preserves products and coproducts, so the subcategory is distributive as
well.
∎
Tracing the origins of the result that was just proven appears challenging. The
claim (i) (iii) appears to be due to Younesse Kaddar
[34]. The presentation here simplifies Kaddar’s calculation by
using (ii). (iii) (i) is stated without proof on the
nLab, and appears to be due to
Sam Staton.
This puts us in a good place to introduce a two-dimensional stable
semantics. This amounts to replacing the stable frame by a
category with products and coproducts for which is
distributive. This means that the somewhat unusual isomorphism holds in . This is known to hold in a number
of categories of algebras, including distributive lattices and commutative rings
[18]. I have yet to grasp the meaning of this for a general Lawvere
theory. Perhaps previous work by Johnstone [33] and Garner
[26] on when categories of varieties are cartesian closed might
give some insight. Finally, note that—unlike distributive
lattices—distributive categories are not self-dual, so this is all we
get.
By Propositions 5.1 and 5.2, the
category is a bicartesian closed category. The
two-dimensional stable semantics is then dictated by the bicartesian closed
structure. The results in this section mean that these follow the
two-dimensional Kripke semantics given in [35]. Thus, every
formula is interpreted as a product-preserving presheaf
Writing to mean for any and for and , the
clauses are the expected proof-relevant categorifications of the stable
semantics of §3. Some are the same as in [35]:
However, the interpretation of is not immediately evident,
as it is a coproduct in . Adamek et al. [3, §4.5] prove the existence of such coproducts abstractly, by
decomposing presheaves as sifted colimits of representables and using the fact
. To enable a direct comparison with the
stable semantics of disjunction of §3, we need to describe
them in a more direct way.
Theorem 5.3.
Let have finite products. Then the coproduct in
is given by the coend
An element of essentially consists of tuples
where is a ‘decomposition’ of , ,
and . If we think of as an algebraic theory, can be
thought of as a term of sort in terms of two variables of sorts and
; and the elements of and can be considered as elements
of the algebra at sorts and respectively.
This is evidently a direct categorification of the stable semantics of
disjunction given in §3. However, as this is now a coend,
these data have to be appropriately quotiented: for any , , and , the tuples and should be identified. This guarantees that the choice of decomposition is
‘minimal.’ It is easy to prove that this object has the right universal
property. However, a conceptual proof that it is product-preserving eludes me.
Finally, notice that this is essentially the ‘free’ product of algebras, as
expected. It is also clearly a version of the Day convolution product on
presheaves [41, §6.2]. It is in fact a known result of higher
algebra that the Day convolution is the coproduct of commutative algebra objects
over a symmetric monoidal -category: see Lurie’s book [42, Lemma
3.2.4.7].
5.1 Completeness
We are now able to show completeness results for the categorical semantics of
intuitionistic logic, i.e. bicartesian closed categories: if is a
bicartesian closed category then it is distributive, and
is an embedding that preserves the bicartesian closed structure of . Lemma
2.1 extends to disjunction and falsity on objects,
but also to proofs. The latter can be represented as terms of the typed
-calculus with sums and an empty type up to equality. We
refer to [16, 37] for background on the categorical
semantics of the typed -calculus.
Lemma 5.4.
Let be a bicartesian closed category.
1.
There is an isomorphism for any
type of the simply-typed -calculus.
2.
If is a term of the typed -calculus,
then the following diagram commutes:
where , and arises from the fact
preserves finite products.
Then, assuming that bicartesian closed categories are complete for the typed
-calculus:
Theorem 5.5.
The subclass of models consisting of over a
distributive is complete for equational theory of the typed
-calculus with sums and an empty type.
Proof.
Let be two terms with when
interpreted in any product-preserving presheaf category
with distributive. Pick any bicartesian
closed . By Lemma 5.4 we have , where the interpretation is now in . But is
faithful, so in every bicartesian closed category .
Then by the completeness of bicartesian closed
categories.
∎
There is of course a converse, which shows that completeness of this class of
models implies completeness of the class of bicartesian closed categories. It is
similar in spirit to Theorem 3.8.
5.2 Morphisms
Unlike most the previous dualities we have presented, the one in this section
has been carefully studied [6, 3]. However, the
terminology is different: instead of stable categories they speak of
algebraic categories; and instead of stable functors, i.e.
functors preserving finite products, they speak of morphisms of algebraic
theories. In fact, the duality required here is a syntax-semantics
duality for Lawvere’s algebraic theories.
To sketch this duality we must first look at the extension properties of
. Given any , where is a category with
sifted colimits, there is a unique that extends and preserves sifted colimits, as in the following
commuting diagram:
(8)
This property is exactly what it means for to be
the sifted colimit completion [3, §4.9]. However, we can also
get a slightly more refined extension property. Suppose that
also preserves coproducts, and that is cocomplete. Then
preserves all colimits and has a right adjoint:
(9)
The reason is that the usual functor is
then valued in , and can readily be shown to be
right adjoint to [3, §4.15].
Then, given any stable take the extension of as in (9)
(10)
We have that acts by
precomposition. It clearly preserves limits; it also preserves sifted colimits,
as they are computed pointwise in [3, §9.3]. Such a functor is called an algebraic functor [3, §9.4]. We thus obtain a (strict) 2-functor
from the (strict) 2-category of Cauchy-complete stable categories, stable
functors, and natural transformations to the (strict) 2-category of
algebraic categories, algebraic functors, and natural transformations.
This functor is a biequivalence, and hence a 2-duality; more
details can be found in [3, §9]. Finally, this can be further
refined to 2-dualities that ‘preserve truth’ in terms of frames.
6 Two-dimensional stable semantics for modal logic
Definition 6.1.
A stable profunctor on is a profunctor which preserves products in its second argument, and for which
preserves coproducts.
This corresponds precisely to an adjunction on , by
the universal property (9):
These functors are more directly expressed as follows:
The expression for follows from (9); it
evidently preserves products. The expression for is the coend
formula for the left Kan extension along Yoneda to all presheaves
[41, §2.3]. It is still the right expression, by the
uniqueness of adjoints. However, it is not easy to see that it preserves
products in : to see that, write as a sifted colimit and use
the rules of coends to show that this set is isomorphic to . The latter clearly preserves products in :
does, and the colimit is sifted.
As in [35], these are the expected categorifications of the
semantics of and .
6.1 Completeness
We can now show another completeness result like that of
§5, which applies to intuitionistic modal proofs.
These are bicartesian closed categories equipped with an adjunction
. They can be represented syntactically by
Clouston’s Fitch-style -calculus which is sound and complete for
such models [14]. Then
is an embedding that preserves all this structure: Scott’s lemma
2.1 extends to and ,
following exactly the proof in §2. Then, a
result similar to Lemma 5.4 holds, leading to the
Theorem 6.2.
The subclass of models consisting of categories
over a distributive equipped with an
adjunction on is
complete for equational theory of intuitionistic modal proofs.
6.2 Morphisms
Following the lead of [35], the 2-duality of
§5.2 can be restricted to a 2-duality
The (strict) 2-category on the left has Cauchy-complete categories equipped with
a stable profunctor as 0-cells; stable functors that preserve the profunctor as
1-cells; and natural transformations natural transformations. The (strict)
2-category on the right has algebraic categories equipped with an
operation that
preserves limits and sifted colimits as 0-cells; algebraic functors equipped with natural transformations
as 1-cells; and natural
transformations as 2-cells. This is essentially a direct categorification of the
duality of §4.2. It can be further refined to a
2-duality where the morphisms preserve truth on the left, and the operator and
implication on the right.
7 Related work
Completions
Much of the development in §3 was based on the filter
completion of a distributive lattice. The dual notion of ideal
completion is far more commonly encountered. It plays a significant rôle in
domain theory, as the ideal completion of a preorder is the free algebraic
dcpo over an arbitrary set of compact-elements-to-be [1, §2.2.6]. The category of algebraic dcpos and continuous maps is
then equivalent to the category of preorders and approximable relations,
which appear rather similar to stable bimodules. The ideal completion also plays
a central rôle in Stone duality for distributive lattices [32, §II].
Choice-free dualities
It is well-known that many Stone-type dualities require the use of a choice-like
principle, e.g. the existence of prime ideals. Choice is sometimes only
necessary when connecting the localic viewpoint with the topological one; see
e.g. [32, §II.4].
Avoiding this use of choice has been a rather active area of research in recent
years, following the work of Bezhanishvili and Holliday
[11]. A choice-free duality for Heyting algebras, as well
as multiple references to recent literature, is given by Hartonas
[29].
Other related work
Bezhanishvili et al. [10] present a positive modal logic.
Their semantics uses a meet-semilattice as a frame. Every formula is interpreted
as a filter over that, leading to the same falsity and disjunction clauses as
the ones I use here. However, the lack of joins and distributivity means that
they cannot handle implication. They also present some interesting links between
their logic and logics of independence and team semantics
[53, 36, 54] to which the results of this paper
might be applicable.
De Groot and Pattison [19] study the fragment
of intuitionistic logic with a meet-preserving modality . They give it a
semantics in semilattices, relating it to filters. Their semantics for is
based on relations which are extremely close to stable bimodules.
The coherent semantics appears rather close to the Kripke semantics of the
separating conjunction of the BI logic of O’Hearn and Pym
[47, 48]. This is not surprising, as the Day convolution is
one of their main monoidal products. However, the fact that their Kripke
semantics can only be shown complete when falsity (interpreted as never true) is
excluded [48, §4] suggests that there might be interesting
connections with the results presented here.
Galal [24] explores a categorification of the Scott-continuous
model of Linear Logic, which also consists of prime algebraic lattices (but with
weaker morphisms than the ones used here)
[30, 31, 46, 52]. The key notion of
directed-completeness is replaced by sifted colimits. No connection to Kripke
semantics is made.
Acknowledgements
This work was supported by the UKRI Engineering and Physical Sciences
Research Council grant
EP/Y033418/1.
I am grateful to Fabian Ruch for suggesting that product-preserving presheaves
might be useful. Thanks are due to Daniel Gratzer for pointers to higher
algebra; to Philip Saville and Pedro Azevedo de Amorim for the use of Day
convolution in BI; and to Ayberk Tosun for general discussions on
spectral locales. Finally, I would like to thank one of the anonymous
reviewers for pointing out that the coherent semantics also work in a
distributive semilattice, as well multiple references to relevant literature
on dualities.
References
[1]
Samson Abramsky and Achim Jung.
Domain theory.
In Samson Abramsky, Dov M. Gabbay, and Thomas S. E. Maibaum, editors,
Handbook of Logic in Computer Science, volume 3, pages 1–168. Oxford
University Press, 1994.
URL: https://www.cs.bham.ac.uk/~axj/pub/papers/handy1.pdf.
[3]
J. Adámek, J. Rosický, and E. M. Vitale.
Algebraic Theories: A Categorical Introduction to
General Algebra.
Cambridge University Press, 2010.
doi:10.1017/CBO9780511760754.
[5]
Jiří Adámek and Jiří Rosický.
Locally Presentable and Accessible Categories.
Cambridge University Press, 1994.
doi:10.1017/CBO9780511600579.
[6]
J. Adámek, F.W. Lawvere, and J. Rosický.
On the duality between varieties and algebraic theories.
Algebra Universalis, 49(1):35–49, 2003.
doi:10.1007/s000120300002.
[7]
Steve Awodey.
Category Theory.
Oxford Logic Guides. Oxford University Press, 2010.
[8]
Gérard Berry.
Stable models of typed -calculi.
In Giorgio Ausiello and Corrado Böhm, editors, Automata,
Languages and Programming, volume 62 of Lecture Notes in
Computer Science, pages 72–89, Berlin, Heidelberg, 1978. Springer
Berlin Heidelberg.
doi:10.1007/3-540-08860-1_7.
[9]
Guram Bezhanishvili and Wesley H. Holliday.
A semantic hierarchy for intuitionistic logic.
Indagationes Mathematicae, 30(3):403–469, 2019.
doi:10.1016/j.indag.2019.01.001.
[10]
Nick Bezhanishvili, Anna Dmitrieva, Jim De Groot, and Tommaso Moraschini.
Positive modal logic beyond distributivity.
Annals of Pure and Applied Logic, 175(2), 2024.
doi:10.1016/j.apal.2023.103374.
[11]
Nick Bezhanishvili and Wesley H. Holliday.
Choice-free Stone Duality.
The Journal of Symbolic Logic, 85(1):109–148, 2020.
doi:10.1017/jsl.2019.11.
[12]
Francis Borceux.
Handbook of Categorical Algebra, volume 3 of Encyclopedia
of Mathematics and its Applications.
Cambridge University Press, 1994.
[13]
Alexander Chagrov and Michael Zakharyaschev.
Modal Logic.
Number 35 in Oxford Logic Guides. Oxford University Press, 1996.
doi:10.1093/oso/9780198537793.001.0001.
[14]
Ranald Clouston.
Fitch-Style Modal Lambda Calculi.
In Christel Baier and Ugo Dal Lago, editors, Foundations of
Software Science and Computation Structures, volume 10803 of Lecture Notes in Computer Science, pages 258–275, Cham, 2018.
Springer International Publishing.
doi:10.1007/978-3-319-89366-2_14.
[15]
J. R. B. Cockett.
Introduction to distributive categories.
Mathematical Structures in Computer Science, 3(3):277–307,
1993.
doi:10.1017/S0960129500000232.
[17]
B. A. Davey and H. A. Priestley.
Introduction to Lattices and Order.
Cambridge University Press, 2nd edition, 2002.
doi:10.1017/CBO9780511809088.
[18]
B. A. Davey and H. Werner.
Distributivity of coproducts over products.
Algebra Universalis, 12(1):387–394, 1981.
doi:10.1007/BF02483898.
[19]
Jim de Groot and Dirk Pattinson.
Modal meet-implication logic.
Logical Methods in Computer Science, 18(3), 2022.
doi:10.46298/lmcs-18(3:1)2022.
[20]
H. De Swart.
Another intuitionistic completeness proof.
The Journal of Symbolic Logic, 41(3):644–662, 1976.
doi:10.2307/2272042.
[21]
Wojciech Dzik, Jouni Järvinen, and Michiro Kondo.
Intuitionistic propositional logic with Galois connections.
Logic Journal of IGPL, 18(6):837–858, 2010.
doi:10.1093/jigpal/jzp057.
[22]
Leo Esakia.
Heyting Algebras: Duality Theory, volume 50 of Trends in
Logic.
Springer International Publishing, 2019.
doi:10.1007/978-3-030-12096-2.
[23]
Melvin Fitting.
Intuitionistic Logic, Model Theory and Forcing.
Studies in Logic and the Foundation of Mathematics. North-Holland,
1969.
[24]
Zeinab Galal.
A Profunctorial Scott Semantics.
In Zena M. Ariola, editor, 5th International Conference on
Formal Structures for Computation and Deduction (FSCD 2020),
volume 167 of Leibniz International Proceedings in Informatics
(LIPIcs), pages 16:1–16:18, Dagstuhl, Germany, 2020. Schloss
Dagstuhl–Leibniz-Zentrum für Informatik.
doi:10.4230/LIPIcs.FSCD.2020.16.
[25]
Adriana Galli, Marta Sagastume, and Gonzalo E. Reyes.
Completeness theorems via the double dual functor.
Studia Logica, 64(1):61–81, 2000.
doi:10.1023/A:1005238330484.
[26]
Richard Garner.
Cartesian closed varieties I: the classification theorem, February
2023.
arXiv:2302.04402 [math].
[27]
G. Gierz, K. H. Hofmann, K. Keimel, J. D. Lawson, M. Mislove, and D. S. Scott.
Continuous Lattices and Domains.
Cambridge University Press, 1 edition, 2003.
doi:10.1017/CBO9780511542725.
[28]
Victor Harnik and Michael Makkai.
Lambek’s categorical proof theory and Läuchli’s abstract
realizability.
Journal of Symbolic Logic, 57(1):200–230, 1992.
doi:10.2307/2275186.
[29]
Chrysafis Hartonas.
Choice-free topological duality for implicative lattices and
Heyting algebras.
Algebra universalis, 85(1):3, 2024.
doi:10.1007/s00012-023-00830-8.
[30]
Michael Huth.
Linear domains and linear maps.
In Stephen Brookes, Michael Main, Austin Melton, Michael Mislove, and
David Schmidt, editors, Mathematical Foundations of Programming
Semantics, volume 802 of Lecture Notes in Computer Science,
pages 438–453, Berlin, Heidelberg, 1994. Springer Berlin Heidelberg.
doi:10.1007/3-540-58027-1_21.
[31]
Michael Huth, Achim Jung, and Klaus Keimel.
Linear types and approximation.
Mathematical Structures in Computer Science, 10(6):719–745,
2000.
doi:10.1017/S0960129500003200.
[32]
Peter T. Johnstone.
Stone Spaces.
Number 3 in Cambridge Studies in Advanced Mathematics. Cambridge
University Press, 1982.
[33]
Peter T. Johnstone.
Collapsed toposes and cartesian closed varieties.
Journal of Algebra, 129(2):446–480, 1990.
doi:10.1016/0021-8693(90)90230-L.
[34]
Younesse Kaddar.
Ideal Distributors, 2020.
Predoctoral research internship, ENS Paris-Saclay and University of
Cambridge.
URL: https://younesse.net/assets/ARPE_report.pdf.
[35]
G. A. Kavvos.
Two-dimensional Kripke Semantics, 2024.
[36]
Juha Kontinen, Julian-Steffen Müller, Henning Schnoor, and Heribert
Vollmer.
Modal independence logic.
Journal of Logic and Computation, 2016.
doi:10.1093/logcom/exw019.
[37]
Joachim Lambek and Philip J. Scott.
Introduction to Higher-Order Categorical Logic.
Number 7 in Cambridge Studies in Advanced Mathematics. Cambridge
University Press, 1988.
[38]
F. William Lawvere.
Functorial semantics of algebraic theories and some algebraic
problems in the context of functorial semantics of algebraic theories.
In Reports of the Midwest Category Seminar II,
volume 50, pages 41–61. Springer Berlin Heidelberg, 1963.
Also available in Reprints in Theory and Applications of
Categories, No. 5 (2004).
URL: http://www.tac.mta.ca/tac/reprints/articles/5/tr5abs.html,
doi:10.1007/BFb0077116.
[39]
F. William Lawvere.
Metric spaces, generalized logic, and closed categories.
Rendiconti del Seminario Matematico e Fisico di Milano,
43(1):135–166, 1973.
doi:10.1007/BF02924844.
[40]
James Lipton.
Constructive Kripke Semantics and Realizability.
In S. S. Chern, I. Kaplansky, C. C. Moore, I. M. Singer, and
Yiannis N. Moschovakis, editors, Logic from Computer Science,
number 21 in Mathematical Sciences Research Institute Publications,
pages 319–357. Springer New York, 1992.
doi:10.1007/978-1-4612-2822-6_13.
[43]
Saunders Mac Lane and Ieke Moerdijk.
Sheaves in Geometry and Logic: A First Introduction to Topos
Theory.
Universitext. Springer New York, 1994.
doi:10.1007/978-1-4612-0927-0.
[44]
M Makkai and G.E Reyes.
Completeness results for intuitionistic and modal logic in a
categorical setting.
Annals of Pure and Applied Logic, 72(1):25–101, 1995.
doi:10.1016/0168-0072(93)00085-4.
[46]
Mikkel Nygaard and Glynn Winskel.
Domain theory for concurrency.
Theoretical Computer Science, 316(1-3):153–190, 2004.
doi:10.1016/j.tcs.2004.01.029.
[47]
Peter W. O’Hearn and David J. Pym.
The Logic of Bunched Implications.
Bulletin of Symbolic Logic, 5(2):215–244, 1999.
doi:10.2307/421090.
[48]
David J. Pym.
The Semantics and Proof Theory of the Logic of Bunched
Implications, volume 26 of Applied Logic Series.
Springer Netherlands, Dordrecht, 2002.
doi:10.1007/978-94-017-0091-7.
[49]
Dana S. Scott.
Relating Theories of the Lambda Calculus.
In Jonathan P. Seldin and J. Roger Hindley, editors, To H.
B. Curry: Essays on Combinatory Logic, Lambda Calculus, and
Formalism. Academic Press, London, 1980.
[50]
Anne Sjerp Troelstra and Dirk Dalen.
Constructivism in mathematics: an introduction, volume 2 of
Studies in Logic and the Foundation of Mathematics.
Elsevier, 1988.
[51]
Wim Veldman.
An intuitiomstic completeness theorem for intuitionistic predicate
logic.
The Journal of Symbolic Logic, 41(1):159–166, 1976.
doi:10.2307/2272955.
[52]
Glynn Winskel.
Linearity and Nonlinearity in Distributed Computation.
In Thomas Ehrhard, Jean-Yves Girard, Paul Ruet, and Philip Scott,
editors, Linear Logic in Computer Science, pages 151–188.
Cambridge University Press, 2004.
doi:10.1017/CBO9780511550850.005.
[53]
Fan Yang and Jouko Väänänen.
Propositional logics of dependence.
Annals of Pure and Applied Logic, 167(7):557–589, 2016.
doi:10.1016/j.apal.2016.03.003.
[54]
Fan Yang and Jouko Väänänen.
Propositional team logics.
Annals of Pure and Applied Logic, 168(7):1406–1441, 2017.
doi:10.1016/j.apal.2017.01.007.