Conservative extension
Encyclopedia
In mathematical logic
, a logical theory
is a (proof theoretic
) conservative extension of a theory
if the language of 
extends the language of 
; every theorem of 
is a theorem of 
; and any theorem of 
which is 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 
.
To put it informally, the new theory may possibly be more convenient for proving theorem
s, but it proves no new theorems about the language of the old theory.
Note that a conservative extension of a consistent theory is 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.
The theorem provers Isabelle and ACL2 adopt this methodology by providing a language for conservative extensions by definition.
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.
means, a stronger notion is obtained:
is a model-theoretic conservative extension of 
if every model of 
can be expanded to a model of 
. It is straightforward to see that each model-theoretic conservative extension also is a (proof-theoretic) conservative extension in the above sense. 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.
Mathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
, a logical theory
is a (proof theoreticProof theory
Proof theory is a branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as plain lists, boxed lists, or trees, which are constructed...
) conservative extension of a theory
if the language of extends the language of ; every theorem of is a theorem of ; and any theorem of which is 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 .To put it informally, the new theory may possibly be more convenient for proving theorem
Theorem
In mathematics, a theorem is a statement that has been proven on the basis of previously established statements, such as other theorems, and previously accepted statements, such as axioms...
s, but it proves no new theorems about the language of the old theory.
Note that a conservative extension of a consistent theory is consistent. Hence, conservative extensions do not bear the risk of introducing new inconsistencies. This can also be seen as a methodology
Methodology
Methodology is generally a guideline for solving a problem, with specificcomponents such as phases, tasks, methods, techniques and tools . It can be defined also as follows:...
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.The theorem provers Isabelle and ACL2 adopt this methodology by providing a language for conservative extensions by definition.
Recently, conservative extensions have been used for defining a notion of module for ontologies
Ontology (computer science)
In computer science and information science, an ontology formally represents knowledge as a set of concepts within a domain, and the relationships between those concepts. It can be used to reason about the entities within that domain and may be used to describe the domain.In theory, an ontology is...
: 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
- ACA0 (a subsystem of second-order arithmeticSecond-order arithmeticIn mathematical logic, second-order arithmetic is a collection of axiomatic systems that formalize the natural numbers and their subsets. It is an alternative to axiomatic set theory as a foundation for much, but not all, of mathematics. It was introduced by David Hilbert and Paul Bernays in their...
) is a conservative extension of first-order Peano arithmetic. - Von Neumann–Bernays–Gödel set theoryVon Neumann–Bernays–Gödel set theoryIn the foundations of mathematics, von Neumann–Bernays–Gödel set theory is an axiomatic set theory that is a conservative extension of the canonical axiomatic set theory ZFC. A statement in the language of ZFC is provable in NBG if and only if it is provable in ZFC. The ontology of NBG includes...
is a conservative extension of Zermelo–Fraenkel set theoryZermelo–Fraenkel set theoryIn mathematics, Zermelo–Fraenkel set theory with the axiom of choice, named after mathematicians Ernst Zermelo and Abraham Fraenkel and commonly abbreviated ZFC, is one of several axiomatic systems that were proposed in the early twentieth century to formulate a theory of sets without the paradoxes...
(ZF). - Internal set theoryInternal set theoryInternal set theory is a mathematical theory of sets developed by Edward Nelson that provides an axiomatic basis for a portion of the non-standard analysis introduced by Abraham Robinson. Instead of adding new elements to the real numbers, the axioms introduce a new term, "standard", which can be...
is a conservative extension of Zermelo–Fraenkel set theoryZermelo–Fraenkel set theoryIn mathematics, Zermelo–Fraenkel set theory with the axiom of choice, named after mathematicians Ernst Zermelo and Abraham Fraenkel and commonly abbreviated ZFC, is one of several axiomatic systems that were proposed in the early twentieth century to formulate a theory of sets without the paradoxes...
with the axiom of choice (ZFC). - Extensions by definitionsExtension by definitionsIn mathematical logic, more specifically in the proof theory of first-order theories, extensions by definitions formalize the introduction of new symbols by means of a definition. For example, it is common in naive set theory to introduce a symbol \emptyset for the set which has no member...
are conservative. - Extensions by unconstrained predicate or function symbols are conservative.
- IΣ1 (a subsystem of Peano arithmetic with induction only for Σ01-formulasArithmetical hierarchyIn mathematical logic, the arithmetical hierarchy, arithmetic hierarchy or Kleene-Mostowski hierarchy classifies certain sets based on the complexity of formulas that define them...
) is a Π02-conservative extension of the primitive recursive arithmeticPrimitive recursive arithmeticPrimitive recursive arithmetic, or PRA, is a quantifier-free formalization of the natural numbers. It was first proposed by Skolem as a formalization of his finitist conception of the foundations of arithmetic, and it is widely agreed that all reasoning of PRA is finitist...
(PRA). - ZFC is a Π13Analytical hierarchyIn mathematical logic and descriptive set theory, the analytical hierarchy is a higher type analogue of the arithmetical hierarchy. It thus continues the classification of sets by the formulas that define them.-The analytical hierarchy of formulas:...
-conservative extension of ZF by Shoenfield's absoluteness theoremAbsoluteness (mathematical logic)In mathematical logic, a formula is said to be absolute if it has the same truth value in each of some class of structures . Theorems about absoluteness typically establish relationships between the absoluteness of formulas and their syntactic form.There are two weaker forms of partial absoluteness...
. - ZFC with the continuum hypothesisContinuum hypothesisIn mathematics, the continuum hypothesis is a hypothesis, advanced by Georg Cantor in 1874, about the possible sizes of infinite sets. It states:Establishing the truth or falsehood of the continuum hypothesis is the first of Hilbert's 23 problems presented in the year 1900...
is a Π21-conservative extension of ZFC.
Model-theoretic conservative extension
With model-theoreticModel theory
In mathematics, model theory is the study of mathematical structures using tools from mathematical logic....
means, a stronger notion is obtained:
is a model-theoretic conservative extension of if every model of can be expanded to a model of . It is straightforward to see that each model-theoretic conservative extension also is a (proof-theoretic) conservative extension in the above sense. 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.