more from this thinker     |     more from this text

Single Idea 15425

[filed under theme 5. Theory of Logic / H. Proof Systems / 6. Sequent Calculi ]

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.

Gist of Idea

The sequent calculus makes it possible to have proof without transitivity of entailment

Source

John P. Burgess (Philosophical Logic [2009], 5.3)

Book Ref

Burgess,John P.: 'Philosophical Logic' [Princeton 2009], p.105

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.

The 5 ideas with the same theme [proof were every step is a proof and not just a formula]:

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]
15426 We can build one expanding sequence, instead of a chain of deductions [Burgess]
15425 The sequent calculus makes it possible to have proof without transitivity of entailment [Burgess]
13686 We can build proofs just from conclusions, rather than from plain formulae [Sider]