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.