Une relation entre théories formelles qui tient lorsque chacune peut s'obtenir de l'autre par l'ajout de définitions explicites de nouveaux symboles de sorte que les deux théories soient intertraduisibles sans modifier le contenu des phrases dans les vocabulaires d'origine.

Principe

Deux théories sont équivalentes définitionnellement lorsqu'il existe des définitions explicites, préservant la vérité, qui traduisent chaque symbole non logique de l'une dans le langage de l'autre et font des axiomes de l'une des conséquences des axiomes de l'autre sous ces définitions.

Démonstration

Considérons une théorie du premier ordre T qui utilise un symbole binaire R et une présentation alternative T' qui remplace R par un symbole S accompagné d'un axiome définissant S(x,y) ↔ φ_R(x,y), où φ_R est une formule dans le langage de T. Si réciproquement R est définissable dans T' par une formule φ_S, alors T et T' sont équivalentes définitionnellement : leurs théorèmes portant sur le vocabulaire commun coïncident après dépliage des définitions.

Mauvaise application

Confondre interprétabilité réciproque ou partage de modèles avec équivalence définitionnelle. L'interprétabilité réciproque peut être plus faible et ne pas fournir de définitions explicites permettant d'éliminer les symboles ajoutés ; en conclure l'équivalence est une erreur fréquente.

Conséquence

Lorsque des théories sont équivalentes définitionnellement, on peut librement remplacer une présentation par l'autre dans des preuves, des constructions de modèles et des applications qui n'impliquent que le vocabulaire partagé ; les deux présentations sont des variantes notationales de la même théorie.

Inversion

Inversement, deux théories peuvent prouver les mêmes phrases dans un langage donné (équivalence conservatrice) sans qu'il existe de définitions explicites pour éliminer les nouveaux symboles ; ces théories ne sont pas équivalentes définitionnellement malgré leur accord sur ces phrases.

Limite

S'applique aux théories formelles où l'on admet des règles d'extension définitoire (introduction de symboles abrégés par des formules définitoires exactes). Elle exclut des relations plus faibles comme l'interprétabilité réciproque, certaines formes d'équivalence de Morita ou l'équivalence sémantique sans clauses définitoires explicites ; elle présuppose aussi une notion acceptée de définitions admissibles dans la logique de fond.

Tension sémantique

Concurrence avec des notions telles que la bi-interprétabilité et l'équivalence catégorique : la bi-interprétabilité permet des traductions mutuelles à un isomorphisme près, tandis que l'équivalence définitionnelle exige des définitions éliminatoires explicites. La tension porte sur le critère pertinent pour dire que deux théories sont 'les mêmes'.

Synthèse

L'équivalence définitionnelle est la notion syntaxique selon laquelle deux théories sont identiques à un changement de notation près : des définitions explicites transforment un vocabulaire en l'autre, rendant chaque théorie une variante notationale de l'autre.