Sequente

Un sequente è un'entità della logica che permette di esprimere legami tra asserzioni complesse facendo uso dei legami metalinguistici e che comporta. Le prime formalizzazioni di sequenti e di calcolo dei sequenti sono dovute al lavoro del logico Gerhard Gentzen, in particolare alle sue scoperte dei primi anni Trenta.

Si dice che lista di asserzioni C_i Δ segue da una lista di asserzioni D_i Γ (o equivalentemente che Γ comporta Δ) e si scrive

${\displaystyle \Gamma \vdash \Delta }$

quando

${\displaystyle (C_{1}ass.\ e\ C_{2}ass.\ e\ \dots \ e\ C_{n}ass.)\ comporta\ (D_{1}ass.\ o\ \dots \ o\ D_{m}ass.)}$

Nella visione della logica classica (LK) Δ è una lista di m asserzioni (o proposizioni), mentre in logica intuizionista (LJ) in Δ trova posto una sola proposizione. Questo è un fatto di notevole importanza perché condiziona tutta la struttura di regole inferenziali sui due sistemi.