Una relación entre teorías formales que se da cuando cada teoría puede obtenerse de la otra añadiendo definiciones explícitas para símbolos nuevos, de modo que ambas son intertraducibles sin cambiar el contenido de las oraciones en los vocabularios originales.

Principio

Dos teorías son equivalentemente definicionales cuando existen definiciones explícitas, que preservan la verdad, que traducen cada símbolo no lógico de una al lenguaje de la otra y convierten sus axiomas en consecuencias mutuas bajo esas definiciones.

Demostración

Considere una teoría de primer orden T que usa un símbolo binario R y una presentación alternativa T' que reemplaza R por un símbolo S junto con un axioma definitorio S(x,y) ↔ φ_R(x,y), donde φ_R es una fórmula en el lenguaje de T. Si recíprocamente R puede definirse en T' por una fórmula φ_S, entonces T y T' son equivalentes definicionales; sus teoremas sobre el vocabulario compartido coinciden tras desplegar las definiciones.

Aplicación incorrecta

Confundir la interpretabilidad mutua o compartir modelos con equivalencia definicional. La interpretabilidad mutua puede ser más débil y no proporcionar definiciones explícitas para eliminar símbolos añadidos; concluir equivalencia a partir de interpretabilidad es un error común.

Consecuencia

Cuando las teorías son equivalentes definicionales, puede sustituirse libremente una presentación por la otra en pruebas, construcciones de modelos y aplicaciones que solo utilicen el vocabulario compartido; las dos presentaciones son variantes notacionales de la misma teoría.

Inversión

La situación inversa son dos teorías que prueban las mismas oraciones en un lenguaje dado (equivalencia conservadora) pero sin definiciones explícitas para eliminar los símbolos nuevos; tales teorías no son equivalentes definicionales pese a coincidir en esas oraciones.

Límite

Se aplica a teorías formales en las que se permiten reglas de extensión definitoria (introducción de símbolos abreviadores con fórmulas definitorias exactas). Excluye relaciones más débiles como la interpretabilidad mutua, algunas formas de equivalencia de Morita o la equivalencia semántica sin cláusulas definitorias explícitas; supone además una noción aceptada de definiciones admisibles en la lógica de base.

Tensión semántica

Compite con nociones como la bi-interpretabilidad y la equivalencia categórica: la bi-interpretabilidad admite traducciones mutuas hasta isomorfismo, mientras que la equivalencia definicional exige definiciones eliminatorias explícitas. La tensión reside en si debe priorizarse la eliminabilidad sintáctica o la traducibilidad semántica.

Síntesis

La equivalencia definicional es la noción sintáctica de que dos teorías son la misma, salvo por la introducción y eliminación de símbolos definidos: definiciones explícitas convierten un vocabulario en el otro, haciendo de cada teoría una variante notacional de la otra.