Classical Harmony and Separability

According to logical inferentialists, the meanings of logical expressions are fully determined by the rules for their correct use. Two key proof-theoretic requirements on admissible logical rules, harmony and separability, directly stem from this thesis—requirements, however, that standard single-conclusion and assertion-based formalizations of classical logic provably fail to satisfy (Dummett in The logical basis of metaphysics, Harvard University Press, Harvard, MA, 1991; Prawitz in Theoria, 43:1–40, 1977; Tennant in The taming of the true, Oxford University Press, Oxford, 1997; Humberstone and Makinson in Mind 120(480):1035–1051, 2011). On the plausible assumption that our logical practice is both single-conclusion and assertion-based, it seemingly follows that classical logic, unlike intuitionistic logic, can’t be accounted for in inferentialist terms. In this paper, I challenge orthodoxy and introduce an assertion-based and single-conclusion formalization of classical propositional logic that is both harmonious and separable. In the framework I propose, classicality emerges as a structural feature of the logic.