In this article, 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.
- Axiomatic extensions
- Cut elimination with proper axioms
- Logic of pivotal assumptions
- Proof theory