more from this thinker | more from this text
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.
Clarification
A 'sequent' says something follows from something else
Gist of Idea
Each line of a sequent calculus is a conclusion of previous lines, each one explicitly recorded
Source
David Bostock (Intermediate Logic [1997], 7.1)
Book Ref
Bostock,David: 'Intermediate Logic' [OUP 1997], p.274
13759 | Each line of a sequent calculus is a conclusion of previous lines, each one explicitly recorded [Bostock] |
13760 | A sequent calculus is good for comparing proof systems [Bostock] |
15425 | The sequent calculus makes it possible to have proof without transitivity of entailment [Burgess] |
15426 | We can build one expanding sequence, instead of a chain of deductions [Burgess] |
13686 | We can build proofs just from conclusions, rather than from plain formulae [Sider] |