4.3 Sequent calculi

The problem with natural deduction is that it is often not clear, even for simple problems, how to construct proofs. Ideally, you should be guided by your knowledge of the rules and the syntax of the problem to be solved. Gentzen therefore introduced a related system, called the sequent calculus, in which there are rules for introduction of the logical constants on the right of the turnstile, and (instead of elimination rules) rules for introduction of the constants on the left. (For details, see the literature, such as Gentzen's original papers, or the survey by Sundholm.)

To understand how MacLogic works, it is vital to recognise that the sequent calculus rules can be regarded, upside down, as tactics for decomposing problems: and that a sequent calculus proof can be regarded (at least in the intuitionistic case) as a recipe for constructing a natural deduction proof.

For example, the intuitionistic sequent calculus rule for "&-introduction on the left" is of the form

where F, G are formula lists and A, B, C are formulae. Let us suppose that we can convert the proof leading to the premiss of this rule instance into a proof of C from the assumptions in F, from A, from B, and from those in G: we can now see how to construct a proof from the assumptions in F, from A&B and from those in G: we add A&B as an assumption, derive from it the formulae A, B by the natural deduction rule &E, and replace the uses (if any) of the assumptions A, B by appeals to A (resp. B) based on the new assumption of A&B. We therefore see the rule of "&-introduction on the left" (in the sequent calculus) as an instruction to use the rule &E in constructing a natural deduction proof. Accordingly, the tactics in MacLogic are named, for example, "Tactic for &E", etc, rather than after the sequent calculus rules themselves. Below we shall often talk about use of a tactic for a natural deduction rule rather than naming the appropriate sequent calculus rule.

This view of sequent calculus rules as tactics for use of natural deduction rules works well for the intuitionistic case: we leave it to the interested reader to work out the correspondence for the other logical constants as an exercise. Accordingly, it is a simple mechanical task to convert a sequent calculus proof (as built in the Derivation window, with the root of the tree at the top left and the leaves at points marked by ) into a natural deduction proof. This is done for you by MacLogic: but you should try to think, as you perform the simple proofs, just how the tactics you are using could be used to construct a natural deduction proof as you go along rather than at the end of the process. Note that the leaves of the derivation turn not into the assumption sequents in the natural deduction proof, but into the minimal sequents, in the middle of the proof, being (in general) both conclusions of elimination rules and premisses of introduction rules.

In the classical case, we use not Gentzen's sequent calculus LK, but that (LJ) for intuitionistic logic, augmented by a double negation rule (upside down, of course, as a tactic). The translation into a natural deduction proof is now easy --- whereas if we used LK, with sequents having multiple consequents, the translation into natural deduction is non-trivial. (It is for this reason that MacLogic's automatic theorem prover gives no advice about how to solve problems: it is based, in the classical case, for efficiency, on the LK calculus, and although it could advise on how to solve a problem in the LK formalism, this is not particularly helpful.)

One very instructive example is the proof of the "Law of Excluded Middle", AÎÒA, in classical logic. (In the sequent calculus LK, allowing multiple consequents on the right, this is trivial--- the proof takes two lines: the first step breaks up the disjunction, obtainingA,ÒA; the next step breaks up the negation, obtaining AA, which is an axiom.)

In the sequent calculus LJ augmented with a double negation rule DN, the first step (using the tactic for DN) is to pose the more complex problemÒÒ(AÎÒA), now to use the tactic for ÒI, obtaining the problem Ò(AÎÒA)Ï, then the tactic for ÒE, obtaining Ò(AÎÒA)AÎÒA, then that for ÎI, obtaining Ò(AÎÒA)ÒA, then that for ÒI, obtaining A,Ò(AÎÒA) Ï, then that for ÒE again, obtaining AÒ(AÎÒA)AÎÒA, and (finally), that for ÎI again. (Two trivial sub-problems have been omitted.)

As a sequent calculus proof (in LJ + DN) we have it as

and as a natural deduction proof, in Lemmon's notation, we have it as

 1 (1)   Ò(AÎÒA) Ass
 2 (2)   A Ass
2 (3)   AÎÒA 2 ÎI
1,2 (4)   Ï 1,3 ÒE
1 (5)   ÒA 2,4 ÒI
1 (6)   AÎÒA 5 ÎI
1 (7)   Ï 1,6 ÒE
  (8)   ÒÒ(AÎÒA) 1,7 ÒI
  (9)   AÎÒA 8, DN

Note that there is a straightforward translation of the sequent calculus (in LJ + DN) proof into a natural deduction proof, but no simple translation is available from the proof in LK. Note also that, in the sequent calculus proof, as we move from the root to the leaves, we have on the left a formula Ò(AÎÒA), which is broken up (i.e. "analysed") using the tactic for ÒE, giving us the formula AÎÒA on the right (in the problem on the leftmost branch of the tree) and a trivial problem ÏÏ in the rightmost branch. But in the problem on the left, we have still the "broken up" formula Ò(AÎÒA) in the antecedent, and this is broken up at the point further up the tree where the tree branches again.

This phenomenon, that as we break formulae up we cannot always throw them away, is an inconvenience of LJ (with or without DN): it adds significantly to the cost of automatic theorem proving in intuitionistic logic. It does not appear in LK (until we consider the effect of the quantifiers), which is why it is relatively easy mechanically to decide problems in zero-order classical logic. But it is also a reason why finding natural deduction proofs in classical logic can be non-trivial, even in the zero-order case: witness the above example.

MacLogic's Construct mode allows you, in two ways, to control whether or not formulae are thrown away as you break them up. (Clearly, when a formula on the right of thesymbol is broken up, there is nowhere in the statement of the new sub-problem(s) to put the old formula.) When a formula on the left is the formula on which the tactic operates, it is removed if

Autothin's being checked is a sign to MacLogic that it can remove such formulae; but it will not do so if the formula is one of the kind to which the above comments about the possibility of their being needed again apply, i.e. is an implication, is a negation or is universally quantified. If the formula is not removed, and you really want to clear it out of the way, then use the Thin tactic, via the ... button on the dialog.

To repeat: MacLogic's Construct mode is based on the use of Gentzen's calculus LJ (perhaps with a DN rule for classical logic, or perhaps without the Ï-Intro_left rule---what we call the ÏE tactic---for minimal logic), in which the rules are regarded upside down as tactics for building natural deduction proofs. (The idea is already in the work of Gentzen & Prawitz.)