Conservative extension explained

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

More formally stated, a theory

T _{2} is a (proof theoretic) conservative extension of a theory T _{1} if every theorem of T _{1} is a theorem of T _{2} , and any theorem of T _{2} in the language of T _{1} is already a theorem of T _{1} .

More generally, if

\Gamma is a set of formulas in the common language of T _{1} and T _{2} , then T _{2} is \Gamma -conservative over T _{1} if every formula from \Gamma provable in T _{2} is also provable in T _{1} .

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

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

An extension which is not conservative may be called a proper extension.

Examples

ACA _{0} , a subsystem of second-order arithmetic studied in reverse mathematics, is a conservative extension of first-order Peano arithmetic.RCA ^{*} _{0} and WKL ^{*} _{0} are \Pi ^{0} _{2} -conservative over EFA .^[1]

• The subsystem

WKL _{0} is a \Pi ^{1} _{1} -conservative extension of RCA _{0} , and a \Pi ^{0} _{2} -conservative over PRA (primitive recursive arithmetic).

• Von Neumann–Bernays–Gödel set theory (

NBG ) is a conservative extension of Zermelo–Fraenkel set theory with the axiom of choice (ZFC ).

• Internal set theory is a conservative extension of Zermelo–Fraenkel set theory with the axiom of choice (

ZFC ).

• Extensions by definitions are conservative.
• Extensions by unconstrained predicate or function symbols are conservative.

I\Sigma _{1} (a subsystem of Peano arithmetic with induction only for \Sigma ^{0} _{1} -formulas) is a \Pi ^{0} _{2} -conservative extension of PRA .^[2] ZFC is a \Sigma ^{1} _{3} -conservative extension of ZF by Shoenfield's absoluteness theorem.ZFC with the continuum hypothesis is a \Pi ^{2} _{1} -conservative extension of ZFC .

Model-theoretic conservative extension

With model-theoretic means, a stronger notion is obtained: an extension

T _{2} of a theory T _{1} is model-theoretically conservative if T _{1} \subseteq T _{2} and every model of T _{1} can be expanded to a model of T _{2} . Each model-theoretic conservative extension also is a (proof-theoretic) conservative extension in the above sense.^[3] 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 definitions
• Extension by new constant and function names

External links

• The importance of conservative extensions for the foundations of mathematics

Notes and References

1. S. G. Simpson, R. L. Smith, "Factorization of polynomials and \Sigma ^{0} _{1} -induction" (1986). Annals of Pure and Applied Logic, vol. 31 (p.305)
2. https://projecteuclid.org/download/pdfview_1/euclid.ndjfl/1107220675A Fernando Ferreira, A Simple Proof of Parsons' Theorem. Notre Dame Journal of Formal Logic, Vol.46, No.1, 2005.
3. Book: Hodges . Wilfrid . Wilfrid Hodges . A shorter model theory . Cambridge University Press. Cambridge . 978-0-521-58713-6 . 1997 . . 58 exercise 8.