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

 

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

---

 

Saying good bye to Harold

 Harold wasn't ill, as far as I know. He seemed to be enjoying his life as an avant-guarde musician, and was due to perform two days (or something like it) after he died. I read it in the website of the venue when I tried to learn more. This seems so unfair! 

Harold A. J. M. Schellinx was very, very clever and a good person. He helped me a lot when we were both starting. I finished my doctorate earlier than him, because he did so much for his. I am still trying to learn some of the things he wrote in 1994! Last time I wrote to him, around 2005, I was trying to get him to publish his thesis in Lulu. Amazon said it had one copy for more than 200 dollars and I said it would be nice if he did republish it. He replied that he still had plenty of copies and if I knew someone who wanted it, I should give them his email. Fair enough.

Harold could have destroyed my career, if he wanted to. He found a big hole in my work and helped me to try to fill it. Which I did, many years later. Andreja Prijatelj was a common friend, who departed  earlier in 2002.

I started this post in September, when I heard the bad news from Jean-Baptiste, via Luiz Carlos. It hurt. Much more than when I heard about Thomas Streicher. At least I had had a chance to catch up with Thomas in Padova, to have lunch and chat about the world with him. I don't think he knew already about his disease. I didn't, for sure, and thought it was only a lovely chat after so many years apart. And that this would become more part of my life now that I only work on things I want to. Little did I know that this was the last time I would see him alive.

But Christmas is the season for ghost stories and for self-recrimination. And  I do have these in spades. I don't mean in epic proportions, like Dicken's `The Christmas Carol' Scrooge, but it feels really heavy right now. I guess it happens to everyone,  reason why the holidays can be so fun and at the same time so sad, so difficult to survive! All that I need to do is be less self-centered, think more of others, understand better what matters to them and act on it. It shouldn't be so hard. (One thing I like about myself is the very Brazilian habit of always thinking we can do it, that there is always new chances and new beginnings).

Ada Lovelace Day 2025

 

 

 Phew! I almost completely missed it! This year's Ada Lovelace heroes are Larisa Maksimova and Ewa Orlowska. Someone once said (and I repeated it dozens of times in talks and in writing) that starting a project is easy; difficult is keeping it up, year after year.  Maintenance is much harder than starting new things. It's not sexy, I can be very boring. I seem to be falling prey to this difficulty now. I have been doing Ada Lovelace Day posts since 2011. Nowadays it should be easier, since I can decide what I want to be working on. But instead it is turning harder: focusing on projects and finishing them off turns out harder if you make your own deadlines.

Anyways, as usual, better late than never. This year, I went back to basics and chose two mathematical logicians, as it was the original goal.  When I was growing up, I had the impression that many logicians, especially from the Iron Curtain countries, were women. They seemed established professionals; they looked much older than the corresponding authors from the West. They also morphed into a jumbled mass in my head. Now I realize the huge differences in subjects, approaches, cultures, etc.  Now I feel that I should try to learn the history of logic/mathematics and its nuances, checking out all the manipulations of  the winners, who write the (lack of) history. (Yes, we have a project on history of Mathematics in the BRICS countries, I have much to learn from my historian friends.) Anyways, here goes the two heroes of 2025:

 Larisa Lvovna Maksimova (5 November 1943 – 4 April 2025) was a Russian mathematical logician known for her research in non-classical logic. Sergei Odintsov (kudos to him!) edited  Larisa Maksimova on Implication, Interpolation, and Definability, Outstanding Contributions to Logic, vol. 15,  2018, a festschrift for her. I just bought the book and I hope to learn what she was doing with strict implication!

But to end on a positive note, the second hero is Stella Ewa Orłowska (born 1935),  a Polish logician. Her research centers on the concept that everything in logic and set theory can be expressed in terms of relations, and has used this idea to publish works on deduction systems and model theory for non-classical logic, and logics of non-deterministic and incomplete information. 

Professor  Orłowska has many  books under her name. She also has a festschrift book, pictured below. Just as well, as I could not find a picture of her today. But I do remember seeing several pictures in previous years. According to Google Scholar  professor Orłowska has a 2025 arxiv paper, joint work with Viktor Marek and Ivo Düntsch on Rough Sets. Wonderful to hear!