Uniqueness of axiomatic extensions of cut-free classical propositional logic

In this paper, we prove that, for any cluster of extra-logical assumptions, there exists exactly one axiomatic (i.e., minimal) extension of classical propositional logic that admits cut elimination. As a corollary, it follows that classically equivalent formulas share the same axiomatization. The moral is that cut elimination “flattens” the specific information encoded by the logical structure of proper axioms.