Sesión Lógica y ComputabilidadEl teorema de Herbrand: Un enunciado autocontenido y una prueba modeloteórica
Mariana Badano
UNC Famaf, Argentina - Esta dirección de correo electrónico está siendo protegida contra los robots de spam. Necesita tener JavaScript habilitado para poder verlo.
El Teorema de Herbrand fue enunciado por primera vez por Herbrand en su tesis de 1930 [1] y constituye un resultado fundamental en lógica matemática que sirve como base teórica para muchos procedimientos de prueba.
El teorema al que comúnmente se hace referencia como “el Teorema de Herbrand” en los cursos modernos de lógica suele ser una versión más débil, restringida a fórmulas que, en forma prenexa, contienen únicamente cuantificadores existenciales. En cambio, la versión completa del Teorema de Herbrand se aplica a todas las fórmulas de primer orden. La versión más simple, restringida a fórmulas existenciales, tiene una demostración modeloteórica bien conocida, mientras que la demostración del teorema general es una demostración sintáctica compleja. Además, no existe una formulación simple del Teorema de Herbrand.
En este trabajo se presenta una formulación autónoma del teorema, junto con una demostración modeloteórica de su versión general. Se espera que esta nueva formulación simplifique la aplicabilidad del Teorema de Herbrand, en particular en la teoría de modelos y el álgebra universal. Como ejemplo de ello, se ofrece un corolario que aplica el teorema a variedades y fórmulas positivas.
Referencias
[1] Jacques Herbrand. Recherches sur la théorie de la démonstration. PhD thesis, Institut de Mathématique de l’Université de Paris, Paris, 1930.