Conservative extension

From Wikipedia, the free encyclopedia

In mathematical logic, a logical theory, T2, is a conservative extension of a theory T1 if the language of T2 extends the language of T1 and every theorem of T1 is a theorem of T2 and any theorem of T2 which is in the language of T1 is already a theorem of T1.

Informally, the new theory may possibly be more convenient for proving theorems, but it proves no new theorems about the old theory. The importance of this notion lies in the following theorem:

If T2 is a conservative extension of T1, and T1 is consistent, then T2 is consistent as well.

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.

The theorem provers Isabelle and ACL2 adopt this methodology by providing a language for conservative extensions by definition.

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.
Internal set theory is a conservative extension of Zermelo-Fraenkel set theory with the Axiom of choice.
Extensions by predicate or function symbols that are explicitly defined by a formula are conservative.
Extensions by predicate or function symbols that are recursively-defined by a set of formulas are conservative
(provided that the recursion scheme leads to a definition).
Extensions by unconstrained predicate or function symbols are conservative.
Extensions by predicate or function symbols that are axiomatized by a Horn theory are conservative.
Any extension enjoying the model expansion property is conservative.