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 $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^{[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.

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

Examples

${\mathsf {ACA}}_{0}$ , 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 ${\mathsf {RCA}}_{0}^{*}$ and ${\mathsf {WKL}}_{0}^{*}$ are $\Pi _{2}^{0}$ -conservative over ${\mathsf {EFA}}$ .^[1]
The subsystem ${\mathsf {WKL}}_{0}$ is a $\Pi _{1}^{1}$ -conservative extension of ${\mathsf {RCA}}_{0}$ , and a $\Pi _{2}^{0}$ -conservative over ${\mathsf {PRA}}$ (primitive recursive arithmetic).^[1]
Von Neumann–Bernays–Gödel set theory ( ${\mathsf {NBG}}$ ) is a conservative extension of Zermelo–Fraenkel set theory with the axiom of choice ( ${\mathsf {ZFC}}$ ).
Internal set theory is a conservative extension of Zermelo–Fraenkel set theory with the axiom of choice ( ${\mathsf {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 _{1}^{0}$ -formulas) is a $\Pi _{2}^{0}$ -conservative extension of ${\mathsf {PRA}}$ .^[2]
${\mathsf {ZFC}}$ is a $\Sigma _{3}^{1}$ -conservative extension of ${\mathsf {ZF}}$ by Shoenfield's absoluteness theorem.
${\mathsf {ZFC}}$ with the continuum hypothesis is a $\Pi _{1}^{2}$ -conservative extension of ${\mathsf {ZFC}}$ .^{[citation needed]}

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.

References

^ ^a ^b S. G. Simpson, R. L. Smith, "Factorization of polynomials and $\Sigma _{1}^{0}$ -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

The importance of conservative extensions for the foundations of mathematics

Mathematical logic

General

Theorems (list)
and paradoxes

Gödel's completeness and incompleteness theorems
Tarski's undefinability
Banach–Tarski paradox
Cantor's theorem, paradox and diagonal argument
Compactness
Halting problem
Lindström's
Löwenheim–Skolem
Russell's paradox

Logics

Traditional	Classical logic Logical truth Tautology Proposition Inference Logical equivalence Consistency Equiconsistency Argument Soundness Validity Syllogism Square of opposition Venn diagram
Propositional	Boolean algebra Boolean functions Logical connectives Propositional calculus Propositional formula Truth tables Many-valued logic 3 finite ∞
Predicate	First-order list Second-order Monadic Higher-order Fixed-point Free Quantifiers Predicate Monadic predicate calculus

Set theory

Set hereditary Class (Ur-)Element Ordinal number Extensionality Forcing Relation equivalence partition Set operations: intersection union complement Cartesian product power set identities
Types of sets	Countable Uncountable Empty Inhabited Singleton Finite Infinite Transitive Ultrafilter Recursive Fuzzy Universal Universe constructible Grothendieck Von Neumann
Maps and cardinality	Function/Map domain codomain image In/Sur/Bi-jection Schröder–Bernstein theorem Isomorphism Gödel numbering Enumeration Large cardinal inaccessible Aleph number Operation binary
Set theories	Zermelo–Fraenkel axiom of choice continuum hypothesis General Kripke–Platek Morse–Kelley Naive New Foundations Tarski–Grothendieck Von Neumann–Bernays–Gödel Ackermann Constructive

Formal systems (list),
language and syntax

Alphabet Arity Automata Axiom schema Expression ground Extension by definition conservative Relation Formation rule Grammar Formula atomic closed ground open Free/bound variable Language Metalanguage Logical connective ¬ ∨ ∧ → ↔ = Predicate functional variable propositional variable Proof Quantifier ∃ ! ∀ rank Sentence atomic spectrum Signature String Substitution Symbol function logical/constant non-logical variable Term Theory list
Example axiomatic systems (list)	of arithmetic: Peano second-order elementary function primitive recursive Robinson Skolem of the real numbers Tarski's axiomatization of Boolean algebras canonical minimal axioms of geometry: Euclidean: Elements Hilbert's Tarski's non-Euclidean Principia Mathematica