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.
Contents
More formally stated, a theory
More generally, if
Note that a conservative extension of a consistent theory is consistent. [If it were not, then by the principle of explosion ("everything follows from a contradiction"), every theorem in the original theory as well as its negation would belong to the new theory, which then would not be a conservative extension.] 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,
The theorem provers Isabelle and ACL2 adopt this methodology by providing a language for conservative extensions by definition.
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
Model-theoretic conservative extension
With model-theoretic means, a stronger notion is obtained: an extension