| Property |
Value |
| dbo:abstract
|
- 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 le langage de T1 est déjà un théorème de T1. Une extension propre est une extension non conservative. Informellement, cela veut dire que la nouvelle théorie peut éventuellement être plus commode pour prouver des théorèmes, mais qu’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 ne courent pas le risque d'introduire de nouvelles incohérences. Elles peuvent aussi être vues comme une méthode pour écrire et structurer des théories volumineuses : on commence avec une théorie T0 connue comme cohérente, puis on construit successivement 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. (fr)
- 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 le langage de T1 est déjà un théorème de T1. Une extension propre est une extension non conservative. Informellement, cela veut dire que la nouvelle théorie peut éventuellement être plus commode pour prouver des théorèmes, mais qu’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 ne courent pas le risque d'introduire de nouvelles incohérences. Elles peuvent aussi être vues comme une méthode pour écrire et structurer des théories volumineuses : on commence avec une théorie T0 connue comme cohérente, puis on construit successivement 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. (fr)
|
| dbo:wikiPageID
| |
| dbo:wikiPageLength
|
- 1544 (xsd:nonNegativeInteger)
|
| dbo:wikiPageRevisionID
| |
| dbo:wikiPageWikiLink
| |
| prop-fr:wikiPageUsesTemplate
| |
| dct:subject
| |
| rdf:type
| |
| rdfs:comment
|
- 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 le langage de T1 est déjà un théorème de T1. Une extension propre est une extension non conservative. si T2 est une extension conservatrice de T1, et si T1 est cohérente, alors T2 est également cohérente. Le démonstrateur automatique Isabelle adopte cette méthodologie en fournissant un langage pour les extensions conservatrices par définition. (fr)
- 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 le langage de T1 est déjà un théorème de T1. Une extension propre est une extension non conservative. si T2 est une extension conservatrice de T1, et si T1 est cohérente, alors T2 est également cohérente. Le démonstrateur automatique Isabelle adopte cette méthodologie en fournissant un langage pour les extensions conservatrices par définition. (fr)
|
| rdfs:label
|
- Conservative extension (en)
- Extension conservatrice (fr)
- 保守扩展 (zh)
|
| rdfs:seeAlso
| |
| owl:sameAs
| |
| prov:wasDerivedFrom
| |
| foaf:isPrimaryTopicOf
| |
| is dbo:wikiPageRedirects
of | |
| is dbo:wikiPageWikiLink
of | |
| is oa:hasTarget
of | |
| is foaf:primaryTopic
of | |
