HOME

TheInfoList



OR:

In
mathematical logic Mathematical logic is the study of logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of for ...
, a conservative extension is a supertheory of a
theory A theory is a rational type of abstract thinking about a phenomenon, or the results of such thinking. The process of contemplative and rational thinking is often associated with such processes as observational study or research. Theories may be s ...
which is often convenient for proving
theorem In mathematics, a theorem is a statement that has been proved, or can be proved. The ''proof'' of a theorem is a logical argument that uses the inference rules of a deductive system to establish that the theorem is a logical consequence of th ...
s, 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 science, a formula is a concise way of expressing information symbolically, as in a mathematical formula or a ''chemical formula''. The informal use of the term ''formula'' in science refers to the general construct of a relationship betwee ...
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 In classical deductive logic, a consistent theory is one that does not lead to a logical contradiction. The lack of contradiction can be defined in either semantic or syntactic terms. The semantic definition states that a theory is consistent i ...
theory is consistent. If it were not, then by the
principle of explosion In classical logic, intuitionistic logic and similar logical systems, the principle of explosion (, 'from falsehood, anything ollows; or ), or the principle of Pseudo-Scotus, is the law according to which any statement can be proven from a co ...
, 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 In its most common sense, methodology is the study of research methods. However, the term can also refer to the methods themselves or to the philosophical discussion of associated background assumptions. A method is a structured procedure for bri ...
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 Module, modular and modularity may refer to the concept of modularity. They may also refer to: Computing and engineering * Modular design, the engineering discipline of designing complex devices using separately designed sub-components * Modul ...
for
ontologies In computer science and information science, an ontology encompasses a representation, formal naming, and definition of the categories, properties, and relations between the concepts, data, and entities that substantiate one, many, or all domains ...
: 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 arithmetic In 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. A precurs ...
studied in
reverse mathematics Reverse mathematics is a program in mathematical logic that seeks to determine which axioms are required to prove theorems of mathematics. Its defining method can briefly be described as "going backwards from the theorems to the axioms", in cont ...
, is a conservative extension of first-order
Peano arithmetic In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano. These axioms have been used nearly u ...
. *
Von Neumann–Bernays–Gödel set theory In the foundations of mathematics, von Neumann–Bernays–Gödel set theory (NBG) is an axiomatic set theory that is a conservative extension of Zermelo–Fraenkel–choice set theory (ZFC). NBG introduces the notion of class, which is a collect ...
(NBG) is a conservative extension of
Zermelo–Fraenkel set theory In set theory, Zermelo–Fraenkel set theory, named after mathematicians Ernst Zermelo and Abraham Fraenkel, is an axiomatic system that was proposed in the early twentieth century in order to formulate a theory of sets free of paradoxes such as ...
with the
axiom of choice In mathematics, the axiom of choice, or AC, is an axiom of set theory equivalent to the statement that ''a Cartesian product of a collection of non-empty sets is non-empty''. Informally put, the axiom of choice says that given any collectio ...
(ZFC). *
Internal set theory Internal set theory (IST) is a mathematical theory of sets developed by Edward Nelson that provides an axiomatic basis for a portion of the nonstandard analysis introduced by Abraham Robinson. Instead of adding new elements to the real numbers, Ne ...
is a conservative extension of
Zermelo–Fraenkel set theory In set theory, Zermelo–Fraenkel set theory, named after mathematicians Ernst Zermelo and Abraham Fraenkel, is an axiomatic system that was proposed in the early twentieth century in order to formulate a theory of sets free of paradoxes such as ...
with the
axiom of choice In mathematics, the axiom of choice, or AC, is an axiom of set theory equivalent to the statement that ''a Cartesian product of a collection of non-empty sets is non-empty''. Informally put, the axiom of choice says that given any collectio ...
(ZFC). * Extensions by definitions are conservative. * Extensions by unconstrained predicate or function symbols are conservative. * IΣ1 (a subsystem of Peano arithmetic with induction only for Σ01-formulas) is a Π02-conservative extension of the
primitive recursive arithmetic Primitive recursive arithmetic (PRA) is a quantifier-free formalization of the natural numbers. It was first proposed by Norwegian mathematician , reprinted in translation in as a formalization of his finitist conception of the foundations of ar ...
(PRA). * ZFC is a Σ13-conservative extension of ZF by Shoenfield's absoluteness theorem. * ZFC with the
continuum hypothesis In mathematics, the continuum hypothesis (abbreviated CH) is a hypothesis about the possible sizes of infinite sets. It states that or equivalently, that In Zermelo–Fraenkel set theory with the axiom of choice (ZFC), this is equivalent to ...
is a Π21-conservative extension of ZFC.


Model-theoretic conservative extension

With
model-theoretic In mathematical logic, model theory is the study of the relationship between formal theories (a collection of sentences in a formal language expressing statements about a mathematical structure), and their models (those structures in which the st ...
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. 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 In 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 ...
*
Extension by new constant and function names In mathematical logic, a theory can be extended with new constants or function names under certain conditions with assurance that the extension will introduce no contradiction. Extension by definitions is perhaps the best-known approach, but it req ...


References


External links


The importance of conservative extensions for the foundations of mathematics
{{Mathematical logic Mathematical logic Model theory Proof theory