Inmathematical logic, aconservative extension is asupertheory of atheory which is often convenient for provingtheorems, but proves no new theorems about the language of the original theory. Similarly, anon-conservative extension is a supertheory which is not conservative, and can prove more theorems than the original.

More formally stated, a theory${\displaystyle T_2}$ is a (proof theoretic) conservative extension of a theory${\displaystyle T_1}$ if every theorem of${\displaystyle T_1}$ is a theorem of${\displaystyle T_2}$, and any theorem of${\displaystyle T_2}$ in the language of${\displaystyle T_1}$ is already a theorem of${\displaystyle T_1}$.

More generally, if${\displaystyle \mathrm{\Gamma }}$ is a set offormulas in the common language of${\displaystyle T_1}$ and${\displaystyle T_2}$, then${\displaystyle T_2}$ is${\displaystyle \mathrm{\Gamma }}$-conservative over${\displaystyle T_1}$ if every formula from${\displaystyle \mathrm{\Gamma }}$ provable in${\displaystyle T_2}$ is also provable in${\displaystyle T_1}$.

Note that a conservative extension of aconsistent theory is consistent. If it were not, then by theprinciple of explosion, every formula in the language of${\displaystyle T_2}$ would be a theorem of${\displaystyle T_2}$, so every formula in the language of${\displaystyle T_1}$ would be a theorem of${\displaystyle T_1}$, so${\displaystyle T_1}$ would not be consistent. Hence, conservative extensions do not bear the risk of introducing new inconsistencies. This can also be seen as amethodology for writing and structuring large theories: start with a theory,${\displaystyle T_0}$, that is known (or assumed) to be consistent, and successively build conservative extensions${\displaystyle T_1}$,${\displaystyle T_2}$, ... of it.

Recently, conservative extensions have been used for defining a notion ofmodule forontologies^{[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 aproper extension.

• ${\displaystyle {\mathsf{A}\mathsf{C}\mathsf{A}}_0}$, a subsystem ofsecond-order arithmetic studied inreverse mathematics, is a conservative extension of first-orderPeano arithmetic.
• Thesubsystems of second-order arithmetic${\displaystyle {\mathsf{R}\mathsf{C}\mathsf{A}}_0^{\ast }}$ and${\displaystyle {\mathsf{W}\mathsf{K}\mathsf{L}}_0^{\ast }}$ are${\displaystyle {\mathrm{\Pi }}_2^0}$-conservative over${\displaystyle \mathsf{E}\mathsf{F}\mathsf{A}}$.^[1]
• The subsystem${\displaystyle {\mathsf{W}\mathsf{K}\mathsf{L}}_0}$ is a${\displaystyle {\mathrm{\Pi }}_1^1}$-conservative extension of${\displaystyle {\mathsf{R}\mathsf{C}\mathsf{A}}_0}$, and a${\displaystyle {\mathrm{\Pi }}_2^0}$-conservative over${\displaystyle \mathsf{P}\mathsf{R}\mathsf{A}}$ (primitive recursive arithmetic).^[1]
• Von Neumann–Bernays–Gödel set theory (${\displaystyle \mathsf{N}\mathsf{B}\mathsf{G}}$) is a conservative extension ofZermelo–Fraenkel set theory with theaxiom of choice (${\displaystyle \mathsf{Z}\mathsf{F}\mathsf{C}}$).
• Internal set theory is a conservative extension ofZermelo–Fraenkel set theory with theaxiom of choice (${\displaystyle \mathsf{Z}\mathsf{F}\mathsf{C}}$).
• Extensions by definitions are conservative.
• Extensions by unconstrained predicate or function symbols are conservative.
• ${\displaystyle I{\mathrm{\Sigma }}_1}$ (a subsystem of Peano arithmetic with induction only for${\displaystyle {\mathrm{\Sigma }}_1^0}$-formulas) is a${\displaystyle {\mathrm{\Pi }}_2^0}$-conservative extension of${\displaystyle \mathsf{P}\mathsf{R}\mathsf{A}}$.^[2]
• ${\displaystyle \mathsf{Z}\mathsf{F}\mathsf{C}}$ is a${\displaystyle {\mathrm{\Sigma }}_3^1}$-conservative extension of${\displaystyle \mathsf{Z}\mathsf{F}}$ byShoenfield's absoluteness theorem.
• ${\displaystyle \mathsf{Z}\mathsf{F}\mathsf{C}}$ with thecontinuum hypothesis is a${\displaystyle {\mathrm{\Pi }}_1^2}$-conservative extension of${\displaystyle \mathsf{Z}\mathsf{F}\mathsf{C}}$.^{[citation needed]}

Withmodel-theoretic means, a stronger notion is obtained: an extension${\displaystyle T_2}$ of a theory${\displaystyle T_1}$ ismodel-theoretically conservative if${\displaystyle T_1\subseteq T_2}$ and every model of${\displaystyle T_1}$ can be expanded to a model of${\displaystyle 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.

• Extension by new constant and function names

• The importance of conservative extensions for the foundations of mathematics

• Mathematical logic
• Model theory
• Proof theory

• Articles with short description
• Short description is different from Wikidata
• All articles with unsourced statements
• Articles with unsourced statements from April 2024
• Articles with unsourced statements from March 2021