Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur Graph Search.
Concept
Extension conservatrice
Résumé
In mathematical logic, a conservative extension is a supertheory of a theory which is often convenient for proving theorems, 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 is a (proof theoretic) conservative extension of a theory if every theorem of is a theorem of , and any theorem of 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 .
Note that a conservative extension of a consistent theory is consistent. If it were not, then by the principle of explosion, every formula in the language of would be a theorem of , so every formula in the language of would be a theorem of , so would not be 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.
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.
a subsystem of second-order arithmetic studied in reverse mathematics, is a conservative extension of first-order Peano arithmetic.
The subsystems of second-order arithmetic and are -conservative over .
The subsystem is a -conservative extension of , and a -conservative over (primitive recursive arithmetic).
Von Neumann–Bernays–Gödel set theory () is a conservative extension of Zermelo–Fraenkel set theory with the axiom of choice ().
Internal set theory is a conservative extension of Zermelo–Fraenkel set theory with the axiom of choice ().
Source officielle
À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.