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