structure for 'Theory of Logic'    |     alphabetical list of themes    |     unexpand these ideas

5. Theory of Logic / H. Proof Systems / 6. Sequent Calculi

[proof were every step is a proof and not just a formula]

5 ideas
Each line of a sequent calculus is a conclusion of previous lines, each one explicitly recorded [Bostock]
     Full Idea: A sequent calculus keeps an explicit record of just what sequent is established at each point in a proof. Every line is itself the sequent proved at that point. It is not a linear sequence or array of formulae, but a matching array of whole sequents.
     From: David Bostock (Intermediate Logic [1997], 7.1)
A sequent calculus is good for comparing proof systems [Bostock]
     Full Idea: A sequent calculus is a useful tool for comparing two systems that at first look utterly different (such as natural deduction and semantic tableaux).
     From: David Bostock (Intermediate Logic [1997], 7.2)
We can build one expanding sequence, instead of a chain of deductions [Burgess]
     Full Idea: Instead of demonstrations which are either axioms, or follow from axioms by rules, we can have one ever-growing sequence of formulas of the form 'Axioms |- ______', where the blank is filled by Axioms, then Lemmas, then Theorems, then Corollaries.
     From: John P. Burgess (Philosophical Logic [2009], 5.3)
The sequent calculus makes it possible to have proof without transitivity of entailment [Burgess]
     Full Idea: It might be wondered how one could have any kind of proof procedure at all if transitivity of entailment is disallowed, but the sequent calculus can get around the difficulty.
     From: John P. Burgess (Philosophical Logic [2009], 5.3)
     A reaction: He gives examples where transitivity of entailment (so that you can build endless chains of deductions) might fail. This is the point of the 'cut free' version of sequent calculus, since the cut rule allows transitivity.
We can build proofs just from conclusions, rather than from plain formulae [Sider]
     Full Idea: We can construct proofs not out of well-formed formulae ('wffs'), but out of sequents, which are some premises followed by their logical consequence. We explicitly keep track of the assumptions upon which the conclusion depends.
     From: Theodore Sider (Logic for Philosophy [2010], 2.5.1)
     A reaction: He says the method of sequents was invented by Gerhard Gentzen (the great nazi logician) in 1935. The typical starting sequents are the introduction and elimination rules. E.J. Lemmon's book, used in this database, is an example.