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

More formally stated, a theory <math>T_2</math> is a (proof theoretic) conservative extension of a theory <math>T_1</math> if every theorem of <math>T_1</math> is a theorem of <math>T_2</math>, and any theorem of <math>T_2</math> in the language of <math>T_1</math> is already a theorem of <math>T_1</math>.

More generally, if <math>\Gamma</math> is a set of formulas in the common language of <math>T_1</math> and <math>T_2</math>, then <math>T_2</math> is <math>\Gamma</math>-conservative over <math>T_1</math> if every formula from <math>\Gamma</math> provable in <math>T_2</math> is also provable in <math>T_1</math>.

Note that a conservative extension of a consistent theory is consistent. If it were not, then by the principle of explosion, every formula in the language of <math>T_2</math> would be a theorem of <math>T_2</math>, so every formula in the language of <math>T_1</math> would be a theorem of <math>T_1</math>, so <math>T_1</math> would not be consistent. 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, <math>T_0</math>, that is known (or assumed) to be consistent, and successively build conservative extensions <math>T_1</math>, <math>T_2</math>, ... of it.

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.

Examples

  • <math>\mathsf{ACA}_0</math>, a subsystem of second-order arithmetic studied in reverse mathematics, is a conservative extension of first-order Peano arithmetic.
  • The subsystems of second-order arithmetic <math>\mathsf{RCA}_0^*</math> and <math>\mathsf{WKL}_0^*</math> are <math>\Pi_2^0</math>-conservative over <math>\mathsf{EFA}</math>.
  • The subsystem <math>\mathsf{WKL}_0</math> is a <math>\Pi_1^1</math>-conservative extension of <math>\mathsf{RCA}_0</math>, and a <math>\Pi_2^0</math>-conservative over <math>\mathsf{PRA}</math> (primitive recursive arithmetic).
  • <math>\mathsf{ZFC}</math> is a <math>\Pi^1_4</math>-conservative extension of <math>\mathsf{ZF}</math> by Shoenfield's absoluteness theorem.
  • <math>\mathsf{ZFC}</math> with the generalized continuum hypothesis is a <math>\Pi^2_1</math>-conservative extension of <math>\mathsf{ZFC}</math>.

Model-theoretic conservative extension

With model-theoretic means, a stronger notion is obtained: an extension <math>T_2</math> of a theory <math>T_1</math> is model-theoretically conservative if <math>T_1 \subseteq T_2</math> and every model of <math>T_1</math> can be expanded to a model of <math>T_2</math>. Each model-theoretic conservative extension also is a (proof-theoretic) conservative extension in the above sense. The model theoretic notion has the advantage over the proof theoretic one that it does not depend so much on the language at hand; on the other hand, it is usually harder to establish model theoretic conservativity.

See also

  • Extension by new constant and function names
  • Admissible rule

References

  • The importance of conservative extensions for the foundations of mathematics