more from this thinker     |     more from this text

---

Single Idea 13686

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

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.

Gist of Idea

We can build proofs just from conclusions, rather than from plain formulae

Source

Theodore Sider (Logic for Philosophy [2010], 2.5.1)

Book Ref

Sider,Theodore: 'Logic for Philosophy' [OUP 2010], p.39

---

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.

---

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]