# Conservative extension

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 is a supertheory which is not conservative, and can prove more theorems than the original.

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.

An extension which is not conservative may be called a proper extension.

## Examples

- ACA0 (a subsystem of second-order arithmetic) is a conservative extension of first-order Peano arithmetic.
- Von Neumann–Bernays–Gödel set theory is a conservative extension of Zermelo–Fraenkel set theory with the axiom of choice (ZFC).
- Internal set theory is a conservative extension of Zermelo–Fraenkel set theory with the axiom of choice (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 Σ1-formulas) is a Π2-conservative extension of the primitive recursive arithmetic (PRA).
- ZFC is a Π3-conservative extension of ZF by Shoenfield's absoluteness theorem.
- ZFC with the continuum hypothesis is a Π1-conservative extension of ZFC.

## Model-theoretic conservative extension

Credits to the contents of this page go to the authors of the corresponding Wikipedia page: en.wikipedia.org/wiki/Conservative extension.