cálculo secuencial
En lógica matemática , el cálculo de secuencias es un estilo de argumentación lógica formal en el que cada línea de una prueba es una tautología condicional (llamada secuencia por Gerhard Gentzen ) en lugar de una tautología incondicional. Cada tautología condicional se infiere de otras tautologías condicionales en líneas anteriores en un argumento formal de acuerdo con las reglas y procedimientos de inferencia , dando una mejor aproximación al estilo natural de deducción utilizado por los matemáticos que al estilo anterior de lógica formal de David Hilbert., en el que cada línea era una tautología incondicional. Pueden existir distinciones más sutiles; por ejemplo, las proposiciones pueden depender implícitamente de axiomas no lógicos . En ese caso, los secuentes significan teoremas condicionales en un lenguaje de primer orden en lugar de tautologías condicionales.
El cálculo secuencial es uno de varios estilos existentes de cálculo de prueba para expresar argumentos lógicos línea por línea.
En otras palabras, los sistemas de deducción natural y cálculo secuencial son tipos particulares distintos de sistemas de estilo Gentzen. Los sistemas de estilo Hilbert suelen tener un número muy pequeño de reglas de inferencia y se basan más en conjuntos de axiomas. Los sistemas de estilo Gentzen suelen tener muy pocos axiomas, si es que tienen alguno, y se basan más en conjuntos de reglas.
Los sistemas de estilo Gentzen tienen importantes ventajas prácticas y teóricas en comparación con los sistemas de estilo Hilbert. Por ejemplo, tanto la deducción natural como los sistemas de cálculo secuencial facilitan la eliminación y la introducción de cuantificadores universales y existenciales para que las expresiones lógicas no cuantificadas puedan manipularse de acuerdo con las reglas mucho más simples del cálculo proposicional.. En un argumento típico, se eliminan los cuantificadores, luego se aplica cálculo proposicional a expresiones no cuantificadas (que normalmente contienen variables libres) y luego se vuelven a introducir los cuantificadores. Esto es muy similar a la forma en que los matemáticos llevan a cabo en la práctica las demostraciones matemáticas. Las pruebas de cálculo de predicados son generalmente mucho más fáciles de descubrir con este enfoque y, a menudo, son más cortas. Los sistemas de deducción natural son más adecuados para la demostración práctica de teoremas. Los sistemas de cálculo secuencial son más adecuados para el análisis teórico.
En la teoría de la demostración y la lógica matemática , el cálculo secuencial es una familia de sistemas formales que comparten un cierto estilo de inferencia y ciertas propiedades formales. Los primeros sistemas de cálculo secuencial, LK y LJ , fueron introducidos en 1934/1935 por Gerhard Gentzen [1] como una herramienta para estudiar la deducción natural en lógica de primer orden (en versiones clásica e intuicionista , respectivamente). El llamado "Teorema principal" de Gentzen ( Hauptsatz ) sobre LK y LJ fue el teorema de eliminación de corte , [2] [3]un resultado con consecuencias metateóricas de largo alcance , incluida la consistencia . Gentzen demostró aún más el poder y la flexibilidad de esta técnica unos años más tarde, aplicando un argumento de eliminación de corte para dar una prueba (transfinita) de la consistencia de la aritmética de Peano , en respuesta sorprendente a los teoremas de incompletitud de Gödel . Desde este trabajo inicial, los cálculos secuenciales, también llamados sistemas Gentzen , [4] [5] [6] [7] y los conceptos generales relacionados con ellos, se han aplicado ampliamente en los campos de la teoría de la prueba, la lógica matemática y la deducción automatizada . .
Una forma de clasificar los diferentes estilos de sistemas de deducción es mirar la forma de los juicios en el sistema, es decir , qué cosas pueden aparecer como la conclusión de una (sub) prueba. La forma de juicio más simple se usa en los sistemas de deducción de estilo Hilbert , donde un juicio tiene la forma
