The material below explains why a change to the curriculum for math1090/2090 is being proposed.
Current course | Proposal | Equational logic | Textbook | Disadvantages
AS/SC/AK/MATH1090.03: Introduction to Sets and Logic:
Sets, functions, relations, induction, proof techniques, logic and logic
circuits, basic combinatorics and some basic graph theory.
AS/SC/MATH2090.03: Introduction to Mathematical Logic. An introduction
to propositional logic; predicate logic, with an emphasis on semantics;
elements of axiomatic number theory. This course is intended for Computer
Science students and for Mathematics students who plan to do further study
in logic.
Main problems with the above:
Piecemeal, repititive and uncoordinated. Want second year to build on and
re-use first year material. Want to be able to build on this material for
later CS courses in hardware design, software engineering, artificial intelligence
and databases. The current curriculum does not apply the material to computer
science topics. Students come away thinking that it is of academic interest
only.
The calculational logic of Gries and Scheider [GS], developed and used at Cornell, present a proof format and logic which can be re-used in a variety of discrete math domains (unlike the more limited proof format of the current math2090 curriculum). The fact that the proof system (from math1090) is re-used (in math2090) gives the student crucial practice that will encourage familiarity with using logic. Students need to see and use the basic concepts repeatedly so that they become internalized and natural. In later courses (e.g. math2320 or calculus), students will use other proof formats, and perhaps even informal English proofs. But the point in these two courses is that they master at least one method well.
Gries and Schneider write:
The GS text uses a variety of examples from Computer Science including hardware design, program specification and verification and database theory.
In a natural deduction system (such as the one currently used in math2090), proving the validity of
(q == r) --> (p \/ q == ~~p \/ r)
takes over 10 steps (you have to prove mutual implication). The GS version of the proof is in two steps - equals are substituted for equals (Leibniz's law):
Assume: q == r |
assumption |
p \/ q |
LHS |
= << by the assumption: q == r >> |
justification in brackets why LHS = MIDDLE |
p \/ r |
MIDDLE |
= << double negation: p == ~~p >> |
justification why MIDDLE = RHS |
~~p \/ q |
RHS |
The GS proof system also has all the strategies of natural deduction, so other proofs that use natural deduction strategies can also be done in the GS format (e.g. case analysis, proof by contradiction etc.). By having Leibniz as the primary inference rule (rather than modes ponens), many proofs are shortened.
Click here to see the difference between the proof of a simple theorem of set theory as it is currently presented in many textbooks and the way it would be presented in GS.
The following comment has been made by a colleague in the Maths. department:
"For recent instructors in the logic course, our biggest dissappointment is the realization that students who can do an effective formal derivation using, say 'negation elimination' (proof by contradiction) have very little ability to use such an argument in an informal setting. They simply do not transfer these formal games with correct arguments in words (say about logical ideas such as consistent sets of formulae). The students do not seem to get the right balance between 'doing derivations in the formal system' and reflecting on what these represent."
One of the reasons this happens is because students learn natural deduction but then never apply it in other domains. To use logic well, one must learn it early and practice a lot. Logicians study formal logic but don't use it in their own proofs. Programmers learn about boolean expressions but never learn a way to calculate with them (even though the basic ideas are the same as number algebra used by engineers and scientists routinely). Hehner says that logic is is a tool like a knife. People have looked at it from every angle. They have described how it works at great length. Now it's time to pick it up and use it.
Number algebra is used by engineers, economists, architects and scientists routinely. It is taught early on and always applications are emphasized. That's why people are comfortable with and transfer it's use to diverse domains. We have to get the notation, terminology and use of logic into the same shape to get it to be used widely as well.
See Boolean Formalism and Explanations (E.C.R. Hehner:, invited lecture at AMAST, Munich,1996 July) where he writes that before the rules of number algebra were developed and internalized by students, it could take many pages to go from (2x + 3 = 3x + 20) to (x = 1). This is because the algebra was not yet fully trusted. The number algebra replaced meaning with symbol manipulation: the loss of meaning is not easy to accept. The author of a proof had to constantly reassure his readers at each step. Those who were skilled in the art of informal reasoning were convinced that thinking about the objects and their meaning directly was the only way to get it right.
Today, we expect chunks of quantitative calculation to be conducted entirely in algebra without reference to objects and their meanings. We just apply the laws without having to justify it at each step with an informal account (e.g. see the proof of Weddurburn's theorem that a finite division ring is a commutative field in the above reference). We can then go further faster and more succintly and with greater certainty.
To do these kind of calculations, you have to get the notation right. The overwhelming reaction to notational issues is: it does not matter what symbols are used. Just use them an get on with it. But to apply an algebra, one must recognize the patterns and matching laws. The logician Goodstein chose to reverse 0 and 1 --- this takes a lot of getting used to and slows comprehension. Calculating in Arabic numerals is much easier than calculating with Roman numerals. The right notation is important!
The GS logic has the virtue of (a) introducing a suitable notation and calculus that can be used for logic and in other domains, and (b) allowing a succint way for doing calculations (which subsumes proof derivations, simplifying, and solving in diverse domains).
The Gries/Schneider text is A Logical Approach to Discrete Maths, Springer Verlag. Between the text and instructor's manual there are 700 worked out examples. The text works on the basis that logic is the glue that underlies reasoning in all areas of Computer Science. Hence logic is treated first, and then that logic is used in a variety of discrete domains (sets, combinatorics, recurrence relations, graph theory etc.).This text can be used for both courses and will cover more ground than the current curriculum does.
There are some disadvantages to the approach.