This copy is not complete yet (it needs more HTML-formatting). In the moment, it is to give just an idea of what the original paper says. Before this copy is finished, visit the original site - http://www.cs.ualberta.ca/~hoover/dimacs-teaching-logic/paper.html - The Editor, 30.10.96
H. James Hoover and Piotr Rudnicki
Department of Computing Science
University of Alberta
Edmonton, Alberta, Canada T6J 2H1
[hoover,piotr]@cs.ualberta.ca
http://www.cs.ualberta.ca/[,]
June 25, 1996
We would like to share our experience of using a proof-checker in teaching introductory logic to first year science students who plan to enroll into computing science. For several years, we have been teaching an introduction to predicate logic as a part of a course which also covers: (a) elementary material of discrete mathematics (sets, relations, functions, and induction), and (b) reasoning about iterative programming constructs using variants and invariants. The presentation of the material from these three areas is spread over the thirteen week course.
The logic component of the course stresses the practical skills of deductive reasoning in predicate calculus. We use the MIZAR-MSE proof-checker to check students' assignments---typically about 50 small proofs for the course. The syntax of the MIZAR-MSE input language is a notation of natural deduction derived from the style of Gentzen, Jaskowski and Fitch. We have chosen a logical system which is an extension of a natural deduction system for the following two reasons:
Our principle reason for teaching logic is to give students the tools for
developing and communicating precise reasoning.
Put more bluntly, we want to rectify the appalling inability to write clear
and cogent proofs that is exhibited by undergraduates, graduate students, and
even academics.
Our goal is to provide the students with a toolkit for structuring and recording proofs that will serve them for their entire career. We want them to understand the basic principles of logical inference, and to learn a syntax that can be adapted to real situations beyond an introductory logic course. We are largely uninterested in tricks and clever techniques with limited applicability. The overall stress is on structuring proofs and showing how the conventional informal proofs are rooted in the basic inference rules of natural deduction. These include: proving an implication by assuming the antecedent and proving the consequent, case analysis, proofs by contradiction, mutual implication, contrapositive, proving a universally quantified formula, using an existential assumption. To quote from Gries [2], p. 7: ``Suddenly, the kinds of informal proofs that students have seen earlier in their education begin to make sense.''
We believe that logic at this level is like arithmetic. You learn it by doing many drills --- the way one uses an implication must be as automatic as doing addition. The logic must be so automatic that you can focus on the problem at hand. The use of a mechanized proof checker is crucial in achieving this goal. We use a proof checker with oversimplified input language such that the drills focus on the mechanics of logical structuring of reasonings. The very important skill of folding and unfolding definitions is limited to simple notions like set operations and properties of binary relations. We feel that we cannot do much more in the given time frame of the course.
This paper is organized as follows: We begin in Section 2 by describing how we use MIZAR-MSE in teaching elementary logic. This is somewhat independent of the formalism used in a proof checker. Some observations collected over the years of using MIZAR-MSE in teaching are in Section 3. We close in Section 4 with some comments on natural deduction and equational reasoning as styles of logic. Appendix A is a brief introduction to the MIZAR-MSE language and characterizes its proof checker. Appendicies B and C provide examples of MIZAR-MSE proofs.
As the first assignment, the students are given a warm-up exercise whose main purpose is to introduce them to the notation. We use variants of the following problems:
The students treat the proof-checker as an adversary which has to be convinced about correctness of their solutions. At this point, the students usually have a poor feel for the checker capabilities.
The students practice with the elementary introduction and elimination rules of natural deduction for propositional calculus with equality. The assignment consists of filling in missing pieces in reasonings and the students practice with: (a) finding the inference rule given premises and a conclusion, (b) finding premises given a conclusion and a rule, or (c) finding the conclusion given premises and a rule. The final part of the assignment consists in writing small proofs using only basic rules of inference. Even the better students require some assistance, especially when they have to prove a disjunctive formula or to reason by cases. We ask the students to write detailed inferences for the examples used in the previous assignment.
Since the MIZAR-MSE checker does not require (actually does not permit) the specification of rules of inference, the students put the names of the applied rules in a comment, see Figure 1 for an example.
Figure 1: A proof annotated by rule names.
The permitted forms of structuring proofs are slightly elaborated versions of the negation, implication, and universal quantifier introduction rules. The choice of the class of acceptable inferences and the class of permitted proof structures has been driven by an attempt to balance the formalism of natural deduction and the practice of recording everyday proofs. We claim that the practical knowledge of proof structures of natural deduction is essential for understanding proofs that the students are likely to encounter in their future life.
The suggested way of developing MIZAR-MSE texts forms an iterative process of stepwise refinement. The first step consists of designing the structure of the top level proof. Then, one tries to discover intermediate steps leading from the assumptions to the conclusion. The refinement continues by deciding which intermediate steps require a proof on their own and which can be justified by simple references to premises. One can work with unfinished inferences which are marked by the proof-checker as not accepted but can be used for reference. Teaching the discipline of stepwise refinement when constructing proofs is a challenge: just like in introductory programming, students exhibit a tendency to jump right into the details without a clear view of the entire task.
An example of developing a MIZAR-MSE text in an iterative process of stepwise refinement is given in Appendix C.
The students get the initial practice in structuring proofs through solving a number of formalized word problems à la Smullyan's knights, knaves and normals puzzles. A very simple example is discussed in Appendix B.
The next assignment is to prove a number of theorems but the axioms and the theorems are given only in English. The students have to translate the axioms in such a way that the given theorems can be proved. Markers check whether the students did not cheat in translations.
The students are given an environment containing definitions of set operations in the MIZAR-MSE notation (there are no function symbols) and a set of conjectures using the traditional notation. The task is to translate the conjectures into the MIZAR-MSE notation and then to prove the ones that are provable and to produce counterexamples to the invalid ones. We find it pedagogically valuable to contrast the detailed proofs done in a demanding formalism with the compact recordings of equational reasoning about sets, which are covered at this point in the course. The final assignment concerns proving theorems about binary relations and their properties, in the style illustrated in Appendix C.
We decided to use a proof-checker for checking students' assignment after we taught the course for several years with proofs written on paper and checked by markers. Here are some observations made by the instructors using MIZAR-MSE in teaching logic for beginners (see also [8,9,10]):
[]#1:
The first course in logic need not, and probably should not, expose the student to the full world of the expert. Instead, the first course should be simple enough to be mastered. With mastery comes the confidence to study other systems in more depth.
The question of which logical system to use in a first course is much like the question of which language should be used in the first computing science course. Our feeling is that in both cases the choice of language is largely irrelevant. In logical reasoning the real work is in the making, folding and unfolding of definitions, not the mechanics of a particular system --- just as for programming the real work is in specification and algorithmic thinking not in coding. The language of an introductory course in logic or programming should let students concentrate on the problem being solved, save them from battling syntax, and let them know when they are right or wrong.
With regards to propositional logic, it is our position that the best proof system for propositional logic is truth-tables. For all practical purposes, mainly the statement of propositions for the sound structural manipulation of formulas, truth-tables are the simplest to explain and easiest (and fastest) for students to use. Using something like natural deduction for propositional reasoning is overkill that simply causes students to wonder why one is deliberately making life complex. For MIZAR-MSE , all propositional reasoning is obvious, and students need not worry about proving the obvious. We of course use basic propositions like de Morgans laws as transformations for an algebra of formula manipulations.
The situation for full predicate calculus is not so clear. There are two popular styles of logical reasoning, which for lack of better terminology we can call natural deduction and equational reasoning. Like programming languages, although these two styles are equivalent in deductive power, whether they are more or less convenient to use depends on the particular problem.
For example, consider the theorem on exchange of existential and universal quantifiers. Compare the equational version of Figure 2 (a slightly modified version of Gries and Schneider [3], page 166) with the MIZAR-MSE version of Figure 3 (which has been annotated to indicate the inference rules employed).
Figure 2: The equational version of quantifier interchange.
Figure 3: The MIZAR-MSE version of quantifier interchange.
The unique naming of variables is simply for the convenience of beginning students, and avoids also introducing scope issues into the argument. The proof works equally well if x', y' are replaced by x, y.
Which proof is more transparent? We would argue that the MIZAR-MSE proof involving existential instantiation is more ``natural'' in this case --- although students initially tend to be confused by the instantiation of witnesses.
On the other hand, equational reasoning can save many steps over the standard natural deduction argument. Figure 4 is an example where the equational reasoning approach is clearly superior (taken from [4], page 5). Contrast this with the longer MIZAR-MSE proof, Figure 5, where we do not have a term language, and a cumbersome means of handling equivalences.
Figure 4: The equational version of subset.
Figure 5: The MIZAR-MSE version of subset.
Why is the equational argument for the subset problem simpler? The lack of terms in MIZAR-MSE is easily solved, and it would be quite possible to add some shorthand to deal with equivalences (for example being able to name a proposition and have the name stand in for part of a formula.) But this would not solve the problem that in natural deduction, quantified formulas must be regularly dismantled and re-assembled. The power of the equational argument comes not so much from the equational reasoning, as from the treatment of quantifiers as operators, and the ability to fold and unfold definitions within formulas without having to dismantle and reassemble them.
Equational reasoning is a tool to be used after you know how to structure a proof. It is a textual shorthand, which like all shorthands is very useful to the expert, and also convenient for the beginner to hide details. Having both natural deduction and equational reasoning supported in the logical system lets one have the best of both worlds, and more closely captures day to day mathematical practice.
The MIZAR-MSE input language and its processor (proof-checker) have been
designed to be used in teaching introductory logic and certain elementary
mathematical theories. MIZAR-MSE serves also as an introduction to
full MIZAR ---a much richer language and system for proof-checking mathematics.
The input language of full MIZAR is a reconstruction of the language
of everyday mathematics based on a set theory and classical logic.
The language of MIZAR-MSE is restricted to ``raw'' predicate calculus
without function symbols and with simplified syntax for logical connectives
and atomic formulae.
MSE stands for Multi-Sorted with Equality.
The MIZAR-MSE software includes a language processor and a logical checker.
The checker consists of two parts: a checker of proof structures and
an inference checker. The power of the inference checker has been
limited to make it suitable for teaching elementary logic.
Figure 6 contains an example of a MIZAR-MSE text in which we prove the non-existence of Russel's barber.
Each MIZAR-MSE text is self-contained and consists of two separate parts: the environment and the text proper.
environEnvironment
...
begin
Text proper
...
The environment section contains a collection of axioms characterizing a theory and is checked only for syntactic correctness. Each axiom is stated as a formula preceded by a label for future reference. The environment may contain also declarations of global constant ( given ... ) and predeclarations of sorts for identifiers ( reserve ... ).
The text proper contains statements of formulae together with their justifications. Each statement introduces a formula, usually labeled for future reference. The justification can be either by a reference to premises ( by ... ) or a proof ( proof ... end ). There is also a special kind of statement, called distributed statement, which can justify a formula without explicitly stating the formula, see below for the now ... end reasoning.
Only simple terms are supported, syntactically consisting of an identifier of a variable or a constant. Every variable or constant has a defining occurrence, which also specifies the sort of the designated object. The following constructions introduce object identifiers:
Each object may have only one sort. All sort identifiers are predefined and denote certain unspecified, non empty and disjoint sets.
In the environment, with reserve ... for ... one can reserve identifiers to designate objects of a given, default sort. When an object with such a pre-declared identifier is introduced and its sort is not given explicitly, then the default sort for the identifier is used.
The syntax of atomic formulae is restricted to:
Two predicates are different when: (i) they have different predicate symbols, or (ii) the numbers of their arguments differ, or (iii) at least two arguments in the same position are of different sort.
We have the usual connectives (listed in decreasing priority):
not, &, or, implies, and iff, and
two quantifiers.
Implication and equivalence are treated as binary operators none of whose
arguments can be an implication or an equivalence unless they are put in
parentheses.
The universal quantifier
for bound_var-list holdshas also the restricted version
for bound_var-list stwhich means the same asholds
for bound_var-list holdsThe existential quantifier has only one general form:implies
ex bound_var-list st Formula
The simple justification has the following general form:
:
... ;
...
:
... ;
...
:
... ;
...
Formula by
,
, ... ,
The MIZAR-MSE checker transforms this inference into the conjunction:
& 
& ... & 
& not Formula
If the checker finds the conjunction to be a contradictory formula of predicate calculus then the original inference is accepted. Unfortunately but inevitably, the checker sometimes does not accept an inference that is logically correct; to get the inference accepted one has to split it into a sequence of `smaller' inferences, or possibly use a proof structure.
The key features of the checker (subject to some size limitations) are as follows:
What is an appropriate level of ``checker power'' is an essential question for the application of proof checkers in teaching. On the one hand, a checker that ``understands'' only the basic rules of inference---although very useful at the beginning---is too weak to be used for larger problems since their solutions become very long and obscure the key thread of the argument. On the other hand, using too strong a checker for teaching introductory logic does not give the students enough exercise in low level proving---and we claim that such an exercise is beneficial for the beginners. We have an impression that our checker is too strong at the initial stages of the course.
In practice, the students do not use the full power of the inference checker, they write deductions in steps smaller than the checker perceives as obvious. This may be a result of our encouraging the students to write deductions that are, first of all, obvious to them.
The syntax of simple justifications suffices for recording inferences corresponding to applications of the the following basic rules of inference:
The existential quantifier elimination rule (choice rule) begins with consider as illustrated in Figure 6. Since the sorts in MIZAR-MSE are assumed to be non empty, the following statement does not require any justification:
consider constant-list being Sort ;while it introduces a constant(s) of the given sort.
The basic inference rules which involve assumptions (suppositions) are the introduction rules for negation, implication and the universal quantifier. These rules are expressed with the help of distributed statements (called also reasonings) enclosed in the now ... end brackets which also delimit a new scope of object and label identifiers. Each distributed statement denotes a formula which is also justified by the statement. Here is how distributed statements are used to illustrate the basic rules of inference which require assumptions.
: now
assume
:
;
. . .
thus
Justification
end;
. . .
implies
by
;
: now
assume
:
;
. . .
thus contradiction Justification
end;
. . .
not
by
;
: now
let
be
;
. . .
thus
Justification
end;
. . .
for
being
holds
by
;
where 
must not contain any
free occurrences of any object identifier introduced inside the now
other than 
.
from inside now ... end .
When making a reference to 
, we make a reference to a formula
and we say that a reasoning denotes the formula.
In the above cases, the formula denoted by the reasoning labeled 
is exactly the conclusion of the inference where 
was used as a premise.
In general, a reasoning may include an arbitrary sequence of generalizations let ... , assumptions assume ... and conclusions thus ... . These syntactic units are called skeleton items and they, taken in order of their appearance, determine the formula denoted by the reasoning:
A proof in MIZAR-MSE is another form of a justification of a formula. Syntactically, a proof has the shape of a now ... end reasoning with proof replacing now . Here is the proof version of the implication introduction rule:
implies
proof
assume
:
;
. . .
thus
Justification
end;
Every proof can be replaced by a distributed statement which denotes the same formula as the formula proven by the proof. In this sense, the proof construct is superfluous in MIZAR-MSE .
When writing a proof we can use a special formula thesis that denotes the yet unproven part of the original proposition. Each skeleton item affects the meaning of thesis. Figure 8 (see also Figure 3) illustrates how the thesis changes when the skeleton items are processed.
We say that the development of a proof is driven by the meaning of thesis , as at each point in a proof, the next skeleton item must agree with the current meaning of thesis . Every proof can be finished by concluding thus thesis , which must be properly justified. Inside a proof, we can switch to an indirect proof by assume not thesis and the only skeleton item permitted later is the conclusion thus contradiction , which must be properly justified.
The user interface to MIZAR-MSE is limited to editing and then processing text files in which the deductions are recorded. The students have a chance to practice their skills of mirroring the logical structure of the proof in its textual layout. We are afraid that a more sophisticated user interface would be an obstacle rather than help for too many students.
Gries [2] uses the following problem originally given by Smullyan:
Three people are talking together. Each is either a knight (always tells the truth) or a knave (always lies). Person B says, `` C and D are of the same type (both knights or both knaves).'' A stranger walking by asks D, ``Are B and C the same type?'' What is D's answer?What B said can be formalized in MIZAR-MSE as follows:
Knight[B] iff (Knight[C] iff Knight[D])and this is also Gries' formalization (modulo some typing inconsistency). If this formalization is satisfactory then the puzzle is solved by noticing that equivalence is associative and our answer can be recorded as follows:
environ given B, C, D being ISLANDER;
Bsaid: Knight[B] iff (Knight[C] iff Knight[D]);
begin
Knight[D] iff (Knight[B] iff Knight[C]) by Bsaid;
At an early point of learning logic this formalization and the solution
may appear to be very cryptic. We found it very instructive to solve
the problem by considering all the cases, as Smullyan [7](puzzle 35)
does. However, somewhere between the first solution and the detailed,
explicit case analysis is the following solution that we found to be helpful to
many students:
environ given B, C, D being ISLANDER;
KK: for x being ISLANDER holds (Knight[x] iff not Knave[x]);
KtB: Knight[B] implies (Knight[C] iff Knight[D]);
KnB: Knave[B] implies not (Knight[C] iff Knight[D]);
begin
Knight[D] implies (Knight[B] iff Knight[C])
proof
assume 1: Knight[D];
2: Knight[B] implies Knight[C] by 1, KtB;
3: Knave[B] implies not Knight[C] by 1, KnB;
thus Knight[B] iff Knight[C] by 2, 3, KK;
end;
Knave[D] implies not (Knight[B] iff Knight[C])
proof
assume 1: Knave[D];
2: Knight[B] implies not Knight[C] by 1, KtB, KK;
3: Knave[B] implies Knight[C] by 1, KnB, KK;
thus not (Knight[B] iff Knight[C]) by 2, 3, KK;
end;
Note how the environment states the theory of Knights and Knaves (axiom KK) as well as giving the context of the specific problem. The simplicity of the Knights and Knaves solutions in any logical system really indicates that it is the modelling and translation activities that are difficult for the world of Knights and Knaves. That is, they are probably not the best vehicle for learning a logical system.
Given is the environment as in Figure 9:
Figure 9: An environment for binary relations.
Because of the limited syntax of MIZAR-MSE what we would like to write
as xRy or 
is written as Is[x, y, R] ,
although probably Is[x, R, y] would look a bit better.
There is no explicit definition of the meaning of the Is predicate;
it is given implicitly by the adopted axioms. Similarly, the other
predicates and the sorts BinRelation and Point are defined
implicitly.
The reserve construct frees us from stating the type of an object when the object is introduced.
It is worthwhile noticing that some instructors prefer to split the definitional axioms into two implications, at least at this stage of teaching logic.
With the given environment we would like to prove that if a connected relation is contained in an antisymmetric one then they are equal. This proposition can be recorded in MIZAR-MSE as follows:
for p, q st Connected[p] & Antisymmetric[q] & Includes[p,q]
holds Includes[q,p]
and an attempt at justifying our claim by simple justifications fails.
for p, q st Connected[p] & Antisymmetric[q] & Includes[p,q]
holds Includes[q,p]
by Connectedness, Antisymmetry, Inclusion;
********************************************^
** Not accepted
The checker does not see the correctness of the recorded inference:
the inference is too complicated. In such case, we have to write
a sequence of more detailed inferences instead.
The proposition is a universally quantified formula that suggests employing
a proof, as simple justifications (usually) do not suffice to prove
such formulae.
The proof structure is dictated by the shape of the proposition:
for p, q st Connected[p] & Antisymmetric[q] & Includes[p,q]
holds Includes[q,p]
proof
let p, q be BinRelation;
assume A: Connected[p] & Antisymmetric[q] & Includes[p,q];
thus Includes[q,p];
********************^
** Not accepted
end;
The skeleton of the proof is appropriate, it is the conclusion of the proof
that needs to be justified. The only way we can prove the conclusion
of the proof is by a reference to the definition of inclusion,
so let us refine our proof accordingly:
for p, q st Connected[p] & Antisymmetric[q] & Includes[p,q]
holds Includes[q,p]
proof
let p, q be BinRelation;
assume A: Connected[p] & Antisymmetric[q] & Includes[p,q];
B: for x, y st Is[x,y,q] holds Is[x,y,p];
*************************************************^
** Not accepted
thus Includes[q,p] by B, Inclusion;
end;
Since it is not clear how to justify the not accepted claim
with a simple justification, we try to write a proof for it:
for p, q st Connected[p] & Antisymmetric[q] & Includes[p,q]
holds Includes[q,p]
proof
let p, q be BinRelation;
assume A: Connected[p] & Antisymmetric[q] & Includes[p,q];
B: for x, y st Is[x,y,q] holds Is[x,y,p]
proof
let x, y be Point;
assume C: Is[x,y,q];
thus Is[x, y, p];
******************************^
** Not accepted
end;
thus Includes[q,p] by B, Inclusion;
end;
If we are not sure how to complete the direct proof of claim labeled B
in a convenient way, we switch to the indirect proof:
for p, q st Connected[p] & Antisymmetric[q] & Includes[p,q]
holds Includes[q,p]
proof
let p, q be BinRelation;
assume A: Connected[p] & Antisymmetric[q] & Includes[p,q];
B: for x, y st Is[x,y,q] holds Is[x,y,p]
proof
let x, y be Point;
assume C: Is[x,y,q];
assume D: not Is[x,y,p];
thus contradiction;
********************************^
** Not accepted
end;
thus Includes[q,p] by B, Inclusion;
end;
And with the assumptions labeled C and D we get a
contradiction in four steps, referring once to each axiom on the way.
The text of the complete proof is presented in Figure 10.
The proof from Figure 10 can be modified to look like the proof in Figure 11. The latter is only a stylistic variation of the former, and at the elementary level of learning logic it is important to recognize the same proof ideas behind different textual representations.
Figure 11: A variation of the proof.
Teaching freshman logic with MIZAR-MSE
This document was generated using the LaTeX2HTML translator Version 95 (Thu Jan 19 1995) Copyright © 1993, 1994, Nikos Drakos, Computer Based Learning Unit, University of Leeds.
The command line arguments were:
latex2html -split 0 paper.tex.
The translation was initiated by Jim Hoover on Wed Jul 17 20:33:00 MDT 1996
