In mathematical logic, a conservative extension is a supertheory of a theory which is often convenient for proving theorems, but proves no new theorems about the language of the original theory. Similarly, a non-conservative extension, or proper extension, is a supertheory which is not conservative, and can prove more theorems than the original. More formally stated, a theory T2 is a (proof theoretic) conservative extension of a theory T1 if every theorem of T1 is a theorem of T2, and any theorem of T2 in the language of T1 is already a theorem of T1. More generally, if Γ is a set of formulas in the common language of T1 and T2, then T2 is Γ-conservative over T1 if every formula from Γ provable in T2 is also provable in T1. Note that a conservative extension of a consistent theory is consistent. If it were not, then by the principle of explosion, every formula in the language of T2 would be a theorem of T2, so every formula in the language of T1 would be a theorem of T1, so T1 would not be consistent. Hence, conservative extensions do not bear the risk of introducing new inconsistencies. This can also be seen as a methodology for writing and structuring large theories: start with a theory, T0, that is known (or assumed) to be consistent, and successively build conservative extensions T1, T2, … of it. Recently, conservative extensions have been used for defining a notion of module for ontologies: if an ontology is formalized as a logical theory, a subtheory is a module if the whole ontology is a conservative extension of the subtheory.
Examples ACA0, a subsystem of second-order arithmetic studied in reverse mathematics, is a conservative extension of first-order Peano arithmetic. The subsystems of second-order arithmetic RCA∗0 and WKL∗0 are Π02-conservative over EFA. The subsystem WKL0 is a Π11-conservative extension of RCA0, and a Π02-conservative over PRA. NBG is a conservative extension of ZFC (= ZF+AC). Internal set theory is a conservative extension of ZFC. Extensions by definitions are conservative. Extensions by unconstrained predicate or function symbols are conservative. IΣ1 (a subsystem of Peano arithmetic with induction only for Σ01-formulas) is a Π02-conservative extension of PRA. ZFC is a Π14-conservative extension of ZF by Shoenfield's absoluteness theorem. ZFC with the generalized continuum hypothesis is a Π21-conservative extension of ZFC.
Model-theoretic conservative extension
With model-theoretic means, a stronger notion is obtained: an extension T2 of a theory T1 is model-theoretically conservative if T1 ⊆ T2 and every model of T1 can be expanded to a model of T2. Each model-theoretic conservative extension also is a (proof-theoretic) conservative extension in the above sense. The model theoretic notion has the advantage over the proof theoretic one that it does not depend so much on the language at hand; on the other hand, it is usually harder to establish model theoretic conservativity.
See also Extension by new constant and function names Admissible rule
References
External links The importance of conservative extensions for the foundations of mathematics