Logic is the glue that binds together methods of reasoning, in all domains.
Gries and Schneider
Click on any of the following items for more information.
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.
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.
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.
A number of articles have been written and talks will be given on equational logic and our approach to teaching 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 = dwhile 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):
|- P ---> |- P[x:= E]
|- P = Q ---> |- E[x:= P] = E[x:= Q]
|- P = Q, |- Q = R ---> |- P = R
|- P, |- P == Q ---> |- Q
We explain how the four inference rules are used in proofs, using the proof of ~p == p == false. Return to table of contents
(0) ~p == p == falseFirst, lines (0)--(2) show a use of inference rule Leibniz:
(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)
(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.
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.
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.
P[z:= p] == (p /\ E[z:= true]) /\ (~p /\ E[z:= false])
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 --FactBy 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
= < Fact b == c == d >
b == c == b ? c
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:
Return to table of contentsI'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''.
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.
Return to table of contentsOn Wednesday, 6 September 1995, David Gries will hold a full-day tutorial on "Teaching Logic as a Tool" at the ZUM 95 conference in Limerick, Ireland. Copies of the text A Logical Approach to Discrete Math will be given to participants who are enrolled in the tutorial. For information on enrolling in the tutorial, email Norah Power at powern@ul.ie .
Return to table of contents