[source: wikipedia](https://en.wikipedia.org/wiki/Sequent_calculus) Sequent calculus is a style of formal logical argumentation (a sequence of statements/propositions/premises and one conclusion at the end). In sequent calculus, every line of a proof is a conditional tautology (which Gerhard Gentzen calls a sequent). This is in contrast to the earlier David Hilbert-style of formal logic, where every line is an *unconditional* tautology. Gentzen-style sequent calculus tends to have few axioms with more inference rules, whereas Hilbert-style formal logic tends to have more axioms and few inference rules. Other styles of *proof calculus* include: - [Hilbert style](https://en.wikipedia.org/wiki/Hilbert_system "Hilbert system"). Every line is an unconditional tautology (or theorem). - Gentzen style. Every line is a conditional tautology (or theorem) with zero or more conditions on the left. - [Natural deduction](https://en.wikipedia.org/wiki/Natural_deduction "Natural deduction"). Every (conditional) line has exactly one asserted proposition on the right. - Sequent calculus. Every (conditional) line has zero or more asserted propositions on the right. # Sequents A sequent is understood to mean that if all of the antecedent conditions are true, then at least one of the consequent formulas is true. 1. **Unconditional assertion**. No antecedent formulas. - Example: ⊢ _B_ - Meaning: _B_ is true. 2. **Conditional assertion**. Any number of antecedent formulas. 1. **Simple conditional assertion**. Single consequent formula. - Example: _A1_, _A2_, _A3_ ⊢ _B_ - Meaning: IF _A1_ AND _A2_ AND _A3_ are true, THEN _B_ is true. 2. **Sequent**. Any number of consequent formulas. - Example: _A1_, _A2_, _A3_ ⊢ _B1_, _B2_, _B3_, _B4_ - Meaning: IF _A1_ AND _A2_ AND _A3_ are true, THEN _B1_ OR _B2_ OR _B3_ OR _B4_ is true