In mathematical logic, a logical theory <math>T_2</math> is a conservative extension of a theory <math>T_1</math> if the language of <math>T_2</math> extends the language of <math>T_1</math>; every theorem of <math>T_1</math>is a theorem of <math>T_2</math>; and any theorem of <math>T_2</math> which is in the language of <math>T_1</math> is already a theorem of <math>T_1</math>.

PropertyValue
dbpprop:abstract
  • In mathematical logic, a logical theory <math>T_2</math> is a conservative extension of a theory <math>T_1</math> if the language of <math>T_2</math> extends the language of <math>T_1</math>; every theorem of <math>T_1</math>is a theorem of <math>T_2</math>; and any theorem of <math>T_2</math> which is in the language of <math>T_1</math> is already a theorem of <math>T_1</math>. More generally, if Γ is a set of formulas in the common language of <math>T_1</math> and <math>T_2</math>, then <math>T_2</math> is Γ-conservative over <math>T_1</math>, if every formula from Γ provable in <math>T_2</math> is also provable in <math>T_1</math>. 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, <math>T_0</math>, that is known (or assumed) to be consistent, and successively build conservative extensions <math>T_1</math>, <math>T_2</math>, ... 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.
  • En logique mathématique, une théorie logique T2 est une extension conservatrice 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 le langage de T1 est déjà un théorème de T1. Informellement, la nouvelle théorie peut éventuellement être plus commode pour prouver des théorèmes, mais elle ne prouve pas de théorème nouveau concernant l'ancienne théorie. L'importance de cette notion réside dans le théorème suivant: si T2 est une extension conservatrice de T1, et si T1 est cohérente, alors T2 est également cohérente Ainsi, les extensions conservatrices n'encourent pas le risque d'introduire de nouvelles incohérences. Elles peuvent également être vues comme une méthodologie pour écrire et structurer des théories volumineuses: commencer avec une théorie T0 connue comme cohérente, et successivement construire des extensions conservatrices T1, T2, etc. Le démonstrateur automatique Isabelle adopte cette méthodologie en fournissant un langage pour les extensions conservatrices par définition.
  • 保守扩展是逻辑中的一个概念。一个知识库K'是K的扩展，如果K是K'的一个子集；K'是是K的保守扩展，如果对所有只用K中的名字构造的命题<math>\alpha</math>, K'<math>\vDash \alpha</math> 当且仅当 K<math>\vDash \alpha</math>。换句话说，保守扩展不会改变原有的知识库的结构。保守扩展在许多领域都有应用，如模块化本体和敏感知识的保护。 在逻辑和推导机制中，I和J分别是一个解释(Interpretation),如果J是I的保守扩展，必须满足以下条件: 1) 解释I作用在语言集合L中，解释J必须作用在语言集合L'中,并且L'包含L 2) 解释I的域(Domain)等于解释J的域 3) 对于任何在语言集合L中的元素e，I(e) = J(e) 那么我们说J是I的保守扩展。
dbpprop:hasPhotoCollection
dbpprop:reference
rdfs:comment
  • In mathematical logic, a logical theory <math>T_2</math> is a conservative extension of a theory <math>T_1</math> if the language of <math>T_2</math> extends the language of <math>T_1</math>; every theorem of <math>T_1</math>is a theorem of <math>T_2</math>; and any theorem of <math>T_2</math> which is in the language of <math>T_1</math> is already a theorem of <math>T_1</math>.
  • En logique mathématique, une théorie logique T2 est une extension conservatrice 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 le langage de T1 est déjà un théorème de T1. Informellement, la nouvelle théorie peut éventuellement être plus commode pour prouver des théorèmes, mais elle ne prouve pas de théorème nouveau concernant l'ancienne théorie.
rdfs:label
  • Conservative extension
  • Extension conservatrice
  • 保守扩展
owl:sameAs
skos:subject
foaf:page
is dbpprop:redirect of