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

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

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

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

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

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

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

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

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.