El proceso formal de ampliar un lenguaje de primer orden añadiendo nuevos símbolos de relación para conjuntos y relaciones que ya son definibles en el lenguaje original, junto con axiomas que afirman que cada símbolo nuevo es equivalente a la fórmula que lo define. La expansión hace explícita la definibilidad en la firma y actúa como una extensión definicional, conservativa cuando se realiza adecuadamente.

Principio

Introducir un símbolo nuevo para cada clase de equivalencia de fórmulas que definen la misma relación y añadir axiomas que identifiquen el símbolo con su fórmula definitoria; considerar la expansión como una extensión definicional conservativa que preserva la demostrabilidad en el lenguaje original.

Demostración

Dado un lenguaje L y una familia de fórmulas L {φ(x) : φ define una propiedad de tuplas}, formar L' = L ∪ {R_φ : un símbolo de relación por cada φ} y añadir los axiomas ∀x (R_φ(x) ↔ φ(x)). Para una teoría T en L compatible con estas identidades, T admite una extensión conservativa T' en L' donde cada R_φ nombra el conjunto definible por φ.

Aplicación incorrecta

Agregar predicados arbitrarios sin axiomas que los vinculen a fórmulas definibles, o asumir que añadir símbolos para clases no definibles conserva la conservación. Confundir morleyización con un enriquecimiento no conservador del lenguaje que cambia la verdad en los modelos.

Consecuencia

Facilita muchos argumentos modelísticos al convertir preguntas de definibilidad en cuestiones sintácticas sobre símbolos; permite el uso uniforme de los símbolos nuevos en construcciones (p. ej., esquemas EM, indiscernibles) mientras se controla la conservatividad.

Inversión

Olvidar los símbolos añadidos (tomar el reducto) vuelve al lenguaje original; propiedades expresadas únicamente mediante los símbolos nuevos pueden desaparecer en el reducto aunque la expansión fuera definicional a nivel de teoría.

Límite

Se aplica a conjuntos y relaciones definibles de primer orden (o a familias definibles explícitamente); no convierte en símbolos fenómenos genuinamente de segundo orden o no definibles. La conservatividad depende de elegir definiciones demostrables en la teoría de base.

Tensión semántica

Compite con la noción de extensión conservativa arbitraria: la morleyización es una extensión definicional particular que convierte fórmulas en símbolos atómicos, mientras que otras extensiones pueden ser conservativas por otras razones; la tensión aparece al decidir si tratar una relación como primitiva o como fórmula definida en las pruebas.

Síntesis

La morleyización consiste en reemplazar de forma controlada fórmulas definibles usadas con frecuencia por nuevos predicados más axiomas de equivalencia, haciendo explícita la definibilidad en la firma mientras se preserva el contenido de la teoría original y se facilitan manipulaciones sintácticas y combinatorias.