4.1 Introduction

It is of course not at all necessary to understand all the theory behind MacLogic to be able to use it effectively. But the interested student may (and the teacher must) enquire as to why it is as it is, and how it works. In this section we try to answer some of these questions.

First, note that with the availability of computers it is now feasible to mechanise most aspects of the tedious task of checking proofs for correctness. But one may also implement the methods (the algorithms) for constructing proofs, and then reflect on how much one wants to take away from the student the task of doing this for herself. Of course, one really wants to provide a variety of levels of help - from the completely automatic checking that a problem is solvable to sensible assistance to the student discovering her own proof. The computer's behaviour should ideally adapt to different levels of expertise: MacLogic, however, is adaptable rather than self-adapting.

Second, the use of computers has led to a re-evaluation of the use of different formal systems in proof presentation. On the one hand, some formal systems are now seen as less important, and others as more important: for example, Gentzen systems are now widely used for presenting the rules about types in programming languages, and for similar purposes in the study of natural language, whereas Hilbert-style axiomatic systems are now not commonly used outside certain formal textbooks on logic for mathematicians. On the other hand, it is clear that even some natural deduction systems are inconvenient to implement on a computer---and when one looks in detail at why, one finds that the difficulties are often those which are hard to explain to students. For example, the widely used textbook by Lemmon presents a system of natural deduction rules, some of which are messy to implement and hard to explain.

MacLogic began as an attempt to understand the problems involved in implementing a proof assistant for type theory [as in the work of Martin-Löf], with a view to the correct development of programs from specifications. Such assistants exist (NuPRL, PICTT, lego, IPE, ALF, Coq---see Bibliography for details). It acquired an independent life of its own as a teaching package, and is intended (by its authors) as an introduction to the kind of proof construction that all computer scientists should do when learning logic, because essentially the same kind of work is involved in programming. But this "art of proof construction" is essentially that which anyone has to do in constructing proofs, whatever their discipline. (It is usually not the same as the way machines are programmed to do it automatically.)

We describe therefore in the remaining sections of this chapter what sorts of formal system MacLogic is really using, and how they are related.