Computer Aided Formal Reasoning 1996/7 Lecture notes 1 Judith Underwood

This course covers foundations for and applications of computer aided formal reasoning. We will be particularly interested in formal reasoning related to computer science, namely, reasoning about programs and data types. Because of this, we will use a constructive logic which naturally has a deep connection with computation.

We begin the course with a historical survey which describes the development of logic, and constructive logic in particular. The history is particularly interesting because the motivation was not originally expressly computational – the ideas of this logic were developed before computers existed. We will then begin to describe constructive logic more formally.

1 What is a proof?

The notion of what a proof is has changed over time, particularly in the last hundred years. The work of Euclid (c. 300 B.C.E.) described geometry as developed from five fundamental axioms which were considered obviously true. There were a number of logical rules which could be used to put together axioms and theorems.

Geometry was then considered to be the foundation of mathematics. As geometry developed to encompass the study of graphs of functions, and hence the functions themselves, it began to lose the geometrical meaning and intuition present in Euclid. It also lost the foundation which Euclid had built. For example, the early justifications for the differential and integral calculus relied on “infinitesimals” – quantities with no measurable size, yet which were not zero. Many people felt that constructions like these were unsatisfactory and searched for alternatives.

In the mid- to late-nineteenth century, several approaches were proposed. All involved a reformulation of the real numbers, which had until then been normally justified by the geometric intuition of the line. Weierstrass (1815-1897) developed a theory of limits which allowed real numbers to be expressed as the limit of a sequence of rationals; Dedekind (1861-1916) and Cantor (1829-1920) also developed theories of the real numbers based on properties and sets.

At about the same time, non-Euclidean geometry was developing, contradicting the implicit notion of Euclid that his five axioms were somehow eternal and fundamental. It became apparent that geometry was insufficient for justifying mathematics, and other approaches were tried through arithmetic, logic, and set theory. Set theory seemed particularly promising, but Betrand Russell (1872-1970) discovered that Cantor’s original formulation lead to paradoxes.

The most famous of these is called (surprise!) Russell’s paradox. It consists of the following argument.

An R-set is any set which contains itself, i.e. any set A such that A ∈ A. Let M be the set of sets which are not R-sets. Is M an R-set? Well, if M is an R-set then M ∈ M, by definition of R-set – but all elements of M are not R-sets, so M cannot be an R-set. But then if M is not an R-set, we must have M ∈ M (by definition of M), which means M is an R-set.

What went wrong? The problem is with the definition of M. More specifically, the problem lies in the implicit assumption that we can define a set merely by specifying some property of its elements. To avoid paradoxes, we must approach the definition of sets more formally.

Given the difficulty in finding a solid foundation for mathematics, people began to think more deeply about the meaning of mathematics and mathematical proof.

2 What does a proof mean?

Until the nineteenth century, mathematics had held a unique place in philosophy. With a few exceptions, philosophers were willing to accept that mathematics had an eternal and universal truth. The origins of this idea go back to Socrates and Plato. Later, empiricist philosophers held that all knowledge came from observation and experience, but even so, many accepted mathematics as somehow fundamentally true. Proofs were considered to be explanations of why something was true.

The “crisis in the foundations” forced a more careful examination of the nature of mathematical truth. If the simple concept of “set” could turn out to be so problematic, how could we ever be sure we had correctly identified an eternal truth? Is there even such a thing? How can we make sure our proofs will only prove “true” statements?

To answer these questions, three general philosophies of mathematics developed around the turn of the century.

Platonism. Platonism holds that mathematics is in fact an eternal truth, which is discovered, rather than invented. The difficulty with finding foundations is an indicator of human fallibility rather than anything to do with mathematics.

Formalism. Associated with Hilbert (1862-1943), formalism says that mathematics is just a formal game played with symbols on paper. It has no deeper meaning. The essence of foundations is then to develop rules for this game which have the properties you desire, for instance, not everything should be provable.

Intuitionism Founded by Brouwer (1881-1966), intuitionism holds that mathematical objects do exist, but only in the human mind. Hence, only mentally constructible objects can exist. This idea has developed into constructivism, which says only formally constructible objects exist.

As an illustration of the different approaches, consider the Continuum Hypothesis. Cantor’s diagonalization argument which shows that the natural numbers cannot be put into a 1-1 correspondence with the real numbers in the interval [0, 1] is a mathematical classic.

An outline of the argument is as follows. Consider the reals in [0, 1] expressed as binary expansions, i.e. each real is represented by an infinite string of zeros and ones like .010010110101100 . . .. Suppose the reals can be put into 1-1 correspondence with the natural numbers, so that we have a table like

\begin{matrix}0 & .01001011101001001 … \\ 1 & .10011010100111010 … \\ 2 & .11111100000000000 … \\ ⋮ & ⋮ \end{matrix}

and so on. Now consider the number n defined by “the ith bit of the expansion of n is (1- the ith bit of the expansion associated with i in the list)”. Then n cannot be in the list, since for each i, it differs from the number associated with i at the ith digit. Therefore, the proposed correspondence is incomplete. ^{1}

This shows that the size of the set of real numbers is larger than the size of the set of the natural numbers . A similar argument can be used to show that the set of subsets of natural numbers is larger than the set of natural numbers – simply consider the string “.0101110100111… ” to describe a set of natural numbers by putting i in the set if the ith bit of the expansion is 1. Call the cardinality (size) of the set of natural numbers ℵ_{0}, and the cardinality of the continuum c. The question is then “is there any cardinality between c and ℵ_{0}?” Another way of stating this is, “is c = ℵ_{1}?”

A Platonist would say that in the real universe of mathematical objects, this question has a single answer, either yes or no. This leaves the question, “how do we determine what the answer is?” It turns out that this question is independent of the current most popular formalization of set theory (called the Zermelo-Fränkel axioms, or ZF). This means that if ZF is consistent, then we can assume either c = ℵ_{1} or c ≠ ℵ_{1} without introducing an inconsistency.

1Actually, this argument is incomplete since there are two representations for some numbers, e.g.

.0111111111 … = .10000000. Fixing this is an exercise for the reader.

Given this, a formalist would then say, “That’s okay, then – add whichever axiom you want and go ahead.” An intuitionist would say “what are these ’real numbers’ you’re going on about? How do I construct them? And what is this ’set of real numbers’? How do I construct it?” For an intuitionist, an infinite string of digits only exists if it is mentally constructible. For a constructivist, this essentially means that the infinite string has to be computable. Furthermore, the set of real numbers (or even the set of computable strings of digits) only exists if it, too, can be mentally constructed or computed. Without these constructions, the question becomes meaningless.

The connection between an intuitionist’s mental constructions and a computer program is a compelling one which has driven a great deal of research in computer science. The idea is that a proof is really a program in disguise – if a theorem asserts that something exists, its proof must provide a method for calculating that something. Furthermore, the statement of the theorem (the proposition proved) serves as a description of the result. The slogans here are “propositions as types” and “proofs as programs”.

The real world

There is yet another meaning of proof which is rarely discussed. This is “proof as genre”. Mathematical proofs in textbooks are rarely completely formal (logic texts are sometimes an exception). Few books even bother to specify what kind of foundation they assume. Proofs in mathematical texts are really more a literary style than anything based on a formal system.

3 Formal proofs

Today we will look at a very small formal proof system. Next time, I will try to convince you that there is really a sensible connection between proofs in this system and things you might recognize as programs. For now, though, the goal is to introduce the notation and main ideas behind a formal proof system.

The formulas which appear in proofs are either variables (P, Q, R …) or given by the rule that if A and B are formulas, then A->B is a formula. The formula A->B is read “A arrow B” or “A implies B” – the symbol -> is an ASCII approximation to an arrow. By convention, we parse

A->B->C as A->(B ->C).

Now we will describe some rules for building proofs. Let G be a (possibly empty) collection of formulas. The first rule is sometimes called axiom:

                                    \overline{G, A ⊢ A}

We consider the whole collection of formulas to the left of the turnstile ( ⊢ ) to be our assumptions; this rule says that if our assumptions include A, then we can conclude A.

In general, the notation G ⊢ A is called a sequent, and represents the judgement that, if we assume the formulas in G, we have a proof of A. We consider that the order in which the formulas in G appear is irrelevant. We often omit the line over the sequent in the axiom rule; the fact that there is nothing above this line signifies that this rule does not depend on having proofs of any other sequents.

The second rule may be called ->introduction:

                                    \frac{G, A ⊢ B}{G ⊢ A->B}

The sequent above the line describes the hypothesis that we have a proof of B given the assumptions G ∪ { A }. By applying the rule ->introduction to this proof, we produce a proof

of A->B.

Finally, we have the rule ->elimination, also called modus ponens:

                                \frac{G1 ⊢ A->B   G2 ⊢ A}{G1 ∪ G2 ⊢ B}

This says that we may “glue together” a proof of A->B and a proof of A to get a proof of B (keeping all the assumptions used in these proofs).

The idea of having an introduction and elimination rule for each logical connective (here, the only one is ->) is very common.

Here are some examples of proofs in this system:

                                      \begin{matrix}P ⊢ P \\ ⊢ P->P \end{matrix}

Since there are no formulas to the left of the turnstile, this gives us a proof of P->P from no assumptions, which means that P->P is a theorem of the system. Proofs with no assumptions are sometimes called closed. Here is another proof:

                                    \begin{matrix}P, Q ⊢ P \\ P ⊢ Q->P \end{matrix}

                                  ⊢ P->( Q->P )

These two proofs have only used the axiom rule and the ->introduction rule. Here is a proof which uses ->elimination:

                                 \begin{matrix}P ⊢ P \\ ⊢ P->P \end{matrix}     P ⊢ P

                                      P ⊢ P ⊢ P->P

Now, this proof is particularly stupid, since we have already seen a simpler proof of the same formula. In fact, this proof contains the simple proof. We have a ->introduction rule which introduces the formula P->P followed immediately by a ->elimination rule. We should really be able to “cancel out” these rules and simplify the proof to

                                      \begin{matrix}P ⊢ P \\ ⊢ P->P \end{matrix}

This is more complicated than it seems from this example. We cannot just cut off the last two rules and the right branch, because the assumption P in the next to last sequent came from the right branch. Another example which shows this more clearly is the following:

                              A->A,B ⊢ B
                              A->A ⊢ B->B
                            ⊢ (A->A)->(B->B)

                                               \begin{matrix}A ⊢ A \\ ⊢ A->A \end{matrix}

                                      ⊢ B->B

This proof introduces the formula (A->A)->(B->B) only to eliminate it again immediately, but cutting off the two rules leaves us with a proof of the sequent A->A ⊢ B->B instead of ⊢ B->B. Somehow we need to get rid of the assumption (A->A), by using the fact that we were given a proof of it on the right branch.

How can we describe this process of proof simplification? These proofs are very cumbersome to manipulate – there is a lot of redundant information in this proof tree structure, and in the first proof above it is difficult to follow which P is which. Next time we will see a notation for proofs which will look suspiciously like typed λ-calculus.

Exercises and other helps

For some of you, all of this may have been review. If you’ve never seen proof rules like this before, it will be well worth your time to make sure you understand how to read and use these rules, since we will be using this format throughout the course. You can view the proofs-as-programs correspondence as either explaining functional programming (i.e. λ-calculus) through proofs, or explaining proofs through functional programs. It will help a lot if you already have at least some grasp of one or the other, but a knowledge of Scheme, Lisp, or ML will probably be enough on the functional programming side. I’ll present the essentials of λ-calculus in class next time, but a more formal introduction can be found in chapter two of Gunter’s book [4].

If you find yourself unsure about mathematical proofs in general – how to find proofs, how to write them, how to understand proofs in the literature – I highly recommend George Exner’s book [6]. This book covers what a mathematics undergraduate should know about proofs, but if you took a more applied undergraduate course you might not have been exposed to this sort of thing.

Exercise: Prove (P->Q->R)->(P->Q)->(P->R), using the proof rules. Remember that this formula is really (P->(Q->R))->((P->Q)->(P->R)). Hint: it is easiest to find proofs by starting with the goal and working backwards.

Exercise: Find two different proofs of (P->Q)->P->Q.

Exercise: Find two different proofs of P->(P->P).

Exercise: (due to P. Odifreddi) Meditate on the three kinds of implication expressed in the rule:

                                    \frac{G, A ⊢ B}{G ⊢ A->B}

References

[1] Philip J. Davis and Reuben Hersh. The Mathematical Experience. 1981.

[2] Paul Benacerraf and Hilary Putnam, eds. Philosophy of Mathematics: selected readings. Second edition 1983.

[3] http://www-groups.dcs.st-and.ac.uk/~history/index.html. The History of Mathemat-

ics web site.

[4] Carl A. Gunter. Semantics of Programming Languages: Structures and Techniques. MIT press, 1992.

[5] Haskell B. Curry. Foundations of Mathematical Logic. Dover publications, 1977.

[6] George R. Exner. An Accompaniment to Higher Mathematics. Springer Undergraduate Texts in Mathematics, 1996.