Over the last thirty years, I have repeatedly returned to a particular question in logic:
What should modal logic look like in a constructive world?
This question first appeared in my work in the early 1990s and has since shaped
a series of papers, collaborations, workshops, and talks. Looking back, it is clear
that these efforts form a small research lineage centered on the interaction between
modality and constructive logic, especially intuitionistic logic.
I thought it might be useful to record a bit of that history.
Early motivations
In the early 1990s, modal logic was overwhelmingly studied in classical settings.
But many areas that interested me—proof theory, type theory, and categorical
semantics—are fundamentally constructive. This was a time when new connections
between logic, computation, and category theory were being actively explored.
Developments such as linear logic and the growing use of categorical semantics
made it increasingly natural to ask how modal operators should behave in
constructive settings.
Working constructively changes the landscape dramatically. Logical principles that
are straightforward classically may behave very differently when one insists on
intuitionistic reasoning. This becomes especially visible when modal operators are
introduced. One cannot simply take a classical modal system and reinterpret it
intuitionistically; the interaction with implication, proof structure, and semantics
becomes much more delicate.
Understanding these interactions became the starting point of my work on
intuitionistic modal logics. One of the first results of this effort was a paper
(Intuitionistic Necessity Revisited) written in 1992 with Gavin Bierman and
presented by him at the Logic at Work Conference in Amsterdam in Dec 1992.
The work was later published as On an Intuitionistic Modal Logic
(Studia Logica, 2000).
That paper explored how a modal operator could be integrated into intuitionistic logic
while preserving the constructive character of the system. One quickly discovers that
the design space is surprisingly large: small changes in the interaction between modal
operators and implication can produce quite different logical systems. For this reason,
the paper did not merely introduce a particular system, but also aimed to clarify the
choices involved in designing constructive modal logics, questions that later became
central to much of the subsequent work in the area.
The resulting system was presented through several complementary proof-theoretic
formulations, including a Hilbert system, a sequent calculus, and a natural deduction
system, which were shown to be equivalent. However, as in the case of
intuitionistic linear logic, constructing a natural deduction system that properly
supports a Curry–Howard correspondence turns out to be subtle. The key issue is
the preservation of substitution: constraints that are invisible at the level of the
sequent calculus become essential in Natural Deduction: your ND proof trees need to
compose. This phenomenon has direct consequences for the categorical semantics
(which is the main point for me!). Ensuring that substitution behaves correctly
corresponds to enforcing coherence conditions, which in practice appear as commuting
conversions or require syntactic refinements such as dual-context systems. From this
perspective, the proof theory and the semantics are tightly linked: the difficulties in
designing natural deduction systems reflect precisely the structural constraints needed
for a well-behaved categorical model.
Perhaps more importantly, the work highlighted that the design of constructive modal
logics inevitably involves a number of nontrivial choices. Different assumptions about
the interaction of □ and ◇ with logical connectives, lead to different but equally
reasonable systems. Recognizing this helped reveal the broader landscape of
intuitionistic modal logics, a landscape that was explored in Alex Simpson’s doctoral
thesis The Proof Theory and Semantics of Intuitionistic Modal Logic (1994).
Design choices in constructive modality
One lesson that emerged early on is that constructive modal logic is not a single
system but rather a family of possible systems. When working constructively one must
decide, for example:
how modal operators interact with implication
which modal principles remain valid intuitionistically
how proofs involving modalities should be structured
what kind of semantics best captures the intended meaning
Different answers to these questions lead to different logics, each suitable for different
applications. Exploring this design space became an ongoing theme of my work and
collaborations.
Workshops and collaborations
Over the years, I organized several workshops and participated in many discussions
devoted to constructive modal logics. These meetings brought together researchers
from logic, type theory, and computer science, and they helped shape the direction of
the field. Much of the progress in understanding these systems emerged from these
exchanges: comparing proof systems, refining semantics, and exploring connections
with programming languages and categorical logic. From time to time, I have also
returned to these questions in blog posts as well as papers. Some of these posts
reflect on the motivations behind constructive modal logics and the choices that arise
when designing them:
Each of these revisits the same central theme from a slightly different perspective.
Over the years this line of work expanded well beyond a single logic or a single paper.
The blog post “Papers about constructive modal logics” collects seventeen papers
written across decades exploring different aspects of modality in constructive settings.
While many of them deal directly with intuitionistic modal logics, others investigate
related modal formalisms including hybrid logics, temporal logics, and description
logics.
What unifies these papers is not a single system but a shared perspective:
understanding how modal notions interact with constructive reasoning, and how
these interactions affect proof theory, semantics, and applications in computer science.
Seen together, these papers trace a research program that gradually explored the
many different ways modality can be incorporated into constructive logical
frameworks.
Looking forward
The interaction between modality and constructive reasoning continues to be rich and
subtle. Modal operators appear naturally in many areas connected with computation
and semantics, and intuitionistic logic remains the natural framework for many of these
applications. As a result, the questions that motivated the early work have not
disappeared. If anything, they have become even more relevant as connections
between logic, type theory, and category theory continue to deepen.
This line of work also continues through the community that has formed around
intuitionistic modal logic. Together with Sonia Marin, I am currently organizing another
IMLA — Intuitionistic Modal Logic and Applications 2026 workshop, which will take place as
part of the Federated Logic Conference (FLoC) 2026 in Lisbon this July. We hope the
workshop will bring together many of the different strands of research in the area—
proof theory, semantics, type theory, and applications—and that it will showcase
several of the traditions that have developed around intuitionistic and constructive
modal logics over the years.
Looking back, it is satisfying to see how a question first explored in the early 1990s
grew into a sustained line of work involving many people and ideas. Constructive
modal logics remain a lively area of research, and the design space they reveal is still
far from fully explored.
No comments:
Post a Comment