Une extension T' d'une théorie T est conservative si T' ne prouve aucune nouvelle phrase dans le langage de T au-delà de celles déjà démontrables dans T ; équivalemment, toute phrase du langage initial prouvable dans l'extension était déjà prouvable dans la théorie de base.

Principe

La conservativité exige que les axiomes ou symboles ajoutés servent seulement à abréger ou organiser le contenu sans produire de conséquences nouvelles exprimables dans le vocabulaire initial ; l'extension ne peut trancher des questions formulées dans le langage d'origine que T laissait ouvertes.

Démonstration

Si T est une théorie du premier ordre et T' s'obtient en ajoutant un symbole fonctionnel neuf f avec un axiome qui définit f(x) comme un terme t(x) déjà exprimable dans T, alors T' est une extension conservative de T parce que toute phrase du langage de T prouvable dans T' peut être réécrite en une preuve dans T en éliminant f via sa définition.

Mauvaise application

Supposer que tout élargissement syntaxique qui préserve la consistance est conservative. Une extension peut être consistante mais non conservative : elle peut prouver de nouveaux théorèmes dans le langage ancien (par exemple en ajoutant un schéma d'axiomes impliquant une assertion arithmétique auparavant indépendante), donc la consistance seule n'implique pas la conservativité.

Conséquence

Une extension conservative est sûre en pratique théorique : on peut introduire définitions, abréviations ou outils commodes sans modifier les engagements de la théorie concernant le sujet initial ; les résultats portant sur le vocabulaire d'origine restent inchangés.

Inversion

Une extension non conservative ajoute de nouveaux théorèmes dans le langage initial ; une telle extension modifie le contenu de la théorie sur les sujets d'origine et peut servir à trancher des phrases auparavant indépendantes.

Limite

La conservativité est une affirmation au sujet des phrases dans le langage de base ; elle ne dit rien sur les nouveaux théorèmes incluant les symboles ajoutés. Elle présuppose un langage de base fixé et ne s'applique pas automatiquement lorsque la signature d'extension modifie ce qui compte comme « phrase initiale ».

Tension sémantique

La tension apparaît entre extension conservative et extension définitionnelle : toutes les extensions définitionnelles sont conservatives, mais toute extension conservative n'est pas nécessairement définitionnelle. Il y a aussi tension avec l'interprétabilité : une extension interprétable peut être ou non conservative selon l'effet de l'interprétation sur les phrases du langage d'origine.

Synthèse

Une extension conservative enrichit une théorie par de nouveaux moyens tout en garantissant qu'aucune affirmation supplémentaire sur le vocabulaire initial ne devient démontrable ; elle formalise l'idée d'un enrichissement notational ou méthodologique sûr qui ne modifie pas les conséquences de base.