In mathematical logic, a logical theory, T2, is a conservative extension of theory, T1, if any consequence of T2, involving symbols of T1 only, is already a consequence 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 prover Isabelle adopts this methodology by providing a language for conservative extensions by definition.

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.
• 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.

See also: Conservativity theorem

External links

---

• The importance of conservative extensions for the foundations of mathematics

Proof theory