La propiedad según la cual siempre que un símbolo no lógico (relación, función o constante) es definible implícitamente por una teoría —es decir, cualesquiera dos modelos de la teoría que concuerdan en el lenguaje base también concuerdan en la interpretación de ese símbolo— entonces existe una definición explícita de ese símbolo mediante una fórmula en el lenguaje original (una fórmula definitoria explícita).

Principio

La idea organizadora es que la unicidad semántica (definibilidad implícita) debe poder convertirse en una especificación sintáctica (una fórmula explícita): si la teoría fuerza una interpretación única de un símbolo respecto del vocabulario base, esa interpretación puede capturarse por una fórmula en el lenguaje base.

Demostración

Ejemplo: el teorema de Beth muestra que la lógica de primer orden clásica satisface esta propiedad: si un símbolo predicado está implícitamente definido por una teoría de primer orden, entonces existe una fórmula de primer orden (en el lenguaje reducido) que lo define explícitamente.

Aplicación incorrecta

Suponer la propiedad de Beth automáticamente en lógicas donde falla (algunas lógicas modales, intuicionistas o extensiones del primer orden no la tienen) o confundir la definibilidad implícita (unicidad semántica) con una mera extensión conservativa o la eliminabilidad sin producir una fórmula explícita.

Consecuencia

Cuando la propiedad de Beth se cumple se pueden sustituir definiciones implícitas por definiciones explícitas, lo que simplifica axiomatizaciones, permite eliminar símbolos auxiliares y conecta con fenómenos de interpolación e interpolación uniforme en la lógica.

Inversión

La falla de la propiedad de Beth da lugar a fenómenos en los que un concepto está determinado de forma única por una teoría pero ninguna fórmula en el lenguaje base lo denota; tales fracasos señalan una brecha entre determinación semántica y expresabilidad sintáctica.

Límite

Se refiere a la definibilidad de símbolos no lógicos respecto a un lenguaje base; no afirma por sí misma la constructibilidad algorítmica de la definición explícita ni se aplica a nociones metateóricas fuera del lenguaje de la teoría.

Tensión semántica

Hay tensión entre la implicitud semántica y la explicitación sintáctica y entre la propiedad de Beth y las extensiones expresivas: recursos expresivos más fuertes pueden facilitar la definibilidad explícita, mientras que lógicas más débiles o constructivas pueden separar lo implícito de lo explícito.

Síntesis

La propiedad de definibilidad de Beth enlaza la unicidad semántica con la definibilidad sintáctica: cuando se cumple, cualquier concepto forzado de forma única por una teoría puede ser dado mediante una fórmula explícita en el lenguaje original, cerrando la brecha entre determinación modelo-teórica y especificación prueba-teórica.