Structured Derivations: a Method for Doing High-School Mathematics Carefully

(1)

Structured Derivations:

a Method for Doing High-School Mathematics Carefully

Ralph-Johan Back

Abo Akademi University, Department of Computer Science Lemminkaisenkatu 14 A, FIN-20520 Turku, Finland

email: backrj@abo.

Joakim von Wright

Abo Akademi University, Department of Computer Science Lemminkaisenkatu 14 A, FIN-20520 Turku, Finland

email: jwright@abo.

Turku Centre for Computer Science TUCS Technical Report No 246 March 1999

ISBN 952-12-0398-6 ISSN 1239-1891

(2)

We show how solutions to typical problems of High School and rst-year University Mathematics can be written using structured derivations. Such a derivation extends the calculational proof format with subderivations that allow inferences to presented at dierent levels of detail. They also constitute a new paradigm where the whole solution process is viewed as an object that can be discussed and manipulated. By using structured derivations and a minimal amount of logical syntax, we can write solution to typical problems in not only algebra and equation solving but also in, e.g., real analysis. We argue why structured derivations give students a better grasp of problem solutions and better possibilities to reread and discuss solutions afterwards, as compared with traditional informal approaches to writing down solutions.

TUCS Research Group

Programming Methodology Research Group

(3)

1 Background

Mathematics teaching is facing many challenges today. The expanding high- technology industry needs ever more people with a solid knowledge of basic Mathematics. However, students often nd Mathematics dicult and hard to understand, and mathematically oriented elds of study are experiencing recruiting problems. Thus there is a need for new approaches that improve general motivation for Mathematics and make it easier for students to solve problems in Mathematics.

Mathematics rests on the combination of abstract concepts and formal notation. Today, nobody questions the use of symbols for numbers and arithmetic operations. The symbols allow us to express ideas concisely. The rules associated with the symbols allow us to reason eciently, combining formal reasoning (using the rules) with intuitive reasoning about the real- world concepts that the symbols represent.

One of the cornerstones of formal reasoning is mathematical proof. How- ever, proofs are often considered dicult and consequently the modern Finnish High School¹ Curriculum Guidelines [13] mention proofs only in connection with geometry. This problem has been recognised in other countries also and strong arguments have been presented in favour of more training in rigorous reasoning [10, 11]. Furthermore, logical notation is used very little, and it is not taught in a systematic way. Instead, the notion of proof is informal and not uniform. Where logic is taught, it is seen as a separate object of study, rather than a tool to be used when solving mathematical problems.

Most of the activities involved when learning Mathematics can be described as problem solving. Students learn new concepts and then apply them by solving problems (exercises). Exactly as for proofs, this problem solving is usually done informally. A solution typically involves a number of interrelated formulas or expressions, but the relationships are not made explicit. This makes it hard for students to know when a problem has been acceptably solved, and it also makes it dicult to look at solutions afterward and discuss them. Only in connection with a few specic problem areas (typically equation solving and rewriting algebraic expressions) a more uniform format for writing solutions is sometimes used.

Within the Computer Science community, a calculational paradigm for manipulating mathematical expressions has emerged. It has been attributed to W. Feijen, and it is described in detail by van Gasteren [5]. The following

1We use the term High School here for the Finnish "lukio/gymnasium", i.e., years 10-12 which follow Secondary School and which prepare students for University-level studies.

1

(4)

is an example of this, deriving a distribution property for set operators:

v 2A\(^B^[^C)

fset comprehension (intersection)^g

v 2A^v 2B[C

fset comprehension (union)^g

v 2A^(^v ²^B^_^v ²^C)

fdistributivity of logical operators^g (^v ²^A^{^}^v ²^B)^_(^v ²^A^{^}^v ²^C)

fset comprehension (intersection, union)^g

v 2(^A^\^B)^[(^A^\^C)

In this proof, the initial expression is transformed step by step. Each new version of the expression is written on a new line and between the two lines is written a symbol denoting the relationship between the expressions (equality in this case) and a justication for the validity of the step. The level of detail in the steps can be varied; in this example the last step is similar to the combination of the rst two steps.

In the calculational proof style, proof becomes a part of Mathematics, and doing a proof resembles rewriting an algebraic expression. A proof (partial or nished, coarse or detailed) is an object that can be inspected and discussed.

Dierent proof paradigms (such as proof by contradiction or proof by case analysis) also t the format of calculational proof.

The calculational proof style can be taken as a basis for courses in Logic and Discrete Mathematics which are included in most Computer Science curricula. A textbook has been written on this basis [6] and experiences of teaching in this way have been positive [7]. In this approach, logic is seen as a tool to be used in Mathematics and Computer Science, rather than as an object of study.

The calculational proof style gives proof fragments that are easy to read, but it does not scale up to writing complete solutions in a structured way.

In this paper, we show how structured derivations (an extension of the calculational proof format) can be used in High-School Mathematics, as a way of writing solutions to typical problems. We argue that this method gives a number of advantages, both over traditional informal ways of writing solutions and over more structured formats, such as calculational proofs:

It forces the student to be explicit about what strategies and rules are used, and in what order.

Solutions to problems can be inspected and discussed afterwards, and they are easy to check.

2

(5)

It is possible to rene an existing solution, making it more accurate and more detailed.

The method supports self-study and distributed cooperation.

There is computer-support for browsing solutions written in this format; thus the person looking at a solution can decide how much detail to look at.

Successful use of the method requires the basic notions of propositional logic (truth values and connectives) to be included in the basic mathematical notation. However, the amount of logical notation is small, and it is shown to be very useful in practice, so the extra eort spent on learning logic is a good investment for the student.

2 Introduction: equation solving

Consider the traditional way of solving a linear equation. Students write each new \version" of the equation on a new line, and indicate the \operation"

used to get from one version to the next (typically to the right, separated from the equation by a vertical bar):

2^x+ 3 = 5 ^j ^,3 2^x= 2 ^j ⁼2

x= 1

Having reached the last line, the student typically checks the solution, to make sure that it is not a \false solution". If the last line is of the form 0 = 0, then the student knows that the answer is that \the equation has innitely many solutions" and if the last line is of the form 0 = 1, then the student knows that the answer is that \the equation has no solutions".

Now consider the same equation, solved in the same way, but with the solution written in the calculational style:

2^x+ 3 = 5

fsubtract 3 from both sides^g 2^x= 2

fdivide both sides by 2^g

x= 1

Here the logical connection (equivalence) between the formulas is made explicit, and next to the equivalence symbolis a justication for the transformation step (typically a reference to a rule together with an instantiation of

3

(6)

some free variables of that rule). By transitivity of equivalence, this derivation shows that the original equation is equivalent to^x= 1, i.e., 2^x+ 3 = 5 is true exactly when ^x = 1 is true. The fact that ^x = 1 is such a simple expression (it gives us immediate and full information about ^x) makes us accept it as an \answer".

It is not uncommon that students are taught to use an explicit equivalence symbol to separate equations, in the same way as we have used in the calculational solution. However, we feel that the real meaning of this equivalence symbol is usually not made explicit enough. Logical equivalence is a relation and it relates equations (which denote truth values), exactly like equality and

\less-than" relate arithmetic expressions (which denote numbers). For this, students need some familiarity with propositional logic: truth values, connectives, truth tables, and algebraic manipulation of boolean expressions.²

2.1 Derivations with truth and falsity

The equivalence connective (as a relation between equations) was the rst piece of logical notation to be introduced. Next we introduce the symbols

T and ^F that stand for logical truth and falsity. Consider the following two equation-solving derivations:

2^x+ 3 = 2^x

fsubtract 3 from both sides^g 3 = 0

funequal numbers^g

F

2^x= 2(^x+ 1)^,2

fsimplify right-hand side^g 2^x= 2^x

fequality is reexive^g

T

Although these examples are trivial, they indicate an important idea: the symbols ^Tand ^F stand for universal truth and falsity, respectively. The fact that the equation 2^x+ 3 = 2^x is equivalent to ^F shows that regardless of what value ^x has, the equation is false, so it has no solutions. Similarly, we infer that any real number is a solution to the equation 2^x= 2(^x+ 1)^,2.

Equation solving now follows a uniform pattern: we manipulate the original equation using equivalence-preserving transformations, trying to reach an expression that is as simple as possible (according to some accepted cri- teria). For equations, expressions of the form ^T, ^F, and ^x = 5 are simple enough for the derivation to be considered completed.

2When these basic facts are taught, we feel it is essential that truth values are not confused with numbers. Furthermore, implication (as a connective) can be omitted at rst, in order to avoid the confusion that often arises in association with its truth table.

4

(7)

2.2 Derivations with conjunction and disjunction

Our aim is to use derivations as a uniform way of writing solutions. Logical connectives give us the tool we need to keep together a derivation in situations where one has traditionally split the solution into seemingly disconnected parts.

Consider solving the equation ^x(^x^,2) = 3(^x^,2):

x(^x^,2) = 3(^x^,2)

fsubtract 3(^x^,2) from both sides^g

x(^x^,2)^,3(^x^,2) = 0

fdistributivity^g (^x^,3)(^x^,2) = 0

fzero-product rule: ^ab= 0 ^a= 0^_^b= 0^g

x,3 = 0^_^x^,2 = 0

fadd 3 to both sides in left disjunct^g

x= 3^_^x^,2 = 0

fadd 2 to both sides in right disjunct^g

x= 3^_^x= 2

The original equation is found to be equivalent to the logical expression

x = 3 ^_ ^x = 2. This can now be interpreted to say that \the equation has two solutions". If the equation solving eort is divided up into the two separate equations ^x^,3 = 0 and ^x^,2 = 0 (which is the common way of proceeding, at least if the equations involved are nontrivial), then students are often confused about the connection between the two separate solutions

x = 3 and ^x = 2. This problem becomes even more evident when the equations involve two or more unknowns and some of the \subequations" do not have a unique solution.³

Note that the explicit connective ^_ also makes it easy to write down rules like the zero-product rule. Of course, students have to learn to read and manipulate connectives, but the eort pays o quickly.

As a second example, consider the equation (^x^,1)(^x²+ 1) = 0:

3The use of explicit logical connectives also makes it easier to avoid the confusing notation; we denitely prefer^x= 1^_^x= 3 to^x= 21.

5

(8)

(^x^,1)(^x²+ 1) = 0

fzero-product rule: ^ab= 0 ^a= 0^_^b = 0^g

x,1 = 0^_^x² + 1 = 0

fadd 1 to both sides in left disjunct^g

x= 1^_^x²+ 1 = 0

fadd -1 to both sides in right disjunct^g

x= 1^_^x² =^,1

fsquare is never negative^g

x= 3^_^F

frules for connectives^g

x= 3

Here the connection between the two subequations is explicit, and the last step of the derivation uses simple rules for calculation with logical formulas (with a little practice, logical rules like^p^_^F^p, ^p^{^}^F^F, etc should be as self-evident as arithmetical rules like^x+0 =^xor 0^x= 0). Thus, the whole solution process is kept together as a single derivation where the problem expression is gradually transformed into a solution.

In every example in this section we have chosen a certain level of detail for the derivation. Choosing the right level of detail is part of the art of present- ing mathematics. Typically, the justications in a very detailed derivation refer to explicit rules (like the zero-product rule), while in a less detailed derivation the justications refer to more general strategies (like \solve the equation"). In the case when a less detailed step is used, it should always be possible to think of a more detailed derivation being hidden, using the ideas of the next section.

3 Subderivations

A rule that is used in a proof step can be established by a separate derivation. Alternatively, we can establish the rule in-line with a subderivation, indented one level to the right and written immediately below a comment that justies using the result of the subderivation. We indicate the start of the subderivation by a label (this label can be a \bullet" or, if there is more than one subderivation, a number). The end is indicated by a small dot to the left of the term immediately following the end of the subderivation. If

6

(9)

the rule is so general that it may be useful in other contexts, or the proof of the rule is long, then an explicit lemma is usually a good idea. However, if the rule is specic to the derivation at hand and its proof is short, then a subderivation is preferred.

A special kind of subderivation is one that we start by focusing on a subterm. Assume that in a derivation, we have reached a term ^t[^t¹] where

t

1 occurs as a subterm. A typical step in a linear derivation can replace the subterm ^t¹ with an equivalent term ^t², leaving the rest of ^t unchanged. If the transformation from ^t¹ to ^t² involves a long sequence of steps, we have to write down the unchanged part of the original term repeatedly. To avoid this, we can start a subderivation by focusing on the subterm ^t¹. If the subderivation proves ^t¹ ^t², then it can be used to justify replacing^t¹ by ^t² in^t.⁴

3.1 Focusing on a subexpression

Consider the following typical exercise: For what values of^xis the expression

x,1

x 2

,1 dened? We take the denedness statement as our starting point and try to manipulate it until we reach an expression that characterises a set of values for ^x in a simple way:

x,1

x 2

,1 is dened

fdenedness of rational expressions^g

x 2

,1⁶= 0

fswitch to logic notation^g

:(^x²^,1 = 0)

fsolve ^x²^,1 = 0^g

x 2

,1 = 0

ffactorisation rule^g (^x+ 1)(^x^,1) = 0

frule for zero product^g

x=^,1^_^x= 1

:(^x=^,1^_^x= 1)

4This argument can be formalised as an^inference^ruleof the form

`t

1 t

2

`t[^t¹]^t[^t²]

7

(10)

fde Morgan rules^g

:x=^,1^{^}^:x= 1

fchange notation^g

x6=^,1^{^}^x⁶= 1 Thus, the expression ^x^,1

x 2

,1 is dened for all values of ^x except ^,1 and 1. In this derivation, focusing on the subterm ^x² ^,1 = 0 allowed us to do equation solving in a subderivation. Note that by using logical connectives and the de Morgan rules the role of the two \solutions" -1 and 1 is made explicit. In mathematical tradition, a graph with intervals is often used to justify the nal solution to problems involving subsets of the real line. Such a graph can illustrate a situation and help nding a proof strategy, and it can be used to check that a solution is feasible. However, by using a derivation we do not need to depend too heavily on such graphs.

A subderivation is a level of detail that can be suppressed if we want to present the solution in a less detailed form. The result of suppressing the subderivation is the following:

x,1

x 2

,1 is dened

fdenedness of rational expressions^g

x 2

,1⁶= 0

fswitch to logic notation^g

:(^x²^,1 = 0)

fsolve ^x² ^,1 = 0^g

:(^x=^,1^_^x= 1)

fde Morgan rules^g

:x=^,1^{^}^:x= 1

fchange notation^g

x6=^,1^{^}^x⁶= 1

In fact, presentation software has been developed that allows this kind of browsing of derivations (see Section 6).

3.2 Focusing and local assumptions

In the special case when we focus on either operand of a conjunction or disjunction, or on the consequent of an implication, the subderivation can make

8

(11)

use of the context that the subterm occurs in. Thus, the subderivation may have additional local assumptions compared with the enclosing derivation.

The following rules show examples of how assumptions may be added in a proof step, when focusing on a subterm of the special form mentioned above.

1. When focusing on either conjunct of a conjunction, the other conjunct may be added as a local assumption.

2. When focusing on either disjunct of a disjunction, the negation of the other disjunct may be added as a local assumption.

3. When focusing on the consequent of an implication, the antecedent may be added as a local assumption.⁵

When a subderivation involves focusing that adds assumptions, we start the subderivation with a line that states the added assumptions inside square brackets.⁶

As an example, we solve an equation involving two unknowns.

jx,1^j+^j2^x^,^yj= 0

fproperty of absolute values^g

x,1 = 0^{^}2^x^,^y= 0

fadd 1 to both sides of left equation^g

x= 1^{^}2^x^,^y= 0

fsimplify right conjunct^g

[^x= 1]

2^x^,^y= 0

fsubstitute using assumption^g 2^,^y= 0

fsolve^g

y= 2

x= 1^{^}^y= 2

5In an implication^t⁾^t⁰, we refer to^tas the^antecedentand to^t⁰ as the^consequent.

6These rules can be formally explained as inference rules, using^sequents. For example, the rst rule can be written as follows:

^;^t^`^t¹^t² ^`^t^{^}^t¹ ^t^{^}^t²

where^tis the conjunct that becomes a local assumption and is the (possibly empty) set of assumptions that are inherited from the outer derivation to the subderivation. Applying such rules amounts to^contextual ^rewriting and the method of focusing described here lies at the heart of the^window^inferencereasoning paradigm [12, 9].

9

(12)

The solution, here written with logical conjunction (^x= 1^{^}^y= 2) could also be written as

(

x= 1

y= 2

This notation has an implicit conjunction; we nd it useful to be more explicit about the connection between the two parts of the solution: ^x= 1 and^y= 2.⁷

4 Further examples

We shall now illustrate how derivations can be written in typical examples in High-School Mathematics, other than pure equation solving and rewriting of algebraic expressions.

4.1 An induction proof

A simple induction proof illustrates how multiple subderivations arise. The induction requires one subderivation for the base case and one for the step case. As our example, we prove the formula

1 + 2 ++ⁿ = ⁿ(ⁿ+ 1) 2 The derivation is as follows:⁸

7This is important, since a similar notation is sometimes used to show the two solutions of a second-degree equation, e.g.,

x

1= 1

x

2= 2

but in this case, the implicit connective involved is disjunction rather than conjunction.

8In this derivation we use ^explicit substitution notation to indicate what exactly has to be proved. In this notation,^t[^x :=^t⁰] means that ^t is to be substituted for all (free) occurrences of^xin ^t.

10

(13)

1 + 2 ++ⁿ

= ^finduction^g

(^base) (1 + 2 ++ⁿ)[ⁿ := 0]

= ^fempty sum is 0^g

= 0^farithmetic^g 0(0 + 1)

= ^fexpressed using substitution2 ^g

n(ⁿ+ 1)

2 [ⁿ:= 0]

(^step) [1 + 2 ++ⁿ = ⁿ(ⁿ+ 1)

2 ]

(1 + 2 ++ⁿ)[ⁿ :=ⁿ+ 1]

= ^fcarrying out substitution^g 1 + 2 ++ⁿ+ⁿ+ 1

= ^finduction assumption^g

n(ⁿ+ 1)

2 +ⁿ+ 1

= ^frules for fractions^g

n

2+ⁿ+ 2ⁿ+ 2

= ^fsimplify the numerator2 ^g

n

2+ 3ⁿ+ 2

= ^ffactorisation2 ^g (ⁿ+ 1)(ⁿ+ 2)

= ^fexpressed using substitution2 ^g

n(ⁿ+ 1)

2 [ⁿ:=ⁿ+ 1]

n(ⁿ+ 1) 2

We give explicit names (rather than \bullets") to the two subderivations, making their roles explicit. Note how the induction assumption is given (inside square brackets) as a local assumption in the second subderivation.

If we hide the subderivations, then there remains only an indication of 11

(14)

the strategy used, but no details of its actual workings:

1 + 2 ++ⁿ

= ^finduction^g

n(ⁿ+ 1) 2

Although this would hardly be acceptable as a solution to a classroom exercise, there are other situations when the intended reader can be assumed to accept this lack of detail.

4.2 A minimisation problem

We determine how the value of^xshould be chosen in order for the expression

x 2

,x,6 to attain its smallest value. This example illustrates the use of text as part of the description that is manipulated.

x 2

,x,6 attains its smallest value

ftransform the quadratic expression^g

x 2

,x,6

= ^fcomplete the square^g

x 2

,x+ 14 ^,6^, 1

= ^farithmetic^g 4 (^x^, 1

2 )²^, 25 4

(^x^, 1

2 )²^, 25

4 attains its smallest value

fconstant term does not aect location of minimum^g (^x^, 1

2 )² attains its smallest value

fsmallest value of a square is zero^g

x,

12 = 0

fadd 12 to both sides^g

x= 12

12

(15)

Note that on the outermost level we work with logical equivalence. In the subderivation, however, we transform a real-valued expression under equality. We make a number of implicit assumptions about the extreme values of quadratic expressions; without them, we would have to make a much more elaborate derivation starting from an expression with quantiers (the expression (^8y ^y²^,^y^,6^x²^,^x^,6); for details we refer to [3]).

5 More advanced derivations

So far all our derivations have preserved equivalence relations (logical equivalence or arithmetic equality). The same method can be used for preserving any transitive relation, as shown by Grundy [9]. Typical examples of relations that we want to preserve are (forward and backward) implication, and orderings (such as and ^<) on natural numbers, integers or reals, etc.

The only important rule that this extension adds it that we have to consider monotonicity properties when focusing on subterms. For example, assume that we want to transform an expression of the form^t¹ ^,^t² under the ordering on the real numbers. We can focus on ^t¹, show ^t¹ ^t⁰¹ and con- clude^t¹^,^t² ^t⁰¹^,^t². In this case, the same relation () can be used in the subderivation; we say that the context is monotonic. However, if we focus on

t

2 then we must reverse the direction of the ordering in the subderivation, because ^t² occurs in a negative position with respect to the ordering (in this case we say that the context is antimonotonic).⁹

5.1 An exercise from real analysis

We now show how a typical problem from real analysis can be solved. We show that the function^f(^x) = 2^xis uniformly continuous. In order to express continuity we need (nested) quantiers, and so this assumes some familiarity with predicate logic.

Our derivation illustrates nested subderivations. It preserves backward implication. This is typical for goal-oriented proof; we start from the thing we want to prove and try to transform (reduce) it to ^T while preserving backward implication. ¹⁰ The justication of this method is that we if we

9The inference rules involved are the following:

`t

1 t

2

`t

1 ,tt

2 ,t

`t

1 t

2

`t,t

1 t,t

2

10Backward implication is the opposite of implication: ^t⁽^t⁰ means the same as^t⁰⁾^t.

13

(16)

have proved ^t ⁽^Tthen we can infer ^t.

f uniformly continuous

fdenition of uniform continuity^g (⁸ ^>0⁾

(⁹ ^>0^{^}(^8x^y ^x^,^y^<^{^}^x^>^y ⁾^jf(^x)^,^f(^y)^j^<)))

( ffocus on consequent, replace in monotonic context^g

[^>0]

(⁹ ^>0^{^}(^8x^y ^x^,^y^<^{^}^x^>^y⁾^jf(^x)^,^f(^y)^j^<))

( ffocus on innermost consequent, replace in monotonic context^g

[^>0^;^x^,^y ^<^;^x^>^y]

jf(^x)^,^f(^y)^j^<

fdenition of ^f^g

j2^x^,2^yj^<

fsimplify using assumptions^g

x,y<=2

( ftransitivity using assumptions^g

=2

(⁹ ^>0^{^}(^8x^y ^x^,^y^<^{^}^x^>^y⁾⁼2))

( f9-introduction rule, witness for is ⁼2^g

=2^>0^{^}(^8x^y ^x^,^y ^<^{^}^x^>^y⁾⁼2⁼2)

fsimplify using assumptions^g

T

(⁸ ^>0⁾ ^T)

fsimplify using basic rules of predicate logic^g

T

Thus the function is uniformly continuous.

The nested quantiers require separate focusing steps, so that it is clear what variables occur free in the assumption of what subderivation. ¹¹ This

11The formal handling of quantiers may seem tricky, but the rules used are essentially formalisations of well-known intuitive strategies used to handle quantiers. Here we need general monotonicity and in addition the rule of ⁹-introduction (proving existence by supplying a witness) is used. Formally, the monotonicity rules we use are of the following form:

`t

1 (t

2

`t^t

1

(t^t

2

`t

1 (t

2

`(^t⁾^t¹)⁽(^t⁾^t²) ^`(^8x^`^t^t¹¹)⁽⁽^t(²^8x^t²) while the rule of⁹-introduction is

`t[^t⁰^=x]

`(^9x^t)

14

(17)

can prove important when considering proofs of continuity vs proofs of uniform continuity. The function in the above example was very simple. How- ever, the same scheme can be used to prove uniform continuity of more complicated functions; only the innermost subderivation becomes longer.

6 Discussion

We have shown how structured derivations can be used when solving problems of the kind that are typical for High School and rst-year University Mathematics. The format allows us to proceed from problem formulation to solution as a single structured derivation, where the steps done in solving the problem are written out explicitly. This derivation can be inspected and discussed as an object in its own right. The level of formality used in the derivation can be varied according to the level of students and the diculty of the problem. The derivation can by built up top-down (starting with the steps on the outermost level), bottom-up (starting with lemmas that provide detail) or linearly from problem solution.

What is then required if students are to use this format for writing solutions? The method of structured derivations formalises and generalises methods already used in, e.g., equation solving, so it should not be seen as contradicting existing practices. Students need to learn some basic propositional logic, but since this logic is put to concrete use, motivation should not be a problem. Structured derivations involves more copying of texts than traditional unstructured formats. However, if computer tools are used, this is not necessarily a problem. When working with pen and paper, abbreviations and ellipses can be used to minimise the amount of completely mechanical copying.

The structured format can be used as a basis for electronically browsable problem solutions. A system for browsing derivations on the world-wide web has been developed by Grundy [8] and later improved [1]. This makes it possible to share and discuss solutions over a distance. The person who browses a derivation can choose to see only the outline (top level) of the derivation or to make visible (by pointing and clicking) details that are hidden in subderivations. It is also possible to build computer support for carrying out the derivations, so that the initial expression is fed into the computer, and after that the individual derivation steps are indicated by means of menus and pointing-and-clicking.

Structured derivations are based on the same principle as standard equation solving, where a new (equivalent) version of an equation is written immediately below the previous version. However, we want to stress the use of

15

(18)

the logical symbol that shows the relationship between the two equations and the justication for the step. In traditional equation solving, the relationship between equations (,⁾or⁽) is usually left implicit. This easily leads students to draw erroneous conclusions, in particular in situations when the equation in question has either no solutions or more than one solution. In cases with more than one solution, rigorous use of connectives (^{^}and ^_) also helps avoid mistakes in the nal steps of the solution. A detailed description of (a slightly less general version of) structured derivations as an inference system for formal logic can be found in [2] and numerous examples of proofs in this style from Computer Science are included in a recent book [4].

We do not claim that all mathematical problems can be solved using structured derivations. However, the collection of examples given in this paper shows that it is feasible to use them in many dierent elds of High School Mathematics including equation solving, algebra and analysis. Traditional mathematical paradigms can also be represented; to prove ^t by contradiction, we derive ^:t ⁽ ^F and to prove ^t by case analysis on ^t⁰, we derive

t 0

`t and ^:t⁰ ^`^t. The use of logical connectives requires some eort, but in our view High School students should be able to use basic logical notation.

Furthermore, many of them have manipulated boolean values and boolean expressions when doing elementary computer programming. The introduction of quantiers can be left to a later stage, when students have become familiar with the derivation format and the use of logical connectives. How- ever, teaching the explicit rules for using quantiers and showing how they are applied in the classical--proofs in calculus would probably make it easier to understand this usually rather tricky part of High School or rst year university mathematics.

References

[1] R. Back, E. Falck, and M. Sjoberg. Publishing mathematical solutions on the Web. Abo Akademi University, 1998.

[2] R.J. Back, J. Grundy, and J. von Wright. Structured calculational proof.

Formal Aspects of Computing, 9:469{483, 1997.

[3] R.J. Back and J. von Wright. Doing High School mathematics carefully.

Tech. Rpt. 140, Turku Centre for Computer Science, November 1997.

[4] R.J. Back and J. von Wright. Renement Calculus: A Systematic In- troduction. Springer-Verlag, 1998.

16

(19)

[5] A.J.M. van Gasteren. On the Shape of Mathematical Arguments. Lecture Notes in Computer Science. Springer-Verlag, Berlin, 1990.

[6] D. Gries and F. Schneider. A Logical Introduction to Discrete Mathe- matics. Springer{Verlag, 1993.

[7] D. Gries and F. Schneider. Teaching math more eectively through calculational proofs. Am. Math. Monthly, pages 691{697, October 1995.

[8] J. Grundy. A browsable format for proof presentation. Mathesis univer- salis (electronic journal: http://www.pip.com.pl/MathUniversalis), 1(2), 1996.

[9] J. Grundy. Transformational hierarchical reasoning. The Computer Journal, 39(4):291{302, May 1996.

[10] G. Hanna and H.N. Jahnke. Proof and application. Educational Studies in Mathematics, 24:421{438, 1993.

[11] C. Hoyles. The curricular shaping of students' approaches to proof. For the Learning of Mathematics, 17(1):7{16, February 1997.

[12] P. J. Robinson and J. Staples. Formalising a hierarchical structure of practical mathematical reasoning. Journal of Logic and Computation, 3(1):47{61, 1993.

[13] Utbildningsstyrelsen (Finnish Education Authority). Grunderna for gymnasiets laroplan (Principles of the High School Curriculum, in Swedish). Tryckericentralen, Helsinki, 1994.

17

(20)

Turku Centre for Computer Science Lemminkaisenkatu 14

FIN-20520 Turku Finland

http://www.tucs.abo.

University of Turku

Department of Mathematical Sciences

Abo Akademi University

Department of Computer Science

Institute for Advanced Management Systems Research

Turku School of Economics and Business Administration

Institute of Information Systems Science