Structured derivations

Short description: Format for presenting mathematical solutions and proofs

For mathematics education, Structured derivations (SD) is a logic-based format for presenting mathematical solutions and proofs created by Prof. Ralph-Johan Back and Joakim von Wright at Åbo Akademi University, Turku, Finland . The format was originally introduced as a way for presenting proofs in programming logic, but was later adapted to provide a practical approach to presenting proofs and derivations in mathematics education including exact formalisms. A structured derivation has a precise mathematical interpretation, and the syntax and the layout are precisely defined. The standardized syntax renders the format suitable for presenting and manipulating mathematics digitally.

SD is a further development of the calculational proof format introduced by Edsger W. Dijkstra and others in the early 1990s. In essence, three main extensions have been made. First, a mechanism for decomposing proofs through the use of subderivations has been added. The calculational approach is limited to writing proof fragments, and longer derivations are commonly decomposed into several separate subproofs. Using SD with subderivations, on the other hand, the presentation of a complete proof or solution is kept together, as subproofs can be presented exactly where they are needed. In addition, SD makes it possible to handle assumptions and observations in proofs. As such, the format can be seen as combining the benefits of the calculational style with the decomposition facilities of natural deduction.

Examples

The following three examples will be used to illustrate the most central features of structured derivations.

A simple equation

Solving a simple equation illustrates the basic structure of a structured derivation. The start of the solution is indicated by a bullet ([math]\displaystyle{ \bullet }[/math]) followed by the task we are to solve (in this case the equation [math]\displaystyle{ 3x+6=16-x }[/math]).

[math]\displaystyle{ \bullet }[/math]	[math]\displaystyle{ 3x+6=16-x }[/math]
[math]\displaystyle{ \Leftrightarrow }[/math]	{ Subtract 6 from both sides }
	[math]\displaystyle{ 3x+6-6=16-x-6 }[/math]
[math]\displaystyle{ \Leftrightarrow }[/math]	{ Add x to both sides }
	[math]\displaystyle{ 3x+6-6+x=16-x-6+x }[/math]
[math]\displaystyle{ \Leftrightarrow }[/math]	{ Add similar terms }
	[math]\displaystyle{ 4x=10 }[/math]
[math]\displaystyle{ \Leftrightarrow }[/math]	{ Divide both sides with 4 }
	[math]\displaystyle{ x=2.5 }[/math]
[math]\displaystyle{ \square }[/math]

Each step in the solution consists of two terms, a relation and a justification that explains why the relationship between the two terms hold. The justifications are given equal amount of space as the mathematical terms in order to indicate the importance of explanations in mathematics.

Assumptions and observations

Specifications of mathematical problems commonly contain information that can be used in the solution. When writing a proof or a solution as a structured derivation, all known information is listed in the beginning as assumptions. These assumptions can be used to create new information that will be useful for solving the problem. This information can be added as observations that build on the assumptions. The following example uses two assumptions ((a)–(b)) and two observations ([1]–[2]). The introductory part of the solution (the task, assumptions and observations) is separated from the proof part by the [math]\displaystyle{ \Vdash }[/math]-symbol, denoting logical provability.

Sea water, where the mass-volume percentage of salt is 4.0%, is vaporized in a pool until its mass has decreased by 28%. What is the concentration of salt after the vaporization?

[math]\displaystyle{ \bullet }[/math]		Calculate the concentration of salt s after the vaporization when
(a)		the original salt concentration was 4.0%
(b)		the mass of seawater left after the vaporization is 28% less than the original mass m.
[1]		{The amount of salt after the vaporization is the same as originally (a), since only water is vaporized }
		The amount of salt is [math]\displaystyle{ 0.04m }[/math]
[2]		{According to (b) the remaining water mass is 72% (100% − 28%) of the original mass }
		The remaining water mass is [math]\displaystyle{ 0.72m }[/math]
[math]\displaystyle{ \Vdash }[/math]		s
[math]\displaystyle{ = }[/math]		{ The salt concentration is the salt mass divided by the total mass }
		[math]\displaystyle{ \dfrac {0.04m}{0.72m} }[/math]
[math]\displaystyle{ = }[/math]		{ Simplify }
		[math]\displaystyle{ \dfrac{1}{18} }[/math]
[math]\displaystyle{ = }[/math]		{ Calculate and convert to percentage }
[math]\displaystyle{ \approx }[/math]		[math]\displaystyle{ 5.6\% }[/math]
[math]\displaystyle{ \square }[/math]

Subderivations

When solving a mathematical problem or constructing a proof, there is often a need to solve smaller problems in order to solve the entire problem. These subsolutions or subproofs are commonly written as fragments on the paper. SD introduces a mechanism for handling this type of subsolutions in a way that keeps these together with the remaining solution in one single chain. These subderivations are indented and the return to the original level is indicated with an ellipsis ([math]\displaystyle{ \ldots }[/math]). The following example is the same as the one above; here, however, the information given as observations above is given in subderivations instead.

[math]\displaystyle{ \bullet }[/math]	Calculate the concentration of salt s after the vaporization when
(a)	the original salt concentration was 4.0%
(b)	the mass of seawater left after the vaporization is 28% less than the original mass m.
[math]\displaystyle{ \Vdash }[/math]	s
[math]\displaystyle{ = }[/math]	{ The salt concentration is the salt mass divided by the total mass }
	[math]\displaystyle{ \dfrac{\text{salt mass}}{\text{total mass}} }[/math]
[math]\displaystyle{ = }[/math]	{ Calculate salt mass }
	[math]\displaystyle{ \bullet }[/math]          Salt mass
	[math]\displaystyle{ = }[/math]          { The amount of salt after the vaporization is the same as originally (a), since only water is vaporized }
	[math]\displaystyle{ 0.04m }[/math]
[math]\displaystyle{ \ldots }[/math]	[math]\displaystyle{ \dfrac{0.04m}{\text{total mass}} }[/math]
[math]\displaystyle{ = }[/math]	{ Calculate total mass }
	[math]\displaystyle{ \bullet }[/math]          Total mass
	[math]\displaystyle{ = }[/math]          { According to (b) the remaining water mass is 28% less than the original mass }
	[math]\displaystyle{ (100-28\%)\cdot m }[/math]
	[math]\displaystyle{ = }[/math]          { Simplify, 72% = 0.72 }
	[math]\displaystyle{ 0.72m }[/math]
[math]\displaystyle{ \ldots }[/math]	[math]\displaystyle{ \dfrac{0.04m}{0.72m} }[/math]
[math]\displaystyle{ = }[/math]	{ Simplify }
	[math]\displaystyle{ \dfrac{1}{18} }[/math]
[math]\displaystyle{ \approx }[/math]	{ Calculate and convert to percentage }
	[math]\displaystyle{ 5.6\% }[/math]
[math]\displaystyle{ \square }[/math]

Teaching experience

Starting in 2001, SD has been empirically evaluated at different education levels with students aged 15–24. The most extensive study so far was a three-year-long quasi experiment conducted at a Finnish high school, where the test group was taught the compulsory mathematics courses using SD and the control group studied according to the traditional approach. The results indicate that the students in the test group performed better in all courses and the matriculation examination, even when potentially influencing factors have been taken into account. Other studies have indicated that students learn to justify their solutions during one single course and that students appreciate the new approach to writing mathematics.

External links

• http://www.imped.fi