Conservative extension

Conservative extension

In mathematical logic, a logical theory T2 is a (proof theoretic) conservative extension of a theory T1 if the language of T2 extends the language of T1; every theorem of T1 is a theorem of T2; and any theorem of T2 which is in the language of T1 is already a theorem of T1.

More generally, if Γ is a set of formulas in the common language of T1 and T2, then T2 is Γ-conservative over T1, if every formula from Γ provable in T2 is also provable in T1.

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, T0, that is known (or assumed) to be consistent, and successively build conservative extensions T1, T2, ... 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.


Model-theoretic conservative extension

With model-theoretic means, a stronger notion is obtained: T2 is a model-theoretic conservative extension of T1 if every model of T1 can be expanded to a model of T2. 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.

External links

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

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”

We are using cookies for the best presentation of our site. Continuing to use this site, you agree with this.