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 Ci Δ segue da una lista di asserzioni Di Γ (o equivalentemente che Γ comporta Δ) e si scrive quando 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.