For example, Lemmon (1965) used the word "sequent" strictly for simple conditional assertions with one and only one consequent formula.
In a general sequent of the form both Γ and Σ are sequences of logical formulas, not sets.
Consequently the three pairs of structural rules called "thinning", "contraction" and "interchange" are not required.)
In the extreme case where the list of antecedent formulas of a sequent is empty, the consequent is unconditional.
An empty antecedent formula list is equivalent to the "always true" proposition, called the "verum", denoted "⊤".
In the extreme case where the list of consequent formulas of a sequent is empty, the rule is still that at least one term on the right be true, which is clearly impossible.
The doubly extreme case ' ⊢ ', where both the antecedent and consequent lists of formulas are empty is "not satisfiable".
(See also the full set of sequent calculus inference rules.)
The assertion symbol in sequents originally meant exactly the same as the implication operator.
But over time, its meaning has changed to signify provability within a theory rather than semantic truth in all models.
In 1934, Gentzen did not define the assertion symbol ' ⊢ ' in a sequent to signify provability.
In 1939, Hilbert and Bernays stated likewise that a sequent has the same meaning as the corresponding implication formula.
[5] In 1944, Alonzo Church emphasized that Gentzen's sequent assertions did not signify provability.
Curry in 1963,[7] Lemmon in 1965,[2] and Huth and Ryan in 2004[8] all state that the sequent assertion symbol signifies provability.
However, Ben-Ari (2012, p. 69) states that the assertion symbol in Gentzen-system sequents, which he denotes as ' ⇒ ', is part of the object language, not the metalanguage.
[9] According to Prawitz (1965): "The calculi of sequents can be understood as meta-calculi for the deducibility relation in the corresponding systems of natural deduction.
"[10] And furthermore: "A proof in a calculus of sequents can be looked upon as an instruction on how to construct a corresponding natural deduction.
"[11] In other words, the assertion symbol is part of the object language for the sequent calculus, which is a kind of meta-calculus, but simultaneously signifies deducibility in an underlying natural deduction system.
A sequent is a formalized statement of provability that is frequently used when specifying calculi for deduction.
Barring any contradictions in the technically precise definition above we can describe sequents in their introductory logical form.
represents a set of assumptions that we begin our logical process with, for example "Socrates is a man" and "All men are mortal".
In many cases, sequents are also assumed to consist of multisets or sets instead of sequences.
For classical propositional logic this does not yield a problem, since the conclusions that one can draw from a collection of premises do not depend on these data.
Natural deduction systems use single-consequence conditional assertions, but they typically do not use the same sets of inference rules as Gentzen introduced in 1934.
In particular, tabular natural deduction systems, which are very convenient for practical theorem-proving in propositional calculus and predicate calculus, were applied by Suppes (1999) and Lemmon (1965) for teaching introductory logic in textbooks.
However, in English, the word "sequence" is already used as a translation to the German "Folge" and appears quite frequently in mathematics.
The term "sequent" then has been created in search for an alternative translation of the German expression.