Secuente

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.