Constructive modal Logics: Again

                                             Gavin Bierman

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:

 

• Why constructive modal logics? (2012)

• Papers about constructive modal logics (2016)

• Intuitionistic modal logic: are you sure? (2025)

   

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.

 

Soundness and completeness are not enough

 This blog post is based on a talk recently given at Chapman University, developed within the context of our joint Topos–Chapman collaboration. I thank the audience for a lively discussion.

Milly Maietti

In the 1990s, intuitionistic linear logic was booming. There were multiple typed calculi, multiple categorical models, and a growing body of results showing soundness and completeness between them.

Everything looked harmonious.

But something subtle was wrong.

In a joint paper with Maria Emilia Maietti, Paola Maneggia, and Eike Ritter, we asked a deceptively simple question:

If two classes of categorical structures are both sound and complete for a typed calculus, are they really the same semantics?

The answer turned out to be NO.

And understanding why required shifting the way we think about categorical semantics.

The landscape: many calculi, many models

By the time we wrote Relating Categorical Semantics for Intuitionistic Linear Logic (2005), there were at least three typed systems in play:

• ILL (Intuitionistic Linear Logic) — with explicit structural operators like let, copy, and discard.
• DILL (Dual Intuitionistic Linear Logic) — using two contexts to separate linear and intuitionistic assumptions.
• LNL (Linear–Non-Linear Logic) — organizing the world via an adjunction between linear and cartesian structure.

On the semantic side, two main model classes were widely used:

• Linear categories (symmetric monoidal closed categories with a suitable comonad).
• Symmetric monoidal adjunctions between cartesian closed and linear categories.

The literature often treated these model classes as essentially equivalent. After all, both were sound and complete for linear logic.

So what was the problem?

The hidden assumption was this: Soundness and completeness identify `the' correct categorical semantics.

But soundness and completeness only tell us that:

• Every derivable statement is valid in the model.
• Every valid statement is derivable in the calculus.

They say nothing about whether the structure of the models matches the structure of the calculus. To see that mismatch, one has to look at something that is often ignored: Model Morphisms.

Organizing everything into categories

Instead of comparing:

• A calculus
• A class of models

We compare:

• The category of theories of a calculus
• The category of models, with structure-preserving morphisms

Once you do that, the real relationships become visible.

And what we discovered was striking:

• The category of linear categories is not equivalent to the category of symmetric monoidal adjunctions.
• Instead, they are related by a reflection.

This is a structural difference, not a minor technicality.

Even though both model classes validate the same theorems of ILL, they do not organize themselves the same way categorically.

Internal language as the criterion

So what should determine the “right” semantics of a calculus?

Our answer was:

A class of models deserves to be called the categorical semantics of a calculus only if the calculus provides its internal language.

This means:

• The category of theories of the calculus is equivalent to the category of models.
• Syntax and semantics match at the level of structure, not just truth.

When we apply this criterion, a clean separation emerges:  

Linear categories have ILL as their internal language. Symmetric monoidal adjunctions do not. Instead, a fragment of LNL provides their internal language.

So although ILL is sound and complete for both model classes, it is the internal language of only one of them. That distinction forces us to rethink what “categorical semantics” really means.

Why this matters today

Looking back, the deeper lesson of the paper is methodological.

It says: Don’t ignore morphisms. Don’t identify semantics via completeness alone. Work at the level of categories of theories and categories of models. Demand internal language equivalence if you want structural alignment.

This shift has implications well beyond linear logic. It applies wherever we relate:

• Syntax and semantics,
• Type theory and category theory,
• Formal systems and their models.

If we only check soundness and completeness, we may miss fundamental structural differences. But if we insist on internal language equivalence, we get a much sharper alignment between syntax and semantics.

A broader theme

At the Topos Institute, we often emphasize that structure matters.

This paper is an early example of that philosophy:

Semantics lives not only in objects, but in the morphisms between them.

When we make morphisms visible, reflections and adjunctions appear. Distinctions that were invisible before become mathematically precise.

And sometimes, what looked like equivalence turns out to be something subtler — and more interesting.

Paola Maneggia

A subtlety: the role of morphisms

There is an important caveat to the story above.

The reflective-subcategory picture depends on what we choose as morphisms of theories and models. If we alter the notion of morphism — for example, allowing preservation up to coherent isomorphism rather than strictly — the comparison may shift. In a fully 2-categorical setting, the distinction between reflection and equivalence can blur. Strict inequivalences may become biequivalences. 

But this does not undermine the main point. It reinforces it: Semantic comparisons only become meaningful once the morphisms are specified. And that specification is itself part of the mathematics.

Conclusion: semantics is a choice

The reflective-subcategory picture we described depends on something that is rarely made explicit:

What counts as a morphism?

• Do theory morphisms preserve structure strictly?
• Or up to coherent isomorphism?
• Are model morphisms strong monoidal functors? Lax?
• Pseudomorphisms in a 2-category?

Change the morphisms, and you may change the comparison. A reflection in one setting might become a biequivalence in another. An apparent inequivalence may dissolve once we pass to the right 2-categorical level.

So was the reflection theorem in the 2005 paper “real”? Or was it an artifact of strictness? Here is the uncomfortable answer:

Categorical semantics is never just about objects. It is about the level of structure at which we choose to work.

And that level is a mathematical decision.

If we stay at the 1-categorical level with strict morphisms, we see a genuine reflective subcategory:

ILL Theories ≃ Linear Categories ↪ SM Adjunctions

If we move to a 2-categorical setting and weaken preservation conditions, some distinctions may blur. But that does not make the earlier result meaningless. It makes it conditional.

And that is the real lesson. When someone says:

“These two notions of model are equivalent.”

The correct response is:

Equivalent in which category? With which morphisms? At what level of coherence?

Until those choices are specified, the statement has no precise mathematical meaning.

Our original paper did not merely compare models of linear logic. It forced those choices into the open. And that, in retrospect, is its lasting contribution. Because once we acknowledge that semantics depends on morphisms, we see something deeper:

Semantics is not discovered. It is structured.

And structuring it correctly is part of the mathematics itself.

                                                         Eike Ritter