el teorema de Herbrand
El teorema de Herbrand es un resultado fundamental de la lógica matemática obtenido por Jacques Herbrand (1930). [1] Esencialmente, permite cierto tipo de reducción de la lógica de primer orden a la lógica proposicional . Aunque Herbrand originalmente demostró su teorema para fórmulas arbitrarias de lógica de primer orden, [2] la versión más simple que se muestra aquí, restringida a fórmulas en forma prenex que contienen solo cuantificadores existenciales , se hizo más popular.
ser una fórmula de lógica de primer orden sin cuantificador, aunque puede contener variables libres adicionales. Esta versión del teorema de Herbrand establece que la fórmula anterior es válida si y solo si existe una secuencia finita de términos , posiblemente en una expansión del lenguaje, con
De manera informal: una fórmula en forma prenex que contiene solo cuantificadores existenciales es demostrable (válida) en lógica de primer orden si y solo si una disyunción compuesta de instancias de sustitución de la subfórmula sin cuantificador es una tautología (derivable proposicionalmente).
La restricción a fórmulas en forma prenex que contienen solo cuantificadores existenciales no limita la generalidad del teorema, porque las fórmulas se pueden convertir a forma prenex y sus cuantificadores universales se pueden eliminar mediante herbrandización . La conversión a la forma prenex puede evitarse si se realiza Herbrandización estructural . Herbrandization puede evitarse imponiendo restricciones adicionales sobre las dependencias variables permitidas en la disyunción de Herbrand.
Una prueba de la dirección no trivial del teorema se puede construir de acuerdo con los siguientes pasos:
Sin embargo, el cálculo secuencial y la eliminación de cortes no se conocían en el momento del teorema de Herbrand, y Herbrand tuvo que demostrar su teorema de una manera más complicada.