El teorema de Herbrand es un resultado fundamental de la lógica matemática obtenido por Jacques Herbrand (1930). [1] En esencia, permite que un cierto tipo de reducción de la lógica de primer orden a la lógica de proposiciones . Aunque Herbrand demostró originalmente 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.
Declaración
Dejar
ser una fórmula de lógica de primer orden con libre de cuantificadores, 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
- y ,
tal que
es válido. Si es válido, se llama una disyunción de Herbrand para
Informalmente: una fórmula en forma prenex que contiene solo cuantificadores existenciales es demostrable (válido) en lógica de primer orden si y solo si una disyunción compuesta de instancias de sustitución de la subfórmula libre de cuantificador dees 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 la forma prenex y sus cuantificadores universales pueden eliminarse mediante Herbrandization . Se puede evitar la conversión a la forma prenex, si se realiza una herbrandización estructural . La herbrandización se puede evitar imponiendo restricciones adicionales a las dependencias variables permitidas en la disyunción de Herbrand.
Boceto de prueba
Se puede construir una demostración de la dirección no trivial del teorema de acuerdo con los siguientes pasos:
- Si la frmula es válida, entonces por lo completo de libre de corte cálculo secuencial , que se sigue de Gentzen 's -eliminación corte teorema, hay una prueba libre de corte de.
- Comenzando de arriba hacia abajo, elimine las inferencias que introducen cuantificadores existenciales.
- Elimine las contracciones-inferencias en fórmulas previamente cuantificadas existencialmente, ya que las fórmulas (ahora con términos sustituidos por variables previamente cuantificadas) podrían dejar de ser idénticas después de la eliminación de las inferencias cuantificadoras.
- La eliminación de las contracciones acumula todas las instancias de sustitución relevantes de en el lado derecho del secuente, resultando así en una prueba de , a partir de la cual se puede obtener la disyunción de Herbrand.
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.
Generalizaciones del teorema de Herbrand
- El teorema de Herbrand se ha extendido a la lógica de orden superior mediante el uso de pruebas de árbol de expansión . [3] La representación profunda de las demostraciones del árbol de expansión corresponde a una disyunción de Herbrand, cuando se restringe a la lógica de primer orden.
- Las disyunciones de marcas y las pruebas de árboles de expansión se han ampliado con una noción de corte. Debido a la complejidad de la eliminación de cortes, las disyunciones de Herbrand con cortes pueden ser no elementalmente más pequeñas que una disyunción de Herbrand estándar.
- Las disyunciones de Herbrand se han generalizado a las secuencias de Herbrand, lo que permite establecer el teorema de Herbrand para las secuencias: "una secuencia de Skolemized es derivable si tiene una secuencia de Herbrand".
Ver también
Notas
- ^ J. Herbrand: Recherches sur la théorie de la démonstration. Travaux de la société des Sciences et des Lettres de Varsovie , Clase III, Sciences Mathématiques et Physiques, 33, 1930.
- ^ Samuel R. Buss: "Manual de teoría de la prueba". Capítulo 1, "Introducción a la teoría de la prueba". Elsevier, 1998.
- ^ Dale Miller: una representación compacta de pruebas. Studia Logica , 46 (4), págs. 347-370, 1987.
Referencias
- Buss, Samuel R. (1995), "Sobre el teorema de Herbrand" , en Maurice, Daniel; Leivant, Raphaël (eds.), Logic and Computational Complexity , Lecture Notes in Computer Science, Berlín, Nueva York: Springer-Verlag , págs. 195–209 , ISBN 978-3-540-60178-4.