How do we begin to lay the foundations of a palace which is already more than 3600 years old? Alan Turing [Tur35] identified what is perhaps the one point of agreement between the Rhind papyrus and our own time, that a ``computer'' ( ie a mathematician performing a calculation) puts marks on a page and transforms them in some way. Even in its most naive form, Mathematics is not passive: we recite the multiplication table, transforming 7×8 into 56, and later find out that xx(y+z) may be replaced by (xxy)+(xxz). We say that these pairs are respectively equal, meaning that they denote the same objects in ``reality,'' even though they are written in different ways.
During the process of calculation (from Latin calx, a pebble) there are intermediate forms with no directly explicable meaning: accountants refer to ``net'' and ``gross'' amounts, and to ``pre-tax'' profits, in an attempt to give them one. The remarkable feature of mathematics is that we may suspend belief like this, and yet rely on the results of a lengthy calculation, even when it has been delegated to a computer.
The notation of elementary school arithmetic, which nowadays everyone takes for granted, took centuries to develop. There was an intermediate stage called syncopation, using abbreviations for the words for addition, square, root, etc . For example Rafael Bombelli ( c. 1560) would write
R. c. L. 2 p. di m. 11 L for our 3Ö{2+11i}.
Many professional mathematicians to this day use the quantifiers ( ",$) in a similar fashion,
$d > 0 s.t. |f(x)-f(x0)| < e if |x-x0| < d, for all e > 0,
in spite of the efforts of Gottlob Frege, Giuseppe Peano and Bertrand Russell to reduce mathematics to logic.
The logical calculus is easier to execute than any of the techniques of mathematics itself, yet only in 1934 did Gerhard Gentzen set it out in a natural way. Even now, mathematics students are expected to learn complicated (e- d)-proofs in analysis with no help in understanding the logical structure of the arguments. Examiners fully deserve the garbage that they get in return.
In Sections 1.4 and 1.5 natural deduction is introduced in a way which has been taught successfully to first year informatics undergraduates, for whom reasoning about the elementary details of their programs is a more pressing concern. Section 1.6 shows how formal methods correspond to carefully written proofs in the vernacular of mathematics and Section 1.7 formalises the way in which routine proofs are found, maybe by machine.
The manipulation of sets and relations more familiar to mathematics students is treated in Section 1.3 and Chapter II. If you are doubtful of the need for formal logic then I suggest reading the later chapters first.
In the spirit of starting out ``from nothing,'' the first two sections discuss the behaviour of purely symbolic manipulation. Nevertheless, the ideas which they introduce will play a substantial role in the rest of the book. We have, for example, to learn the difference between object-language and meta-language. Logic is primarily a meta-theory, and historically it has sought its object-language in some strange places: for medieval logicians, the motivation was theology. Today it is mathematics and programming, but in the first instance we shall apply logic to formal manipulation itself.
The final section discusses classical and intuitionistic logic, and why we intend to use the latter. This chapter and the next raise some of the questions of logic. The rest of the book uses modern tools to illuminate a few of those issues.