Conservative extension

Wikipedia

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,[citation needed] is a supertheory which is not conservative, and can prove more theorems than the original.

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

More generally, if is a set of formulas in the common language of and , then is -conservative over if every formula from provable in is also provable in .

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 would be a theorem of , so every formula in the language of would be a theorem of , so 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, , that is known (or assumed) to be consistent, and successively build conservative extensions , , ... of it.

Recently, conservative extensions have been used for defining a notion of module for ontologies[citation needed]: 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

Model-theoretic conservative extension

With model-theoretic means, a stronger notion is obtained: an extension of a theory is model-theoretically conservative if and every model of can be expanded to a model of . Each model-theoretic conservative extension also is a (proof-theoretic) conservative extension in the above sense.[5] 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

References

  1. 1 2 S. G. Simpson, R. L. Smith, "Factorization of polynomials and -induction" (1986). Annals of Pure and Applied Logic, vol. 31 (p.305)
  2. Fernando Ferreira, A Simple Proof of Parsons' Theorem. Notre Dame Journal of Formal Logic, Vol.46, No.1, 2005.
  3. Michael Rathjen, Power Kripke-Platek set theory and the axiom of choice. Journal of Logic and Computation, Vol.30, No.1, 2018.
  4. Richard Platek, Eliminating the continuum hypothesis. The Journal of Symbolic Logic, Vol.36, No.1, 1969.
  5. Hodges, Wilfrid (1997). A shorter model theory. Cambridge: Cambridge University Press. p. 58 exercise 8. ISBN 978-0-521-58713-6.