Teaching about Proof

David Gries and Fred B. Schneider

What is a proof? Where can one learn about proofs? Where can one gain skill in developing and presenting the proofs required in math and science courses?

Math courses don't seem to be the place. Sure, informal proofs are presented, using a mixture of English and formal notation, and students are asked to develop similar proofs. But the emphasis is not on the proofs but on the topic being taught, like calculus. Students are just expected to know about proofs and how to develop them.

What about courses on logic? After all, as Webster's Third New International Dictionary says, logic is the science that investigates the principles governing correct or reliable inferences. In fact, learning about how people reason was the impetus for the development of logic in the first place. However, the logics and formal proof styles taught in logic courses don't seem useful-no one uses them, except to study logic! Strategies for developing proofs are not taught, and substantial applications of proof techniques are rarely discussed. Students come away feeling that the study of logic is only an academic exercise. In terms of gaining a useful skill in developing proofs, they haven't found the help they were looking for.

Computer science, however, is providing new approaches to proof. Researchers in programming methodology have long felt the need to reason formally in order to manage complexity in computer programs. Over the years, an equational style of formal proof evolved. Fortuitously, this style has turned out to be applicable in many domains. Equational proofs are similar to the arithmetic and algebraic calculations done in high school; the "breakthrough" was to employ the style in logical calculations as well. Wi th experience, it was seen that many hitherto informal proofs could be developed formally-with an increase in simplicity and understanding. As Hilbert claimed in his famous speech at the Second International Congress of Mathematicians in 1900, rigor became a simplifying force.

The equational style of logic and proof is the basis for our new text, A Logical Approach to Discrete Math. The text teaches proof principles and strategies to impart a skill in developing formal proofs. It then exploits this skill in treating a number of areas of discrete math. Thus, logic becomes the unifying theme for a course that was previously viewed as just a bunch of disjoint topics. Logic is seen as the glue that binds together arguments in all domains.

Our text is helping this rather revolutionary view of logic to spread beyond Cornell, where it has been taught in the freshman/sophomore level computer-science course CS280 for three years. However, it has sparked controversy, for not everyone believes that our approach is right. Naturally, we think it is, and our experiences back us up.

Instead of being the most hated part of a discrete math course, proofs have become interesting. There are now lively discussions about developing proofs, much as one might discuss plot development in a literature class. Some students tell us that they are using their new skill in math and physics courses. Others say that they have lost their fear of math notation and that our course has taught them to think logically.

In fact, we believe our approach can be of help to many others besides computer science students. Math, physics, and engineering students could benefit from a better understanding of proof. We go even further: we believe that a course built on this approach would make a great alternative to the courses now required for gaining literacy in "quantitative" and rigorous thinking.

Comparison of the Equational and Hilbert Style of Proofs

Consider Einstein's formula , where c, the speed of light, is different from 0. Below is a formal, equational-style calculation of a formula that gives m in terms of e and c. (Note that = is used for equality over the real numbers or over the logical values true and false, while is used only for equality over logical values. Also, in our proofs we rely implicitly on associativity of several operators. An operator ; is associative if . Associativity allows us to remove the parentheses and write only . Operators + and are associative, as is equality over logical values.)

This proof consists of three steps, each showing the equality of two formulas justified by some substitution of equals for equals. For example, the penultimate formula equals the last, , because and substituting m for in yields . Because of transitivity of equality, "if a = b and b = d, then a = d", the first formula equals the last.

Figure 1 below is the same proof rendered in the style typically taught in logic courses. Each line gives a new theorem, which is justified using the rule shown to its right. The proof style makes the proof longer and harder to understand. It is also more difficult to develop such proofs. And the style obscures the structure of a proof, making it difficult to talk about principles and strategies.

Portia's Suitor's Dilemma

The following problem, a takeoff on a scene in Shakespeare's Merchant of Venice, shows how equational logic can be used to solve a problem. Portia has a suitor, who wants to marry her (that's what suitors wanted in those days). Undecided herself, she tests him with a puzzle. She places her portrait in one of two caskets. On the gold casket, she writes the inscription, "The portrait is not here." On the silver casket, she writes, "Exactly one of these inscriptions is true." Portia explains to her suitor that each inscription may be true or false. If he can determine which casket contains her portrait, she will marry him.

To solve the problem, formalize it as follows. First, introduce names to stand for the possible results:
gc: The portrait is in the gold casket.
sc: The portrait is in the silver casket.
Next, introduce names to stand for the inscriptions:
g: The portrait is not in the gold casket (the inscription on the gold casket)
s: Exactly one of g and s is true (the inscription on the silver casket)

Now, formalize relations between these names. Clearly, g is the negation of gc-if one is true, the other is false. We write this as follows, where operation not x is true if x is false, and is false if x is true.

Inscription s is true when one of s and g is true and the other is false. The simplest way to express this is However, we cannot claim that is true, but only that it is inscription s. Since s is a name for can be used interchangeably, i.e., they are equivalent:
.

F1 and F2 formalize the problem. We now determine whether we can derive either gc or sc from them. F2 has the most structure, so it is the most promising for manipulation. The formula in the first hint below is written without parentheses because equality over logical values is associative.

Hence, the portrait is in the gold casket.

David Gries joined the Department of Computer Science in 1969 and served as department chair from 1982 to 1987. His goal over the years has been to see how research ideas in his field of interest, programming methodology, can influence undergraduate education.

Fred B. Schneider (B.S. '75) joined the faculty in 1978. His research concerns concurrent programming and mission-critical software.