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

---