#### 1.2 Proof construction* vs* presentation

Many textbooks of logic implicitly aim to teach the art of
presenting proofs in a certain format, the *natural deduction*
style. That is to say, complete proofs are presented, beginning
of course with simple proofs and moving on to more complex proofs.
After a short while, the complexity of these proofs becomes overwhelming,
and it is hard to see how they were obtained in the first place.
Sometimes hints are given, of course. More often than not, no
complete proofs are given after a certain stage, just instructions
on how one could produce a complete proof if one had to. Some
texts even present an even more forbidding format, the* axiomatic*
style, often ascribed to Hilbert: presentation of complete proofs
then ceases even earlier in the text. This style is convenient
if one is going to do meta-logic, but is not one in which anyone
ever constructs (non-trivial) proofs.

Unfortunately, the natural deduction style is, although well-suited
for use in the presentation of complete short proofs, also ill-suited
to your task of constructing proofs. An alternative style, called
the *sequent calculus*, is appropriate if you want to prove
something for yourself. MacLogic allows you to work in both styles:
in either **Check** mode or **Construct** mode, corresponding
respectively to the natural deduction style and the sequent calculus
style. **Check** mode is appropriate if you want to check an
existing natural deduction proof for correctness, and **Construct**
mode is used if you want to construct a proof for yourself. In
fact, the proof constructed is a sequent calculus proof: this
can be translated mechanically, if you wish, by MacLogic, to a
natural deduction proof, by the method outlined in section
4.3 below. The translation is fairly transparent.