# Good textbook for learning Sequent Calculus

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)?

• According to my experience, a good way of practicing with "basic" sequent calculus, is to start 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. Of course, you can study directly sequent calculus with (e.g.) Sara Negri & Jan von Plato, Structural Proof Theory (2001). Commented Jan 23, 2014 at 20:25
• BTW you can use link in this form: [sequent calculus](http://en.wikipedia.org/wiki/Sequent_calculus) which is rendered in a post as: sequent calculus. See editing help. Commented Jan 27, 2014 at 14:43
• @Martin Sleziak - tanks ! I will improve my usage of links. Commented Jan 27, 2014 at 15:52
• @Mauro My comment was directed to the OP. (But if it is useful for others too, I am glad.) Commented Jan 27, 2014 at 16:42

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.

• @Peter_Smith I had a browse of Mendelson's "Introduction to Mathematical Logic" but it looks more about axiomatic logic than that it teaches how to do axiomatic logic (compare it with Hackstaff's "systems of formal logic", 1966 what is the only reasonable textbook on axiomatic logic I have seen) Lemmon's "beginning logic" is definitly Natural deduction, no way to do a logic that does not contian some structural rule. I think what I would like is a book that not assumes some structural rules so that weakening, contraction, self-distribution , assertion not automaticly become tautologies. Commented Jan 23, 2014 at 21:03
• I really can't see why Mendelson doesn't count as teaching how to do axiomatic logic -- it has done that to generations of students over 50 years. You can indeed say that Lemmon is natural deduction in sequent calculus style. Commented Jan 23, 2014 at 22:06
• Do you plan do to Goldrei's Propositional and Predicate Calculus in your guide? What kind of deduction system does this book use? Is it by the chance natural deduction? Commented Jan 24, 2014 at 12:34
• Goldrei uses much the same axiomatic system as Mendelson. Commented Jan 24, 2014 at 15:37
• @PeterSmith For example: Does Mendelson teach how to proof $(Q \to R) \to ((P \to Q) \to (P \to R))$ from the axioms $(P \to (Q \to R)) \to ((P \to Q) \to (P \to R))$ and $P \to (Q \to P)$ using universal substitution and modus ponens only? It was this kind of very basic hands-on axiomatic logic I was interested in. Most books I know just state you can proof it without really teaching how to do it. Hackstaff on the other hand spends 4 pages (61-64) on this proof alone. Commented Jan 25, 2014 at 17:12

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.

• It is again available in paperback : Gaisi Takeuti, Proof Theory: Second Edition (Dover Books on Mathematics, 2013). Commented Jan 30, 2014 at 15:41

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.

• Natural deduction is nor axiomatic nor Hilbert style. It is Gentzen style and has no axioms only inference rules. Commented Jan 26, 2014 at 20:09
• @MauroALLEGRANZA I don't know how well you know sequent calculus or axiomatic logic, but they are not upside down tableaux methods, even that axiomatic but "mimicks" ND is incorrect, it is more the other way around ND mimics axiomatic logic and does that in a bad way, ND has build-in assumptions (any theorem you can prove) while axiomatic logic has no build-in assumptions Commented Jan 27, 2014 at 22:55
• My suggestion to the OP was intended to sugegst way of "practicing" with different proof systems in order to learn how to "find" derivations. Using Kleene's axiomatic system is (for me) easier than Mendelson's, because Kleene introduce more axioms, corresponding to intro- ed elim-rules. So, e.g., the proof of $(A \land B) \rightarrow (A \lor B)$, can be "mimicked" from the ND's one in this way : (i) assume $A \land B$; (ii) with Ax $\vdash (A \land B) \rightarrow A$, apply modus ponens and get $A$; (iii) with Ax $\vdash A \rightarrow (A \lor B)$, apply mp and get $A \lor B$; 1/2 Commented Jan 28, 2014 at 7:49
• (iv) having obtained : $A \land B \vdash A \lor B$, apply deduction theorem and get : $\vdash (A \land B) \rightarrow (A \lor B)$. In this way, *if you have learned ND, you can practice with derivations in axiomatic systems. Commented Jan 28, 2014 at 7:52
• @Willemien - about the relationship between Gentzen systems and semantic tableaux, you can see at least : R.Smullyan, First-Order Logic (1969), Ch.XI, page 101-on; S.C.Kleene, Mathematical Logic (1967); Mordechai Ben-Ari, Mathematical Logic for Computer Science (3rd ed, 2012), page 51-on. Commented Jan 28, 2014 at 15:22