Conservative extension
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 [math]\displaystyle{ T_2 }[/math] is a (proof theoretic) conservative extension of a theory [math]\displaystyle{ T_1 }[/math] if every theorem of [math]\displaystyle{ T_1 }[/math] is a theorem of [math]\displaystyle{ T_2 }[/math], and any theorem of [math]\displaystyle{ T_2 }[/math] in the language of [math]\displaystyle{ T_1 }[/math] is already a theorem of [math]\displaystyle{ T_1 }[/math].
More generally, if [math]\displaystyle{ \Gamma }[/math] is a set of formulas in the common language of [math]\displaystyle{ T_1 }[/math] and [math]\displaystyle{ T_2 }[/math], then [math]\displaystyle{ T_2 }[/math] is [math]\displaystyle{ \Gamma }[/math]-conservative over [math]\displaystyle{ T_1 }[/math] if every formula from [math]\displaystyle{ \Gamma }[/math] provable in [math]\displaystyle{ T_2 }[/math] is also provable in [math]\displaystyle{ 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]\displaystyle{ T_2 }[/math] would be a theorem of [math]\displaystyle{ T_2 }[/math], so every formula in the language of [math]\displaystyle{ T_1 }[/math] would be a theorem of [math]\displaystyle{ T_1 }[/math], so [math]\displaystyle{ 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]\displaystyle{ T_0 }[/math], that is known (or assumed) to be consistent, and successively build conservative extensions [math]\displaystyle{ T_1 }[/math], [math]\displaystyle{ 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.
An extension which is not conservative may be called a proper extension.
Examples
- [math]\displaystyle{ \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]\displaystyle{ \mathsf{RCA}_0^* }[/math] and [math]\displaystyle{ \mathsf{WKL}_0^* }[/math] are [math]\displaystyle{ \Pi_2^0 }[/math]-conservative over [math]\displaystyle{ \mathsf{EFA} }[/math].[1]
- The subsystem [math]\displaystyle{ \mathsf{WKL}_0 }[/math] is a [math]\displaystyle{ \Pi_1^1 }[/math]-conservative extension of [math]\displaystyle{ \mathsf{RCA}_0 }[/math], and a [math]\displaystyle{ \Pi_2^0 }[/math]-conservative over [math]\displaystyle{ \mathsf{PRA} }[/math] (primitive recursive arithmetic).[1]
- Von Neumann–Bernays–Gödel set theory ([math]\displaystyle{ \mathsf{NBG} }[/math]) is a conservative extension of Zermelo–Fraenkel set theory with the axiom of choice ([math]\displaystyle{ \mathsf{ZFC} }[/math]).
- Internal set theory is a conservative extension of Zermelo–Fraenkel set theory with the axiom of choice ([math]\displaystyle{ \mathsf{ZFC} }[/math]).
- Extensions by definitions are conservative.
- Extensions by unconstrained predicate or function symbols are conservative.
- [math]\displaystyle{ I\Sigma_1 }[/math] (a subsystem of Peano arithmetic with induction only for [math]\displaystyle{ \Sigma^0 1 }[/math]-formulas) is a [math]\displaystyle{ \Pi^0_2 }[/math]-conservative extension of [math]\displaystyle{ \mathsf{PRA} }[/math].[2]
- [math]\displaystyle{ \mathsf{ZFC} }[/math] is a [math]\displaystyle{ \Sigma^1 3 }[/math]-conservative extension of [math]\displaystyle{ \mathsf{ZF} }[/math] by Shoenfield's absoluteness theorem.
- [math]\displaystyle{ \mathsf{ZFC} }[/math] with the continuum hypothesis is a [math]\displaystyle{ \Pi^2_1 }[/math]-conservative extension of [math]\displaystyle{ \mathsf{ZFC} }[/math].[citation needed]
Model-theoretic conservative extension
With model-theoretic means, a stronger notion is obtained: an extension [math]\displaystyle{ T_2 }[/math] of a theory [math]\displaystyle{ T_1 }[/math] is model-theoretically conservative if [math]\displaystyle{ T_1 \subseteq T_2 }[/math] and every model of [math]\displaystyle{ T_1 }[/math] can be expanded to a model of [math]\displaystyle{ T_2 }[/math]. 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
References
- ↑ 1.0 1.1 S. G. Simpson, R. L. Smith, "Factorization of polynomials and [math]\displaystyle{ \Sigma_1^0 }[/math]-induction" (1986). Annals of Pure and Applied Logic, vol. 31 (p.305)
- ↑ Fernando Ferreira, A Simple Proof of Parsons' Theorem. Notre Dame Journal of Formal Logic, Vol.46, No.1, 2005.
- ↑ Hodges, Wilfrid (1997). A shorter model theory. Cambridge: Cambridge University Press. p. 58 exercise 8. ISBN 978-0-521-58713-6
External links
 |  |
