Evert Willem Beth

El teorema de definibilidad de Beth es un resultado fundamental en lógica que establece que una propiedad definida implícitamente por una teoría de primer orden tiene una definición explícita dentro de esa teoría. Esto significa que si un nuevo símbolo o propiedad se determina de forma única en todos los modelos de una teoría, debe existir una fórmula que, utilizando únicamente los símbolos existentes de la teoría, lo defina. El teorema establece una equivalencia entre la definibilidad implícita y explícita en la lógica clásica de primer orden, vinculando su sintaxis (pruebas) y su semántica (modelos). ^{[ 2 ]}

La contribución más famosa de Beth a la lógica formal son los tableaux semánticos , que son procedimientos de decisión para la lógica proposicional y la lógica de primer orden . Es un método semántico —como las tablas de verdad de Wittgenstein o la resolución de J. Alan Robinson— en contraposición a la demostración de teoremas en un sistema formal, como los sistemas axiomáticos empleados por Frege , Russell y Whitehead , e Hilbert , o incluso la deducción natural de Gentzen . Los tableaux semánticos son un procedimiento de decisión eficaz para la lógica proposicional, mientras que son solo semi-eficaces para la lógica de primer orden, ya que esta última es indecidible , como lo demuestra el teorema de Church . Muchos consideran que este método es intuitivamente simple, especialmente para estudiantes que no están familiarizados con el estudio de la lógica, y es más rápido que el método de las tablas de verdad (que requiere una tabla con 2ⁿ ^filas para una oración con n letras proposicionales). Por estas razones, Wilfrid Hodges, por ejemplo, presenta diagramas semánticos en su libro de texto introductorio, Lógica , y Melvin Fitting hace lo mismo en su presentación de lógica de primer orden para científicos informáticos , Lógica de primer orden y demostración automatizada de teoremas .

Uno comienza con la intención de demostrar que un determinado conjunto${\displaystyle \Gamma \,}$de fórmulas implican otra fórmula${\displaystyle \varphi \,}$, dado un conjunto de reglas determinadas por la semántica de los conectores de las fórmulas (y cuantificadores, en lógica de primer orden ). El método consiste en asumir la verdad concurrente de cada miembro de${\displaystyle \Gamma \,}$y de${\displaystyle \neg \varphi }$(la negación de${\displaystyle \varphi \,}$), y luego aplicar las reglas para ramificar esta lista en una estructura arbórea de fórmulas (más simples) hasta que cada rama posible contenga una contradicción . En este punto se habrá establecido que${\displaystyle \Gamma \cup \{\neg \varphi \}}$es inconsistente y, por lo tanto, que las fórmulas de${\displaystyle \Gamma \,}$juntos implican${\displaystyle \varphi \,}$.

Se trata de una clase de modelos relacionales para la lógica no clásica (véase la semántica de Kripke ).