On the Design of Mathematical Concepts

Manfred Kerber1

Martin Pollet2,1

1School of Computer Science, The University of Birmingham, England

http://www.cs.bham.ac.uk/~mmk
2Fachbereich Informatik, Universität des Saarlandes, Saarbrücken, Germany

http://www.ags.uni-sb.de/~pollet

It is one of the deep mathematical insights that foundational systems like first-order logic or set theory can be used to construct large parts of existing mathematics and formal reasoning. Unfortunately this insight has been used in the field of automated theorem proving as an argument to disregard the need for a diverse variety of representations. While design issues play a major rôle in the formation of mathematical concepts, the theorem proving community has largely neglected them. We argue that this leads not only to problems at the human computer interaction end, but that it causes severe problems at the core of the systems, namely at their representation and reasoning capabilities. In order to improve applicability, theorem proving systems need to take care about the representations used by mathematicians.

Donald Norman gives a fascinating introduction into "The Design of Everyday Things." His insights are of a very general nature and we argue that the principles for good design hold in mathematics as well. The design of concepts in mathematics takes a lot of the burden on getting things right from the human user and puts it into an appropriate representation. The different representations are used to keep information together, hide unimportant details and allow to concentrate on the important parts. Sometimes the right representation is the key step in the process of problem solving. If one were to use a foundational system directly, however, everything would have to be expressed explicitly in a uniform representation, which offers no or only little structural support.

  o   d1   ...   dn
  d1   c11   ...   c1n
 
.
.
.		  
.
.
. 		 
.
   .
      . 		 
.
.
.
  dn   cn1   ...   cnn
To exemplify this, we will take a closer look at multiplication tables. The information accessible from the table is that it is a binary operation, it is discrete and defined on a finite domain. Domain and range are directly given. The table has its own notion of well-formedness, that is, all di have to occur and have to be different, the table must be fully filled. In the design we find natural and cultural constraints. Multiplication tables are designed in a way that their structure puts "information in the world" that makes it difficult to violate well-formedness. An under-specification would leave a hole in the structure, it is impossible to enter more than one entry per field. Furthermore, although the order of the di in the columns and rows could in principle be different, cultural conventions prevent that. This in turn makes particular reasoning methods possible which are connected to the representation. For instance, the commutativity of o is checked by verifying that the table is symmetric with respect to the diagonal. For more details, see the full technical report of this contribution at

ftp://ftp.cs.bham.ac.uk/pub/authors/M.Kerber/TR/CSRP-02-06.pdf or ftp://ftp.cs.bham.ac.uk/pub/authors/M.Kerber/TR/CSRP-02-06.ps.gz.

© 2002, Springer, Manfred Kerber, Martin Pollet.
The URL of this page is http://www.cs.bham.ac.uk/~mmk/papers/02-AAI-design.html.
Also available as pdf ps.gz bib .