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.