Good textbook for learning Sequent Calculus

Question

There are many modern text books teaching logic using Natural Deduction.

There are no books teaching logic using the axiomatic method (see Good book for learning and practising axiomatic logic )

Now in another post (Prove by introduction rules (P ⇒ Q) || (Q ⇒ R)⇒ (P NOT Q ⇒ R), (P ⇒ Q)⇒ !Q⇒ !P + more. ) somebody is struggling with sequent calculus ( http://en.wikipedia.org/wiki/Sequent_calculus )

Are there good textbooks to study logic using the sequent calculus method (or do you just have to be fluent in natural deduction before you should even have a look at it)?

Answer 1

1) I don't agree -- to respond to your initial remark -- that there are no good books teaching logic using the axiomatic method. Many classic texts do just that, famously Mendelson (which taught me serious logic, many moons ago). Of more recent axiomatic texts, Leary's Friendly Introduction is terrific. And for a book very carefully written for self-study, Goldrei's Propositional and Predicate Calculus seems excellent (I says "seems" as I've only just found out about this text!).

2) But to respond to the main question, about sequent calculi: I'm not sure what level of text you are looking for. (And it also depends what exactly you count as a sequent calculus. In one sense, Lemmon's classic introductory text Beginning Logic can be said to use a sequent calculus in very thin disguise. Instead of writing a sequent as $A, B, C \Longrightarrow D$, say, he writes something like $1,4,7\ (n)\ D$ where the numbers on the left of the line-number refer back to the lines at which $A$, $B$ and $C$ respectively appear as assumptions, and then he writes his proofs linearly rather than as trees.)

But, for someone who knows a little logic already and who wants a Gentzen-style presentation, I'd say the place to start is Sara Negri and Jan von Plato's very nice text Structural Proof Theory.

Answer 2

I think that you complaint can be addressed searching for good textbooks with exercise (quite all), hints for solution (not all) and, for more recent one, support material available on the web.

A textbook that offer all this is George Boolos & John Burgess & Richard Jeffrey, Computability and Logic (5th ed - 2007); unfortunately the exposition is not (I think) fitted for practicing with proof systems.

My personal experience is that you can practice with different methods and then try to benefit from their interrelations.

For example, I've found my preferred proof system with tableaux method (see R.Smullyan, First-Order Logic (1969, Dover reprint) ) and then observe that the sequent rules are the tableaux rules written "upside-down". In this way, starting from the bottom [e.g. with the sequent : $\rightarrow A$] and applying "backward" tableaux rules, you will be able to construct the sequent proof.

Another approach that I've found useful is to practice with Natural Deduction, that is quite easy to learn. Then you can "apply" this ability to axiomatic (or Hilbert-style) systems, translating your Natural Deduction proofs into Hilbert system, that is axiomatic but "mimicks" ND [see also S.C.Kleene, Mathematical Logic (1967, Dover reprint)].

This proof system, unlike Mendelson's, uses "more" axioms; for example (see Kleene, page 15) conjunction ($\land$) is "managed" by :

$\vdash A \rightarrow (B \rightarrow (A \land B))$

and

$\vdash (A \land B) \rightarrow A$ and $\vdash (A \land B) \rightarrow B$

that are really introduction- and elimination-rules in "axiomatic" form.

Answer 3

I learned sequent calculus from the first couple of chapters of Takeuti's text (Proof Theory, now out of print: http://www.amazon.com/Proof-Theory-Studies-Foundations-Mathematics/dp/0444879439).

I can't really compare it with other texts, but I found it worked well for me.