Una relación entre teorías en la que una teoría nueva se obtiene de una teoría base añadiendo símbolos nuevos junto con axiomas definitorios explícitos que caracterizan esos símbolos en términos del lenguaje base, de modo que no se introducen nuevos teoremas en el lenguaje original (conservatividad).

Principio

Cada símbolo añadido debe acompañarse de una fórmula definitoria en el lenguaje original que determine su significado (a menudo mediante condiciones de existencia y unicidad), y la extensión debe ser eliminable en el sentido de que cualquier teorema sobre el vocabulario original demostrable en la extensión ya era demostrable en la teoría base.

Demostración

Introducir un símbolo de función f y añadir el axioma ∀x ∃!y φ(x,y) y el axioma definitorio ∀x∀y (f(x)=y ↔ φ(x,y)). Siempre que la teoría base demuestre las afirmaciones de existencia y unicidad o se trate f como una abreviatura definicional conservativa, la extensión no produce resultados nuevos en el lenguaje antiguo.

Aplicación incorrecta

Tratar adiciones arbitrarias de axiomas como definicionales (por ejemplo, añadir axiomas de existencia sin equivalencia definicional) o no verificar la eliminabilidad; tales movimientos pueden aumentar encubiertamente la fuerza, probar nuevas oraciones en el lenguaje original o introducir compromisos no deseados.

Consecuencia

Las extensiones definicionales permiten el desarrollo modular de teorías y comodidad notacional sin cambiar el contenido sustantivo respecto a los símbolos originales; preservan la consistencia y permiten eliminar definiciones para recuperar las pruebas originales.

Inversión

Una extensión no definicional (axiomática) añade contenido teórico genuino y puede probar en el lenguaje original enunciados que antes eran indemostrables; pasar de definicional a axiomática incrementa la fuerza expresiva y prueba‑teórica.

Límite

Se aplica a teorías formales donde pueden enunciarse definiciones explícitas; no cubre extensiones conservativas logradas por medios indirectos no eliminables, ni extensiones que añadan afirmaciones de existencia sin equivalencia definicional o que dependan de recursos de orden superior.

Tensión semántica

Existe tensión con nociones como extensión conservativa, eliminabilidad y definibilidad implícita: una extensión definicional es un tipo especial de extensión conservativa con definiciones explícitas eliminables, pero las definiciones implícitas o abreviaturas no eliminables difuminan la distinción.

Síntesis

Una extensión definicional añade símbolos con definiciones explícitas eliminables de modo que la teoría extendida es conservativa sobre la base para el lenguaje original; formaliza notación segura y modularidad sin alterar las consecuencias de la teoría original.