Extension conservatrice

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher
Ce modèle est-il pertinent ? Cliquez pour en voir d'autres.
Cet article est orphelin. Moins de trois articles lui sont liés (décembre 2015).

Aidez à ajouter des liens en plaçant le code [[Extension conservatrice]] dans les articles relatifs au sujet.

image illustrant les mathématiques
Cet article est une ébauche concernant les mathématiques.

Vous pouvez partager vos connaissances en l’améliorant (comment ?) selon les recommandations des projets correspondants.

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 également ê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.

Sources[modifier | modifier le code]

(en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « Conservative extension » (voir la liste des auteurs).