## [Cálculo de Secuentes](/es/node/59902) Definición Un marco deductivo formal en el que los secuentes son las unidades sintácticas primarias y las pruebas se construyen aplicando reglas de inferencia estructurales y lógicas a los secuentes, frecuentemente incluyendo una regla de corte y a veces reglas estructurales como debilitamiento, contracción y permutación. ## Principio Principio El cálculo de secuentes organiza la deducción alrededor de manipulaciones locales de las partes antecedente y sucedente; esa localidad respalda transformaciones modulares de pruebas (por ejemplo, eliminación del corte) y búsqueda sistemática de pruebas. ## Demostración Demostración En el cálculo de secuentes clásico LK se puede derivar A∨B ⇒ A∨B a partir de axiomas de identidad y luego usar reglas de introducción izquierda/derecha para construir pruebas más extensas; una demostración estándar es aplicar eliminación del corte para transformar una prueba que usa corte en otra que no lo usa. ## Aplicación incorrecta Aplicación incorrecta Tratar las reglas del cálculo de secuentes como reglas semánticas de reescritura en lugar de pasos de inferencia sintácticos, o aplicar reglas estructurales irrestrictas en contextos (como la lógica lineal) donde están prohibidas, lo que conduce a derivaciones incorrectas o no pertinentes. ## Consecuencia Consecuencia El cálculo de secuentes sustenta resultados meta-teóricos (eliminación del corte, consistencia, propiedad de subfórmula en ciertas formulaciones) y herramientas prácticas (búsqueda sistemática hacia atrás, base para demostradores automáticos y transformaciones de pruebas). ## Inversión Inversión La inversión es adoptar marcos alternativos (deducción natural, sistemas de Hilbert) donde las reglas de inferencia actúan sobre fórmulas en lugar de secuentes; la comparación pone de relieve compensaciones entre simetría, localidad y tamaño de la prueba. ## Límite Límite Se aplica a la teoría sintáctica de pruebas y a sistemas formales que representan consecuencia lógica mediante secuentes; no proporciona en sí modelos semánticos y debe instanciarse con una firma lógica y un conjunto de reglas — distintas elecciones producen variantes clásicas, intuicionistas, lineales u otras. ## Tensión semántica Tensión semántica Existe tensión entre el cálculo de secuentes y la deducción natural: el cálculo enfatiza la simetría y la manipulación estructural de contextos, mientras la deducción natural enfatiza la introducción/eliminación de conectivos y a menudo produce pruebas más compactas para el razonamiento humano. ## Síntesis Síntesis El cálculo de secuentes es una arquitectura deductiva centrada en secuentes y gobernada por reglas, que hace explícitas las operaciones estructurales, posibilita teoremas rigurosos de transformación de pruebas y facilita la búsqueda mecanizada de pruebas, estando parametrizado por la elección de reglas.