Un objeto sintáctico de la forma Γ ⇒ Δ (donde Γ y Δ son, típicamente, multiconjuntos o secuencias finitas de fórmulas) que expresa que la conjunción de fórmulas en Γ implica la disyunción de fórmulas en Δ dentro de un sistema de demostración por secuentes.

Principio

Un secuente internaliza la consecuencia lógica como un único token similar a una fórmula, de modo que las reglas de inferencia operan localmente sobre las partes antecedente y sucedente, permitiendo la manipulación sistemática de la estructura de la consecuencia.

Demostración

Ejemplo de secuente: {A, A→B} ⇒ {B}. Interpretado en un cálculo de secuentes clásico, las reglas permiten transformar las premisas en el sucedente; este único secuente representa la afirmación de que A y A→B implican B.

Aplicación incorrecta

Leer un secuente Γ ⇒ Δ simplemente como la implicación material (∧Γ)→(∨Δ) sin respetar las reglas estructurales o el contexto, o tratar los secuentes como condicionales semánticos en contextos donde el cálculo restringe reglas estructurales (por ejemplo, secuentes intuicionistas de conclusión única).

Consecuencia

El uso de secuentes hace explícitos fenómenos estructurales (debilitación, contracción, permutación, corte); la representación por secuentes soporta resultados meta como la eliminación del corte y estrategias sistemáticas de búsqueda de pruebas.

Inversión

La inversión es intercambiar antecedente y sucedente (Δ ⇒ Γ) o convertir juicios de secuente en teoremas a nivel de fórmula en un sistema estilo Hilbert; tales inversiones ponen de manifiesto asimetrías (p. ej., secuentes intuicionistas de conclusión única).

Límite

Se aplica dentro de los cálculos de secuentes y marcos sintácticos afines; es un dispositivo formal y no en sí mismo una valoración semántica o un modelo; los secuentes presuponen una decisión sobre si Γ/Δ son conjuntos, multiconjuntos o secuencias y sobre las reglas estructurales permitidas.

Tensión semántica

Existe tensión entre el secuente como token sintáctico de consecuencia y otras representaciones de consecuencia (Hilbert, deducción natural, tableaux): todas expresan consecuencia pero distribuyen el trabajo lógico de forma diferente entre reglas y contextos.

Síntesis

Un secuente es una representación sintáctica concentrada de consecuencia, Γ ⇒ Δ, diseñada para que reglas de inferencia locales manipulen componentes antecedente y sucedente, lo que permite análisis estructural y transformaciones algorítmicas de pruebas.