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

 

Threads, Not Tallies

 

A standard story in proof theory textbooks says that an intuitionistic sequent calculus is obtained from a classical one by imposing a single-conclusion restriction. Gentzen’s LJ arises from LK by allowing at most one formula in the succedent. From this, many readers conclude that constructivism is about cardinality: classical logic allows multiple conclusions; intuitionistic logic does not.

The story is convenient.

It is also misleading.

Since Maehara (1954), and as emphasized by Takeuti, Kleene and Dragalin, it has been known that intuitionistic logic can be presented with multiple-conclusion sequents. What these systems retain is not a global restriction, but a local one: implication introduction (and ∀-introduction) may only be applied when the succedent contains a single formula.

If that local restriction is dropped outright, the system collapses into classical logic.

So if constructivism is not about single conclusions, what is it about?

---

From Cardinality to Dependency

In A Short Note on Intuitionistic Propositional Logic with Multiple Conclusions, Luiz Carlos Pereira and I propose a different answer.

The motivation came from work with Martin Hyland on Full Intuitionistic Linear Logic. In trying to formulate a genuinely intuitionistic linear system with multiple conclusions, we were forced to isolate what actually prevents classical collapse.

The answer is simple. In the system FIL (Full Intuitionistic Logic):

• Multiple formulas are allowed in the succedent.

• There are no global or local cardinality restrictions.

• The provable formulas are exactly those of LJ.

What changes is not what can be proved, but how dependency is tracked.

Each assumption in the antecedent is indexed.
Each formula in the succedent carries the set of indices on which it depends.

Implication introduction on the right has the usual form

with one condition: 

The index of the  discharged assumption $A$ must not occur in the dependency set of any formula in $\mathrm{\Delta }$.

In other words:

Implication introduction isolates a dependency thread. It must not leak into parallel branches.

The Smallest Collapse

The force of this condition appears immediately.

Start with an indexed assumption:

$$1\!:\!A \;\vdash\; 1\!:\!$$

Now add $\bot$ on the right (with no dependencies):

$$1\!:\!A \;\vdash\; 1\!:\!A, \bo$$

Here the first succedent formula depends on assumption 1; $\bot$ depends on nothing.

Now attempt to abstract over $A$  on ⊥ to introduce implication on the right.

This is illegal.

The rule requires that the index of the discharged assumption 1 not appear in the dependency set of any side formula. But the side formula $1\!:\!A$ still carries index 1.

The dependency thread has not been isolated. The abstraction is blocked.

Nothing classical has been invoked. Just an attempt to abstract while keeping the assumption active elsewhere.

That tiny forbidden move is precisely the seam through which classical reasoning would otherwise enter, in the shape of the excluded middle:   

     

What Changes — and What Doesn’t

FIL proves exactly the same formulas as LJ. At the level of theorems, nothing changes.

What changes is the explanation.

Constructivism is not about limiting how many conclusions appear on the right. It is about ensuring that implication behaves like function formation. When we abstract over an assumption, the resulting proof must form a coherent functional thread, independent of others.

The single-conclusion restriction enforced this indirectly. Explicit dependency control makes the mechanism visible.  

 

In Retrospect

When this work first appeared in the mid-1990s and then in 2005, it seemed modest: a reformulation of intuitionistic propositional logic showing that single-conclusion restrictions are not essential.

In hindsight, it looks different.

The same idea — controlling discharge by tracking dependency explicitly — reappears naturally in intuitionistic linear logic, in modal systems, and in intermediate logics.

What began as a technical clarification begins to look structural.

Instead of treating constructivism as a syntactic restriction or a list of forbidden principles (no excluded middle, no double negation), we can see it as a discipline governing how dependency threads are formed, discharged, and kept independent.

Threads, not tallies.

 A health warning: The notion of dependency here is not the same as in Martin-Löf's  Dependent Type Theory, nor the same as in the model-theoretic  Dependence Logic of Väänänen's.

Learning from Penelope

 

In Homer’s Odyssey, Penelope survives not by force, but by craft.

She weaves by day and unweaves by night. The weaving keeps the suitors at bay; the unweaving buys her time. It is not indecision. It is strategy. It is control over her own narrative.

I have decided to learn from Penelope.

Over the next months (or years), I will be rewriting my old papers.

Not because the mathematics is wrong.
Not because the results no longer matter.
But because I was — and perhaps still am — a lousy communicator.

Many of my early papers were written quickly, defensively, or under constraints that now feel foreign: editorial fashions,  page limits, the pressure to “fit” a venue. Many were published behind paywalls that I cannot even access anymore, given the lack of institutional support. The irony is not lost on me: I cannot easily read my own work. And cannot point others to it.

Commercial publishing has made something strange happen in mathematics. We produce knowledge collectively, mostly publicly funded, then hand it over to companies who sell it back to us. The system has normalized the idea that authors do not own access to their own intellectual labor. That should trouble us more than it does.

But this project is not primarily about protest.

It is about clarity.

If I am serious about Network Mathematics, and about mathematics as a way of life — about extracting structure from the literature while also living responsibly within it — then my own work should not be an obstacle. It should not require insider knowledge to decode. It should not assume a reader who already knows what I mean to say. So I am weaving again.

I will rewrite old papers as arXiv preprints: With clearer motivations. With expanded explanations. With better examples. With connections made explicit. With historical context where I once assumed it was obvious. With diagrams where prose struggles. With prose where diagrams obscure.

Some papers may be gently revised. Some may be substantially reorganized.
Some may need to be undone and rewoven almost entirely.

This is not repudiation. It is evolution.

Mathematics deserves expository care. Ideas deserve to be legible beyond the circle that first conceived them. And younger researchers — including my younger self — deserve texts that do not require deciphering as a rite of passage.

Penelope’s weaving was an act of resistance. Mine is an act of responsibility.

If you have ever read one of my older papers and thought, “I suspect there’s something important here, but I wish it were clearer,” this project is for you. If you have ever struggled to access your own published work, this project is for you. If you believe that clarity is not a concession but a form of rigour, then perhaps this project is for all of us.

I am unweaving.

So that I can weave again.

Manels and their effects (on my health)

 

Maybe you haven't heard about `Manels'? As Gemini explains: A "manel" is a panel of professionals, often at conferences or in media, composed entirely of men. It is often seen as a failure of diversity, equity, and inclusion (DEI), implying that women are either not qualified to contribute or that their perspectives are unnecessary.

 

One of the most widely cited and "outrageous" examples of a manel in the context of reproductive health occurred in 2017. A group of approximately 25 Republican men was photographed in the White House discussing a healthcare bill that included significant changes to pregnancy and maternity care, as well as the defunding of Planned Parenthood. The image became a viral symbol of the exclusion of women from the very policies that govern their bodies and lives, according to the BBC.

Yes, I know that one is not supposed to talk about DEI in the USA in 2026. Even the word "women" can get your research project proposal disqualified! Still, it took me a while to construct the email message below about manels in my kind of research and I want to be able to point people to it.

 

On all male programs and PCs (again)

---

Dear colleagues,

I’m writing to raise—yet again—an issue that many of us encounter with dispiriting regularity: conferences, workshops, and events in logic whose visible leadership is overwhelmingly male—whether in the form of all-male (or nearly all-male) invited speaker lineups, all-male program committees, or both.

I want to be explicit about scope. I am not interested in debating whether particular cases are “small,” “technical,” or “too specialized.” That line of argument is a familiar slippery slope, and in practice it serves to normalize exclusion rather than to explain it. In logic, there is no shortage of qualified women across areas. When both the speaker list and the PC skew heavily male, that reflects choices made during organization.

All-male programs and PCs are not neutral. Together, they send a clear signal about who is seen as authoritative, who is entrusted with gatekeeping roles, and who is assumed to represent the field. These signals accumulate: they shape visibility, invitations, evaluation practices, and ultimately who feels that they belong.

Organizers sometimes respond that exclusions are unintentional. That may be true—but unintentional bias is still bias, and its effects are not softened by good intentions. Organizing an event involves two clear points of intervention where effort can make a real difference:

1. Who is invited to speak, and

2. Who is asked to serve on the program committee or equivalent decision-making body.

Both are acts of curation and judgment, and both come with responsibility.

I also want to stress that this conversation is specifically about our mailing list, women-in-logic. This list is not moderated, many of us do not have the time or energy to act as moderators. But that does not mean we have to accept, circulate, or normalize calls for papers or announcements that reproduce the same exclusionary patterns we see on generic mailing lists. Setting expectations about what is acceptable here matters.

I would like to encourage two simple norms:

1. That we call attention—politely but explicitly—when all-male or overwhelmingly male speaker lineups or PCs are announced or promoted in our community spaces.

2. That diversity among both speakers and PCs be treated as a basic quality check, not an optional extra or a last-minute fix.

Speaking up can feel awkward, especially when omissions are framed as oversights. But silence signals acceptance, and acceptance ensures repetition.

If others on this list are willing to share strategies that have worked—especially around PC formation as well as speaker selection—I think that would be extremely valuable.

Best regards,
Valeria

---