A Logical Framework Perspective on Conservativity

Conservative extension is one of the most important concepts in formal logic, capturing the intuition when an extension does not substantially change the extended language or theory. Multiple non-equivalent definitions have emerged, including conceptually very different ones in proof and model theory. We use a logical framework that allows stating these notions in a logic-independent way. This allows proving several meta-theorems that yield new intuitions about conservativity: The existence of the different notions of conservativity is neither a coincidence nor a defect: we recover them as canonical points on a spectrum of gradual refinement from syntax to semantics. Moreover, the model and proof-theoretical notions correspond to the well-known difference between admissible and derivable rules. Finally, we can formally capture that the completeness of a logic corresponds to the conservativity of its semantics. All results are intuitively simple but have previously not been stated rigorously and in full generality.