 Conservative extension

In mathematical logic, a logical theory T_{2} is a (proof theoretic) conservative extension of a theory T_{1} if the language of T_{2} extends the language of T_{1}; every theorem of T_{1} is a theorem of T_{2}; and any theorem of T_{2} which is in the language of T_{1} is already a theorem of T_{1}.
More generally, if Γ is a set of formulas in the common language of T_{1} and T_{2}, then T_{2} is Γconservative over T_{1}, if every formula from Γ provable in T_{2} is also provable in T_{1}.
To put it informally, the new theory may possibly be more convenient for proving theorems, 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, T_{0}, that is known (or assumed) to be consistent, and successively build conservative extensions T_{1}, T_{2}, ... 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.
Examples
 ACA_{0} (a subsystem of secondorder arithmetic) is a conservative extension of firstorder Peano arithmetic.
 Von Neumann–Bernays–Gödel set theory is a conservative extension of Zermelo–Fraenkel set theory (ZF).
 Internal set theory is a conservative extension of Zermelo–Fraenkel set theory with the axiom of choice (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 Σ^{0}_{1}formulas) is a Π^{0}_{2}conservative extension of the primitive recursive arithmetic (PRA).
 ZFC is a Π^{1}_{3}conservative extension of ZF by Shoenfield's absoluteness theorem.
 ZFC with the continuum hypothesis is a Π^{2}_{1}conservative extension of ZFC.
Modeltheoretic conservative extension
With modeltheoretic means, a stronger notion is obtained: T_{2} is a modeltheoretic conservative extension of T_{1} if every model of T_{1} can be expanded to a model of T_{2}. It is straightforward to see that each modeltheoretic conservative extension also is a (prooftheoretic) 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.
Further information: Conservativity theoremExternal links
Categories:
Wikimedia Foundation. 2010.
Look at other dictionaries:
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… … Wikipedia
Conservative Party (UK) — Conservative Party Conservative and Unionist Party Leader … Wikipedia
Extension conservative d'une théorie T — ● Extension conservative d une théorie T théorie T telle que chaque formule du langage L(T) de T qui est un théorème de T est aussi un théorème de T … Encyclopédie Universelle
conservative — in the meaning ‘moderate, cautious, low’, as in a conservative estimate, is one of Fowler s lost causes. He regarded it as a ridiculous ‘slipshod extension’ and rejected it outright. But it is now well established in the language and is… … Modern English usage
Conservative and Unionist Women's Franchise Association — The Conservative and Unionist Women s Franchise Association (CUWFA) was a British women s suffrage organisation open to members of the Conservative and Unionist Party.[1] Formed in 1908 by members of the National Union of Women s Suffrage… … Wikipedia
Extension conservatrice — En logique mathématique, une théorie logique T2 est une extension conservatrice (ou conservative) d une théorie T1 si le langage de T2 étend le langage de T1, si chaque théorème de T1 est un théorème de T2 et si tout théorème de T2 qui est dans… … Wikipédia en Français
Conservative governments — The Conservative Party traditionally shuns the notions of ideology and abstract thought, and has established a practice of responding to particular circumstances in a manner which will preserve those institutions beneficial to the existing… … Encyclopedia of contemporary British culture
conservative — ● conservatif, conservative adjectif (bas latin conservativus) Se dit d un système dont l énergie mécanique reste constante. Se dit de la circulation d un champ de vecteurs lorsqu elle ne dépend pas du chemin suivi. Se dit du flux d un champ de… … Encyclopédie Universelle
Progressive Conservative Party of Manitoba — Active provincial party Leader Hugh McFadyen President Michael Richards Founded 1882 ( … Wikipedia
Progressive Conservative Party of Ontario — Parti progressiste conservateur de l Ontario Active provincial party Leader Tim Hudak … Wikipedia