Sequence calculus

In the proof theory and mathematical logic is denoted by sequent calculus a family of formal systems (or calculi ) that share a certain style of derivation and certain properties. The first sequential calculi, LK for classical and LJ for intuitionist logic, were introduced by Gerhard Gentzen in 1934 as a formal framework for the investigation of systems of natural reasoning in first-order predicate logic .

The Gentzensche law on LK and LJ says that the cut rule applies in these systems, a set of far-reaching consequences in the metalogic . The flexibility of the sequential calculus became apparent later, in 1936, when Gentzen used the cut-elimination technique to prove the consistency of Peano arithmetic .

The sequential calculi, which go back to Gentzen, and the general concepts behind them are used as standard in broad areas of proof theory, mathematical logic, and machine-aided proof .

Notations and conventions

The following characters are used in this article:

• ${\displaystyle \Gamma }$, ...: formula quantities ${\displaystyle \Phi }$
• ${\displaystyle \varphi }$, , ...: formulas of predicate logic ${\displaystyle \psi }$ ${\displaystyle \rho }$
• ${\displaystyle \vdash }$ : Sign for derivation relationship
• ${\displaystyle \vDash }$,  : Sign for the relation of logical truth / consequence ${\displaystyle \nvDash }$
• ${\displaystyle \neg }$ : Sign of negation
• ${\displaystyle \vee }$ : Adjunct sign
• ${\displaystyle \exists }$ : Existential quantifier
• ${\displaystyle (}$,  : Brackets as auxiliary characters for greater clarity ${\displaystyle )}$
• ${\displaystyle '}$ : Identification for the extension of a formula set
• ${\displaystyle {\mathfrak {M}}}$ : Symbol for model
• ${\displaystyle s}$ : (Character for variable allocation function)

The following conventions are introduced:

• By means of various rules, the remaining junctions can be converted into formulas, which then only contain and . The forming rules follow: ${\displaystyle \wedge ,\rightarrow ,\leftrightarrow }$ ${\displaystyle \neg }$ ${\displaystyle \vee }$
  • ${\displaystyle (\varphi \wedge \psi ):\Leftrightarrow (\neg (\neg \varphi \vee \neg \psi ))}$
  • ${\displaystyle (\varphi \rightarrow \psi ):\Leftrightarrow (\neg \varphi \vee \psi )}$
  • ${\displaystyle (\varphi \leftrightarrow \psi ):\Leftrightarrow (\neg (\neg (\neg \varphi \vee \psi )\vee \neg (\neg \psi \vee \varphi )))}$
• Using a conversion rule, the quantifier (universal quantifier) ​​can be represented as follows: ${\displaystyle \forall }$
  • ${\displaystyle \forall x\varphi :\Leftrightarrow \neg \exists x\neg \varphi }$

Use is made of these transformations in the examples.

introduction

The sequence calculus is used to map the procedure for mathematically proving theorems as precisely as possible. One component of this proof method is that additional requirements can be introduced at every point in the proof, which then either remain until the end or can be eliminated again.

The basic unit of the sequential calculus is a character string (a sequence) of variables , each of which stands for expressions of the logical system under consideration; z. B. for expressions of a first level language . We designate such a sequence with ${\displaystyle \phi _{i},\phi }$

${\displaystyle \phi _{1}\phi _{2}\dots \phi _{n}\phi }$

or shorter with

${\displaystyle \Gamma \phi ,}$

where stands for the sequence of expressions . The idea is that the conditions are in and the last link denotes the consequence of these conditions. The prerequisites are also known as the antecedent and the inference as the consequent. While the succession in the variant of the calculus shown here consists of only one formula, other variants, including Gentzen's LK, allow any number of formulas in the succession. ${\displaystyle \Gamma }$ ${\displaystyle \phi _{1},\dots ,\phi _{n}}$ ${\displaystyle \Gamma }$ ${\displaystyle \phi }$

The sequence calculus deals with the derivation of sequences . If there is a derivation of the sequence in the calculus , then one also writes ${\displaystyle \Gamma \phi }$

${\displaystyle \vdash \Gamma \phi .}$

Definition: The expression is called from derivable (short:) , if there is from with . ${\displaystyle \phi }$ ${\displaystyle \Phi }$ ${\displaystyle \Phi \vdash \phi }$ ${\displaystyle \phi _{1},\dots ,\phi _{n}}$ ${\displaystyle \Phi }$ ${\displaystyle \vdash \phi _{1},\dots ,\phi _{n},\phi }$

The sequence rules: general shape

In the following, the rules for the sequential calculus of classical first-order predicate logic are listed. Sequence rules have the general form

${\displaystyle {\frac {\Gamma _{1}\phi _{1},\Gamma _{2}\phi _{2},\dots ,\Gamma _{n}\phi _{n}}{\Gamma \phi }}.}$

Above the line are already derived sequences, and below the sequence that can be derived from them.

Different spelling

Sequence rules can also be found in the literature in the form

${\displaystyle {\frac {\Gamma _{1}\vdash \phi _{1},\Gamma _{2}\vdash \phi _{2},\dots ,\Gamma _{n}\vdash \phi _{n}}{\Gamma \vdash \phi }}}$

or as

${\displaystyle {\frac {\Gamma _{1}\Rightarrow \phi _{1},\Gamma _{2}\Rightarrow \phi _{2},\dots ,\Gamma _{n}\Rightarrow \phi _{n}}{\Gamma \Rightarrow \phi }}}$

written down.

Rules of the sequential calculus of first order predicate logic with identity

The rules of the sequential calculus of first order predicate logic with identity are divided into the following groups:

Basic rules, join rules, quantifier rules and identity rules.

Basic rules

The basic rules include the antecedent rule and the acceptance rule.

Antecedent rule

${\displaystyle \left({\text{Ant}}\right)\qquad {\frac {\Gamma \varphi }{\Gamma '\varphi }},}$

where: ${\displaystyle \Gamma \subseteq \Gamma '}$

In words: you can easily add assumptions.

Acceptance rule

${\displaystyle \left({\text{Ann}}\right)\qquad {\frac {}{\Gamma \varphi }},}$ where: ${\displaystyle \varphi \in \Gamma }$

In words: one can infer assumptions from them.

Juncture rules

The rules of connectivity include case distinction, contradiction, the introduction of adjunct in the antecedent and the introduction of adjunct as a consequence.

Case distinction

${\displaystyle \left({\text{FU}}\right)\qquad {\frac {\begin{aligned}{\Gamma \psi \varphi ,\Gamma \neg \psi \varphi }\end{aligned}}{\Gamma \varphi }}}$

In words: If one the one hand, assuming the other hand, assuming can derive, one may, without any assumption about or having to make, to close. ${\displaystyle \varphi }$ ${\displaystyle \psi }$ ${\displaystyle \neg \psi }$ ${\displaystyle \psi }$ ${\displaystyle \neg \psi }$ ${\displaystyle \varphi }$

Contradiction

${\displaystyle \left({\text{KD}}\right)\qquad {\frac {\begin{aligned}{\Gamma \neg \psi \rho ,\Gamma \neg \psi \neg \rho }\end{aligned}}{\Gamma \psi }}}$

In words: If leads to a contradiction, then one can conclude. ${\displaystyle \neg \psi }$ ${\displaystyle \psi }$

Adjunction introduction in the antecedent

${\displaystyle \left(\vee -{\text{Ant}}\right)\qquad {\frac {\begin{aligned}{\Gamma \varphi \rho ,\Gamma \psi \rho }\end{aligned}}{\Gamma (\varphi \vee \psi )\rho }}}$

In words, disjunctions of the form in the antecedent can be used in two ways - on the one hand in the case and on the other hand in the case . ${\displaystyle (\varphi \vee \psi )}$ ${\displaystyle \varphi }$ ${\displaystyle \psi }$

Adjunction introduction as a consequence

${\displaystyle \left(\vee -{\text{Kon1}}\right)\qquad {\frac {\begin{aligned}{\Gamma \varphi }\end{aligned}}{\Gamma (\varphi \vee \psi )}}}$

${\displaystyle \quad \left(\vee -{\text{Kon2}}\right)\qquad {\frac {\begin{aligned}{\Gamma \psi }\end{aligned}}{\Gamma (\varphi \vee \psi )}}}$

In words: You can always weaken the consequence by introducing an adjunct.

Quantifier rules

The quantifier rules include the introduction of existence as a consequence and the introduction of existence as an antecedent.

Introduction into existence as a consequence

${\displaystyle \left(\exists -{\text{Kon}}\right)\qquad {\frac {\Gamma \varphi {\frac {t}{x}}}{\Gamma \exists x\varphi }}}$

In words: If one can deduce from this that t has a property expressed by, then one can also infer that something exists which has a property expressed by. ${\displaystyle \Gamma }$ ${\displaystyle \varphi }$ ${\displaystyle \varphi }$

Introduction of existence in the antecedent

${\displaystyle \left(\exists -{\text{Ant}}\right)\qquad {\frac {\Gamma \varphi {\frac {y}{x}}\psi }{\Gamma \exists x\varphi \psi }}}$if y is not free in the sequence . ${\displaystyle \exists x\varphi \psi }$

Identity Rules

The rules of identity include reflexivity and the rule of substitution.

Reflexivity

${\displaystyle \left({\text{Ref}}\right)\qquad {\frac {}{t\equiv t}}}$

In words: The equivalence relation on the subject area D is reflexive.

Substitution rule

${\displaystyle \left(\exists -{\text{Sub}}\right)\qquad {\frac {\Gamma \varphi {\frac {t}{x}}\psi }{\Gamma t\equiv t'\varphi {\frac {t'}{x}}\psi }}}$

In words: inserting the identical into the identical.

Useful derivations

With the rules of the sequential calculus set out above, some more useful rules are now derived in finitely many steps. To distinguish them from the above basic rules , they are also called derived rules . (As a reminder: derivation is to be equated with sequence manipulation by applying the rules.) These rules, once derived, can then be used without any problems, that is, it is sufficient to show their derivation here once. Here the following rules are proven: the principle of the excluded third , the triviality , the chain closure , the contraposition and the disjunctive syllogism . Regarding the notation: Each derivation is divided into three columns. The numbering of the individual modifications is in the left column. They are useful for unambiguous reference through other modifications. The middle column contains the new modification, with a succession of sequences as a result. The right column contains the information on how the sequence in the middle column was achieved. The rule is written in brackets, and possibly, preceded by a colon (read as “applied to”), the line numbers relevant to the result are noted. Example: "(Ant): 1., 2." is read as "Antecedent rule, applied to lines one and two".

Sentence of the excluded third party

${\displaystyle \left({\text{AD}}\right)\qquad {\frac {}{\varphi \vee \neg \varphi }}}$

Derivation:

${\displaystyle {\begin{alignedat}{3}1.\quad &\varphi \varphi &\quad &({\text{Ann}})\\2.\quad &\varphi (\varphi \vee \neg \varphi )&\quad &(\vee -{\text{Kon1}}):1.\\3.\quad &\neg \varphi \neg \varphi &\quad &({\text{Ann}})\\4.\quad &\neg \varphi (\varphi \vee \neg \varphi )&\quad &(\vee -{\text{Kon2}}):3.\\5.\quad &(\varphi \vee \neg \varphi )&\quad &({\text{FU}}):2.,4.\end{alignedat}}}$

triviality

${\displaystyle \left({\text{Triv}}\right)\qquad {\frac {\begin{aligned}\Gamma \varphi ,\Gamma \neg \varphi \end{aligned}}{\Gamma \psi }}}$

Derivation:

${\displaystyle {\begin{alignedat}{3}1.\quad &\Gamma \varphi &\quad &({\text{Prämisse}})\\2.\quad &\Gamma \neg \varphi &\quad &({\text{Prämisse}})\\3.\quad &\Gamma \neg \psi \varphi &\quad &({\text{Ant}}):1.\\4.\quad &\Gamma \neg \psi \neg \varphi &\quad &({\text{Ant}}):2.\\5.\quad &\Gamma \psi &\quad &({\text{KD}}):3.,4.\end{alignedat}}}$

Chain link

${\displaystyle \quad \left({\text{KS}}\right)\qquad {\frac {\begin{aligned}\Gamma \varphi \psi ,\Gamma \varphi \end{aligned}}{\Gamma \psi }}}$

Derivation:

${\displaystyle {\begin{alignedat}{3}1.\quad &\Gamma \varphi \psi &\quad &({\text{Prämisse}})\\2.\quad &\Gamma \varphi &\quad &({\text{Prämisse}})\\3.\quad &\Gamma \neg \varphi \varphi &\quad &({\text{Ant}}):2.\\4.\quad &\Gamma \neg \varphi \neg \varphi &\quad &({\text{Ann}})\\5.\quad &\Gamma \neg \varphi \psi &\quad &({\text{Triv}}):3.,4.\\6.\quad &\Gamma \psi &\quad &({\text{FU}}):1.,5.\end{alignedat}}}$

Note: The rule (trivial) was used in this derivation. This example shows that a rule only needs to be derived once without errors; it can subsequently be used as an abbreviation. By using the rule (Triv), five steps of derivation have been left out (namely the five steps that are required to derive (Triv)).

Counterposition

${\displaystyle \left(KP1\right)\qquad {\frac {\Gamma \varphi \psi }{\Gamma \neg \psi \neg \varphi }}}$

${\displaystyle \left(KP2\right)\qquad {\frac {\Gamma \varphi \neg \psi }{\Gamma \psi \neg \varphi }}}$

${\displaystyle \left(KP3\right)\qquad {\frac {\Gamma \neg \varphi \psi }{\Gamma \neg \psi \varphi }}}$

${\displaystyle \left(KP4\right)\qquad {\frac {\Gamma \neg \varphi \neg \psi }{\Gamma \psi \varphi }}}$

Derivation of (KP1) ((KP2) - (KP4) analogous):

${\displaystyle {\begin{alignedat}{3}1.\quad &\Gamma \varphi \psi &\quad &({\text{Prämisse}})\\2.\quad &\Gamma \neg \psi \varphi \psi &\quad &({\text{Ant}}):1.\\3.\quad &\Gamma \neg \psi \varphi \neg \psi &\quad &({\text{Ann}})\\4.\quad &\Gamma \neg \psi \varphi \neg \varphi &\quad &({\text{Triv}}):2.,3.\\5.\quad &\Gamma \neg \psi \neg \varphi \neg \varphi &\quad &({\text{Ann}})\\6.\quad &\Gamma \neg \psi \neg \varphi &\quad &({\text{FU}}):4.,5.\end{alignedat}}}$

Disjunctive syllogism

${\displaystyle \left(DS\right)\qquad {\frac {\begin{aligned}\Gamma (\varphi \vee \psi ),\Gamma \neg \varphi \end{aligned}}{\Gamma \psi }}}$

Derivation:

${\displaystyle {\begin{alignedat}{3}1.\quad &\Gamma (\varphi \vee \psi )&\quad &({\text{Prämisse}})\\2.\quad &\Gamma \neg \varphi &\quad &({\text{Prämisse}})\\3.\quad &\Gamma \varphi \neg \varphi &\quad &({\text{Ant}}):2.\\4.\quad &\Gamma \varphi \varphi &\quad &({\text{Ann}})\\5.\quad &\Gamma \varphi \psi &\quad &({\text{Triv}}):4.,3.\\6.\quad &\Gamma \psi \psi &\quad &({\text{Ann}})\\7.\quad &\Gamma (\varphi \vee \psi )\psi &\quad &(\vee -{\text{Ant}}):5.,6.\\8.\quad &\Gamma \psi &\quad &({\text{KS}}):7.,1.\end{alignedat}}}$

Properties of the sequential calculus

correctness

The correctness principle is as follows:

The following applies to all formula sets and all formulas : If , then . ${\displaystyle \Phi }$ ${\displaystyle \varphi }$ ${\displaystyle \Phi \vdash \varphi }$ ${\displaystyle \Phi \vDash \varphi }$

The correctness of the sequential calculus is shown by the fact that it is shown for each individual rule of the sequential calculus that it is correct, that is, that each model and each variable assignment s that make the premises of the rule true also make its consequence true. All correctness proofs taken together then result in the proof of the correctness theorem. ${\displaystyle {\mathfrak {M}}}$

Definitions

In order to be able to show the correctness theorem, “model”, “variable allocation” and “make true” (logical truth) must first be defined.

model

A model is an ordered pair such that: ${\displaystyle {\mathfrak {M}}=(D,{\mathfrak {I}})}$

1. ${\displaystyle D}$is a non-empty set (the carrier or the subject area , English domain , over which the quantifiers run)
2. ${\displaystyle {\mathfrak {I}}}$ is the interpretation function for predicates, functions and constants (not relevant in the following)

Variable assignment

A variable assignment s over a model is a function . ${\displaystyle {\mathfrak {M}}=(D,{\mathfrak {I}})}$ ${\displaystyle s:\{v_{0},v_{1},\dots \}\rightarrow D}$

Logical truth / consequence

The following applies to all formulas and all formula sets : follows logically from (short:) iff for all models and all variable assignments s above applies: If , then . (In other words: Every which makes true even makes true.) ${\displaystyle \varphi }$ ${\displaystyle \Phi }$ ${\displaystyle \varphi }$ ${\displaystyle \Phi }$ ${\displaystyle \Phi \vDash \varphi }$ ${\displaystyle {\mathfrak {M}}}$ ${\displaystyle {\mathfrak {M}}}$ ${\displaystyle {\mathfrak {M}},s\vDash \Phi }$ ${\displaystyle {\mathfrak {M}},s\vDash \varphi }$ ${\displaystyle {\mathfrak {M}},s}$ ${\displaystyle \Phi }$ ${\displaystyle \varphi }$

Correctness of the rules of the sequential calculus

The correctness of the rules of sequential calculus is shown by showing the logical truth of the rules. This is based on the definition of the logical truth / sequence. Now it is shown that every single rule of the sequential calculus is logically true. (Not all of the evidence is shown. It is sufficient to outline a few. The rest of the evidence is structurally similar.)

Correctness of (Ant)

Assuming is correct, i.e. H. . Be a set of formulas, so that: . Be chosen arbitrarily, so that: . Then also and according to the prerequisite also applies . It follows from this . So is correct. ${\displaystyle \Gamma \varphi }$ ${\displaystyle \Gamma \vDash \varphi }$ ${\displaystyle \Gamma '}$ ${\displaystyle \Gamma \subseteq \Gamma '}$ ${\displaystyle {\mathfrak {M}},s}$ ${\displaystyle {\mathfrak {M}},s\vDash \Gamma '}$ ${\displaystyle {\mathfrak {M}},s\vDash \Gamma }$ ${\displaystyle {\mathfrak {M}},s\vDash \varphi }$ ${\displaystyle \Gamma '\vDash \varphi }$ ${\displaystyle \Gamma '\varphi }$

Correctness of (Ann)

If so , then applies . Thus is correct. ${\displaystyle \varphi \in \Gamma }$ ${\displaystyle \Gamma \vDash \varphi }$ ${\displaystyle \Gamma \varphi }$

Correctness of (FU)

Assumed and are correct, i.e. H. and . Be chosen arbitrarily, so that: . ${\displaystyle \Gamma \psi \varphi }$ ${\displaystyle \Gamma \neg \psi \varphi }$ ${\displaystyle \Gamma \cup \{\psi \}\vDash \varphi }$ ${\displaystyle \Gamma \cup \{\neg \psi \}\vDash \varphi }$ ${\displaystyle {\mathfrak {M}},s}$ ${\displaystyle {\mathfrak {M}},s\vDash \Gamma }$

Case 1: . Then and thus according to the requirement . ${\displaystyle {\mathfrak {M}},s\vDash \psi }$ ${\displaystyle {\mathfrak {M}},s\vDash \Gamma \cup \{\psi \}}$ ${\displaystyle {\mathfrak {M}},s\vDash \varphi }$

Case 2: . Then . Then and thus according to the requirement . ${\displaystyle {\mathfrak {M}},s\nvDash \psi }$ ${\displaystyle {\mathfrak {M}},s\vDash \neg \psi }$ ${\displaystyle {\mathfrak {M}},s\vDash \Gamma \cup \{\neg \psi \}}$ ${\displaystyle {\mathfrak {M}},s\vDash \varphi }$

The following applies in both cases . Thus is correct. ${\displaystyle \Gamma \vDash \varphi }$ ${\displaystyle \Gamma \varphi }$

Correctness of (KD)

Adopted and . Then applies to everyone with : ${\displaystyle \Gamma \cup \{\neg \psi \}\vDash \rho }$ ${\displaystyle \Gamma \cup \{\neg \psi \}\vDash \neg \rho }$ ${\displaystyle {\mathfrak {M}},s}$ ${\displaystyle {\mathfrak {M}},s\vDash \Gamma \cup \{\neg \psi \}}$

${\displaystyle {\mathfrak {M}},s\vDash \rho }$and . Then there is no , so that: . Then for all with : . Thus it applies and is therefore correct. ${\displaystyle {\mathfrak {M}},s\nvDash \rho }$ ${\displaystyle {\mathfrak {M}},s}$ ${\displaystyle {\mathfrak {M}},s\vDash \Gamma \cup \{\neg \psi \}}$ ${\displaystyle {\mathfrak {M}},s}$ ${\displaystyle {\mathfrak {M}},s\nvDash \psi }$ ${\displaystyle {\mathfrak {M}},s\nvDash \Gamma }$ ${\displaystyle \Gamma \vDash \psi }$ ${\displaystyle \Gamma \psi }$

If the remaining rules have also been proven, i.e. their correctness has been shown, the correctness theorem has been proven and it can be said: If a formula in the sequence calculus can be derived, then this formula is also logically true.

completeness

The calculation is also complete . That means that:

The following applies to all formula sets and all formulas : If , then . ${\displaystyle \Phi }$ ${\displaystyle \varphi }$ ${\displaystyle \Phi \vDash \varphi }$ ${\displaystyle \Phi \vdash \varphi }$

Intuitively, this means that all true sequences can be derived using the rules given above.

Examples

Finally, two examples with the sequence calculus should be presented.

example 1

${\displaystyle {\frac {\Gamma \varphi \psi }{\Gamma \varphi \rightarrow \psi }}}$

Derivation:

${\displaystyle {\begin{alignedat}{3}1.\quad &\Gamma \varphi \psi &\quad &({\text{Prämisse}})\\2.\quad &\Gamma \varphi (\neg \varphi \vee \psi )&\quad &(\vee -{\text{Kon}}):1.\\3.\quad &\Gamma \neg \varphi \neg \varphi &\quad &({\text{Ann}})\\4.\quad &\Gamma \neg \varphi (\neg \varphi \vee \psi )&\quad &(\vee -{\text{Kon}}):3.\\5.\quad &\Gamma (\neg \varphi \vee \psi )&\quad &({\text{FU}}):2.,4.\\6.\quad &\Gamma (\varphi \rightarrow \psi )&\quad &({\text{Umformung}}).\end{alignedat}}}$

Example 2

${\displaystyle {\frac {\Gamma \varphi \wedge \psi }{\Gamma \varphi }}}$

Derivation:

${\displaystyle {\begin{alignedat}{3}1.\quad &\Gamma \varphi \wedge \psi &\quad &({\text{Prämisse}})\\2.\quad &\Gamma \neg (\neg \varphi \vee \neg \psi )&\quad &({\text{Umformung}})\\3.\quad &\Gamma \neg \varphi \neg \varphi &\quad &({\text{Ann}})\\4.\quad &\Gamma \neg \varphi (\neg \varphi \vee \neg \psi )&\quad &(\vee -{\text{Kon}}):3.\\5.\quad &\Gamma \neg \varphi \neg (\neg \varphi \vee \neg \psi )&\quad &({\text{Ant}}):2.\\6.\quad &\Gamma \neg \varphi \varphi &\quad &({\text{Triv}}):4.,5.\\7.\quad &\Gamma \varphi \varphi &\quad &({\text{Ann}})\\8.\quad &\Gamma \varphi &\quad &({\text{FU}}):7.,6.\end{alignedat}}}$

literature

• Heinz-Dieter Ebbinghaus , Jörg Flum, Wolfgang Thomas: Introduction to mathematical logic. Berlin: Springer-Verlag, 2007.
• Gerhard Gentzen (ed. ME Szabo): The Collected Papers of Gerhard Gentzen , Amsterdam 1969.
• Wolfgang Rautenberg : Introduction to Mathematical Logic. A textbook . 3rd, revised edition. Vieweg + Teubner, Wiesbaden 2008, ISBN 978-3-8348-0578-2 .
• Gaisi Takeuti : Proof theory (=  Studies in logic and the foundations of mathematics . Volume 81 ). 2nd Edition. North-Holland, Amsterdam 1987, ISBN 0-444-87943-9 .
• Richter, MM: logic calculations. Stuttgart: Teubner Verlag, 1978.
• AS Troelstra , H. Schwichtenberg . Basic Proof Theory (Cambridge Tracts in Theoretical Computer Science). Cambridge University Press, ISBN 0-521-77911-1 .

Web links

• Sequent Calculus by Alex Sakharov MathWorld
• Jan von Plato :  The Development of Proof Theory: Natural deduction and sequent calculus. In: Edward N. Zalta (Ed.): Stanford Encyclopedia of Philosophy .
• Frederic Portoraro:  Automated Reasoning: Sequent Deduction. In: Edward N. Zalta (Ed.): Stanford Encyclopedia of Philosophy .