An introduction to teaching logic as a tool

Logic is the glue that binds together methods of reasoning, in all domains.
Gries and Schneider

The text A Logical Approach to Discrete Math

We, David Gries and Fred B. Schneider, have written a text

A Logical Approach to Discrete Math (Springer Verlag, 1993),
which attempts to change how logic and discrete math is taught. Our thesis is that logic is the glue that binds together arguments in all domains. Therefore, instead of teaching propositional and predicate calculus in one or two weeks and then forgetting about it, we make logic the focus of the course. But this requires a logic that lends itself to formal application by people. For this purpose, we use an equational logic, in which substitution of equals for equals rather than modus ponens is the main inference rule.

First, we teach logic for six weeks, spending time on the development of rigorous proofs. We discuss principles and heuristics developing proofs and work toward giving students a skill in formal manipulation. Thereafter, we use the logic in giving rigorous introductions to: set theory, mathematical induction, a theory of sequences, a theory of integers, functions and relations, combinatorics, solving recurrence relations, and modern algebra.

Our experience is that students are far more positive about notation, proof, and rigor after this course than they are after a conventional discrete math course. Many students say that they are now less apprehensive about mathematics and proof, and others say they are using their new skill in formal manipulation in other courses. Some teachers who have used our text (in primarily teaching institutions) say that the approach helps the weaker students more than the stronger ones. These experiences give us hope that adoption of our approach can lead over the years to a radical change in the field's attitude toward proof and mathematics and its ability to deal with formality.

Instructor's Manual for A Logical Approach to Discrete Math

A 300-page Instructor's Manual for A Logical Approach to Discrete Math contains four essays on our approach to teaching logic and discrete math, hints on teaching from all 20 chapters, and answers to the over-950 exercises. The Instructor's Manual is not available electronically, for security reasons. The exercises in the text can be used as homework only if students don't have the Instructor's Manual.

The Instructor's Manual can be obtained from Gries (email to gries@cs.cornell.edu). Some form of confirmation that you are a faculty member will be necessary. We ask for \$18 (\$20 for those outside the U.S. and Canada) to help defray the cost of producing and mailing the Instructor's Manual.

Panel on teaching logic as a tool (March 1995)

At the conference of the ACM Special Interest Group on Computer Science Education in March 1995 in Nashville, a panel was held on the Gries/Schneider approach to teaching logic and discrete math in a formal and manner, using an equational logic. Three faculty members from primarily teaching institutions discussed their experiences with the approach: Stan Warford of Pepperdine University, Joan Krone of Denison University, and Peter Weston of Daniel Webster College. All three had used the text A Logical Approach to Discrete Math for at least one semester.

The three panelists felt that the approach was far more effective than conventional approaches to discrete math. Students understood proof better and lost some of their fear of math. Warford pressed the point that proofs were previously the difficult and hated part of conventional discrete-math courses, while the development of proofs was readily accepted by students with the new approach.

Krone said that students were able to enjoy their other math classes better as a result of applying a homogeneous treatment to topics from a multiplicity of domains. Students were able to distinguish between theory and metatheory and to acquire an understanding of the concepts of soundness and completeness as a result of seeing several logics. Students also found it natural to write formal specifications for programs.

Weston indicated that the formal, rigorous approach helped the weaker students more than the stronger students, mainly because the approach explains everything clearly and rigorously and gives students strategies and principles for constructing proofs.

The panelists felt they could not easily go back to old approaches to teaching logic and discrete math, even though the extra time spent on logic and proof meant that fewer topics could be covered. The increased understanding of proof and mathematics with the new approach far overshadowed the reduced coverage of topics.

Articles on teaching logic as a tool

A number of articles have been written and talks will be given on equational logic and our approach to teaching logic.

• David Gries. Equational Logic as a Tool. Invited lecture, AMAST 95, 3 July 1995, Montreal, Cananda. Contact krishnan@cs.concordia.ca for information about the conference.

• David Gries. Equational logic: a great pedagogical tool for teaching a skill in logic. Invited lecture, Zum 95, 6-9 September 1995, Limerick, Ireland. Contact Michael Hinchey at Michael.Hinchey@cl.cam.ac.uk for information about the conference.

• Gries and Schneider. Equational propositional logic. IPL 53, 3 (February 1995), 145--152. This paper proves the soundness and completeness of propositional logic E by relating it to Church's logic P1.

• Gries and Schneider. Teaching math more effectively through the design of calculational proofs. Tech. Rpt. 94-1415, March 1994. Accepted for publication in the Mathematical Monthly.

• Gries and Schneider. A new approach to teaching mathematics. Tech. Rpt., Computer Science Department, Cornell University, February 1994. Accepted for publication in PRIMUS.

• Gries. Teaching calculation and discrimination: a more effective curriculum. Comm. ACM 34, 3 (March 1991), 44-55.

Introduction to equational logic

Equational propositional logic E is a product of researchers in the field of the formal development of algorithms. (Click here to see a short history.) E is sound and complete. The emphasis in proofs is on substitution of equals for equals instead of modus ponens. Equality, or equivalence, assumes an important role instead of being a bit player, as in most propositional logics.

In our notation, b = c denotes equality, for b and c of the same type, while b == c, or equivalence, is defined only for b and c of type boolean. For b and c of type boolean, b = c and b == c have the same meaning.

One reason for having two symbols for equality over the booleans is that equality = is usually viewed as being conjunctional:

```    b = c = d is an abbreviation for b = c /\ c = d
```
while b == c can be used associatively, which is of great importance for us:
```    b == c == d is equal to b == (c == d) and to (b == c) == d.
```

Below is a typical proof in equational logic. The line numbers are present only for later discussion. This example is chosen because it is simple but shows all aspects of the formal proof system (as discussed later). The theorem numbers refer to theorems of A Logical Approach to Discrete Math. Here, we use "~" for "not". Associativity and symmetry of operators are treated transparently, without mention; this results in a large reduction in the number of theorems to be presented and simplifies manipulation. Finally, note that the style is just a formalization of the style of calculation used in high school, and indeed by many scientists in their work --that is why the style is so useful. Return to table of contents

Here is a proof of ~p == p == false.

```    (0)     ~p == p == false
(1)  =     < (3.9), ~(p == q) == ~p == q, with q:= p >
(2)     ~(p == p) == false
(3)  =     < Identity of == (3.9), with q:= p >
(4)     ~true == false     --(3.8)
```

Here are the four inference rules of logic E. (P[x:= E] denotes textual substitution of expression E for variable x in expression P):

• Substitution: If P is a theorem, then so is P[x:= E].
` |- P   --->  |- P[x:= E]`
• Leibniz: If P = Q is a theorem, then so is E[x:= P] = E[x:= Q].
` |- P = Q   --->  |- E[x:= P] = E[x:= Q]`
• Transitivity: If P = Q and Q = R are theorems, then so is P = R.
` |- P = Q,  |- Q = R   --->  |- P = R`
• Equanimity: If P and P == Q are theorems, then so is Q.
` |- P, |- P == Q   --->  |- Q`

```    (0)     ~p == p == false
(1)  =     < (3.9), ~(p == q) == ~p == q, with q:= p >
(2)     ~(p == p) == false
(3)  =     < Identity of == (3.9), with q:= p >
(4)     ~true == false     --(3.8)
```
First, lines (0)--(2) show a use of inference rule Leibniz:
` (0) = (2)`
is the conclusion of Leibniz, and its premise ~(p == p) == ~p == p is given on line (1). In the same way, the equality on lines (2)--(4) are substantiated using Leibniz.

The "hint" on line (1) is supposed to give a premise of Leibniz, showing what substitution of equals for equals is being used. This premise is theorem (3.9) with the substitution p:= q, i.e.

`  (~(p == q) == ~p == q)[p:=q]`
This shows how inference rule Substitution is used within hints.

From (0) = (2) and (2) = (4), we conclude by inference rule Transitivity that (0) = (4). This shows how Transitivity is used.

Finally, note that line (4), ~true == false, is a theorem, as indicated by the hint to its right. Hence, by inference rule Equanimity, we conclude that line (0) is also a theorem. And (0) is what we wanted to prove. Return to table of contents

This proof format has several advantages.

• The use of each inference rule is determined by the proof format, so the names of the inference rules need not be mentioned. This reduces the amount of reading and writing in a proof.
• The proof is completely rigorous, but without complexity overwhelming. Further, the proof is simple enough for students to comprehend. In fact, it formalizes the style of calculation taught in high school.
• In general, there is little copying of formulas from one line to another --one of the disadvantages of Hilbert-style proofs.
• With this format, useful proof principles and strategies can be taught.
• The proof can be read forward or backward.

Here are the axioms of equational propositional logic, in the order in which they are presented and taught. Note that, equivalence comes first. Note also that, after the first axiom, we take advantage of associativity of equivalence and write sequences of equivalences without parentheses.

• Associativity of ==: ((p == q) == r) == (p == (q == r))
• Symmetry of ==: p == q == q == p
• Identity of ==: true == q == q

• Definition of false: false == ~true
• Distributivity of not: ~(p == q) == ~ p == q
• Definition of /==: (p /== q) == ~ (p == q)

• Associativity of \/: (p \/ q) \/ r == p \/ (q \/ r)
• Symmetry of \/: p \/ q == q \/ p
• Idempotency of \/: p \/ p == p
• Distributivity of \/: p \/ (q == r) == p \/ q == p \/ r
• Excluded Middle: p \/ ~p

• Golden rule: p /\ q == p == q == p \/ q

• Implication: p => q == p \/ q == q
• Consequence: p <= q == q => p

• Anti-implication:: p /=> q == ~(p => q)
• Anti-consequence: p /<= q == ~(p <= q)

Precedence rules

Our precedence rules are designed to make formula manipulation easier by reducing the need for parentheses in many circumstances. There are other reasons for some of the precedences, as well. In the table below, we give the precedences from tightest to loosest binding, showing also the symbols we use for the symbols in this html document. We give also some of the arithmetic operators.
1. [x:= E] (textual substitution)
2. ~, - (negation or complement, unary minus)
3. *, /, mod, div (multiplication, division, mod, integer division)
5. =, <, >, /=, <=, >= (conventional relational operators. These are conjunctional.
6. /\, \/ (and, or)
7. =>, <=, /=>, /<= (implication, consequence, anti-implication, anti-consequence)
8. ==, /== (equivalence, inequivalence --for boolean operands only)

Useful proof principles and strategies

In teaching students about proofs and their development, it helps to be able to demonstrate principles and strategies for developing proofs. Here are several useful ones that appear in A Logical Approach. They are perhaps obvious to the mature mathematician or computer scientist. However, to students they are not. Mathematicians and computer scientists have, in general, not discussed such principles and strategies, and that is one reason students have previously had trouble developing proofs.
• Heuristic. To prove P == Q, transform P == Q to a known theorem, transform P to Q, or transform Q to P.
• Heuristic. The operators that appear in an expression and the shape of its subexpressions focus the choice of theorems to be used in manipulating it. Therefore, in developing the next step of a proof, identify applicable theorems by matching theorems with the structure of the subexpressions of the current expression.
• Heuristic of Operator Elimination. To prove a theorem about an operator, first eliminate it using its definition, then manipulate, and finally reintroduce the operator (if necessary).
• Heuristic. To prove P == Q, transform the side with the most structure (either P or Q) into the other.
• Principle. Structure proofs to minimize the number of rabbits pulled out of a hat --make each step seem obvious, based on the structure of the expression and the goal of manipulation.
• Principle. Lemmas can provide structure, bring to light interesting facts, and ultimately shorten a proof.
• Heuristic. Exploit the ability to parse theorems like Golden rule, p /\ q == p == q == p \/ q, in many different ways (using associativity and symmetry transparently).

Grounding informal proof techniques in logic

One of the objects of our rigorous approach to proof is to explain to students how informal proof methods are grounded in logic. In Chapter 4 of A text on teaching logic as a tool: A Logical Approach to Discrete Math, we explain how each informal technique has a solid foundation underneath it, in the form of a theorem or metatheorem. Here is a list of informal techniques together with the theorems on which they are based.

• Assuming the antecedent: Based on the Deduction Metatheorem.
• Case analysis: (p \/ q) /\ (p => r) /\ (q => r) => r.
• Partial evaluation (if P[z:= true] and E[z:= false] are theorems, then so is P):
`    P[z:= p]  ==  (p /\ E[z:= true]) /\ (~p /\ E[z:= false])`
• Mutual implication: (p == q) == (p => q) /\ (q => p).
• Proof by contradiction: p => false == p.
• Proof by contrapositive: p => q == ~q => ~p.

A neat solution to a word problem

Logician Raymond Smullyan has written several books (e.g. What is the Name of this Book?, Prentice Hall, 1978), in which many word problems are stated and proved. We show off the use of equational logic with one of his problems, which was brought to our attention and solved by Michael Barnett.

A group of three people, each of which is a liar (lies all the time) or is a truar (tells the truth all the time) are talking. B says that C and D are the same type (both liars or both truars). Someone then asks D, ``Are B and C the same type?'' What does D answer?

Here's our solution. Let b stand for "B" is a truar", and similarly for c and d. The statement ``C and D are the same type'' is formalized as c == d. Since B said it, we have b == (c == d). D's answer can be formalized as b ? c, where ? is either == if D answers ``yes'' or /== if D answers ``no'', and we have to determine which it is. Since D answers, we write this as d == (b ? c).

We manipulate d == b ? c under the truth of b == c == d. In the manipulation,we omit all parentheses because == is associative and == and /== are mutually associative.

```         d == b ? c --Fact
=       < Fact b == c == d >
b == c == b ? c
```
By inference rule Equanimity, the last line is a theorem. But the last line is a theorem only if ? is ==. Therefore, we conclude that D answered ``yes''. Return to table of contents

Lest the reader thinks that the answer is obvious because of our simple proof, we give Smullyan's own answer, an answer that many people might give if they did not think about formalizing and then manipulating. It is filled with confusing case analysis:

I'm afraid we can solve this problem only by analysis into cases.

Case One: B is a truar. Then C, D really are of the same type. If D is a truar, then C is also a truar, hence is of the same type as B, so D being truthful answers ``yes''. If D is a liar, then C is also a liar (since he is the same type as D), hence is of a different type than B. So D, being a liar, lies and answers ``yes''.

Case Two: B is a liar. Then C, D are of different types. If D is a truar, then C is a liar, hence he is of the same type as B. So D, being a truar, answers ``yes''. If D is a liar, then C, being of different type than D, is a truar, hence of a different type than B. Then D, being a liar, lies about B and C being of different types and answer ``yes''.

A short history of Equational Logic

Equational logic was developed over the years (beginning in the early 1980's) by researchers in the formal development of programs, who felt a need for an effective style of manipulation, of calculation. Involved were people like Roland Backhouse, Edsger W. Dijkstra, Wim H.J. Feijen, David Gries, Carel S. Scholten, and Netty van Gasteren. Wim Feijen is responsible for important details of the proof format.

The axioms are similar to those use by Dijkstra and Scholten in their monograph Predicate calculus and program semantics (Springer Verlag, 1990), but our order of presentation is slightly different.

In their monograph, Dijkstra and Scholten use the three inference rules Leibniz, Substitution, and Transitivity. However, theirs is not a logic, as logicians use the word, but a system of manipulation with definite semantic overtones. By this we mean that some of their manipulations are based on the meanings of the terms involved, and not on clearly presented syntactical rules of manipulation. The first attempt at making a real logic out of it appeared in A Logical Approach to Discrete Math. However, inference rule Equanimity is missing there, and the definition of theorem is contorted to account for it. The introduction of Equanimity and its use in the proof format is due to Gries and Schneider. It is used, for example, in the proofs of soundness and completeness, and it will appear in the second edition of A Logical Approach to Discrete Math.