on these data. In substructural logic, however, this may become quite important. 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 and for teaching introductory logic in textbooks. Etymology Historically, sequents have been introduced by Gerhard Gentzen in order to specify his famous sequent calculus. In his German publication he used the word "Sequenz". 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. Kleene makes the following comment on the translation into English: "Gentzen says 'Sequenz', which we translate as 'sequent', because we have already used 'sequence' for any succession of objects, where the German is 'Folge'." See also Gerhard Gentzen Intuitionistic logic Natural deduction Sequent calculus Notes References External links Proof theory Logical expressions