Extension conservatrice
Un article de Wikipédia, l'encyclopédie libre.
 |
Cet article est une ébauche concernant les mathématiques.
Vous pouvez partager vos connaissances en l’améliorant. (Comment ?).
|
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.
