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 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