Definition

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.

Motivation

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.

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

In mathematics, the Peano axioms (or Peano postulates) are a set of first-order axioms proposed by Giuseppe Peano which determine the theory of Peano arithmetic (also known as first-order arithmetic). ... In foundations of mathematics, Von Neumann-Bernays-Gödel set theory (NBG) is an axiom system for set theory designed to yield the same results as Zermelo-Fraenkel set theory, together with the axiom of choice (ZFC), but with only a finite number of axioms, that is without axiom schemas. ... The Zermelo-Fraenkel axioms of set theory (ZF) are the standard axioms of axiomatic set theory on which, together with the axiom of choice, all of ordinary mathematics is based in modern formulations. ...

See also

relative consistency

Links

The importance of conservative extensions for the foundations of mathematics