Single Idea 13686

[catalogued under 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 Reference

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.