First Order Reasoning

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(x_{0})| < e if |x-x_{0}| < 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.