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

- the
**Autothin**check box in the dialog is checked, and - the formula is not an implication, a negation or a universal quantification.

**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.)