Generation and presentation of formal mathematical documents
Martijn Oostdijk · TU/e Research Portal · 2001
ly) but also the mathematical content itself is defined in the language. In the beginning of the 20th century interest in formal mathematics was revived due to the discovery of some negative findings such as Russell’s paradox, Godel’s incompleteness proof, Hilbert’s problems, and Brouwer’s intuitionism. An important aspect of Brouwer’s intuitionism is that it proposes to only consider mathematical principles that are constructive, which in a radical way gets rid of many inaccuracies. After practical computers were introduced in the 1950’s, Leibniz’ dream of a universal language for stating problems, at least when we restrict ourselves to mathematics, might become a reality in the form of theorem provers. De Bruijn’s Automath [69] system is one of the first such theorem provers, based on typed λ-calculus. Note that the introduction of automatic computers radically changes the reasons why people study formal mathematics. The possibility to mechanically check the correctness of mathematical statements makes the field of formal mathematics interesting for mathematicians and computer scientists who are not in the first place interested in the logical foundations of mathematics. Formality is a relative notion. To solve a real world problem, one builds a mathematical model which is an abstraction of the real world problem. Reasoning about such a model forces one to consider the problem in abstract terms, leaving out irrelevant details which may obscure a solution. Since such a model is formulated in the mathematical domain, we can apply mathematical methods to it, invented by generations of clever mathematicians. While building such a model formalizes the problem, it is often not formal in the strict syntactical sense used in this thesis. Formalizing does not imply making a mathematical model of a real world problem, but encoding of mathematical content in a formal language L. Such a formal encoding allows manipulation of the mathematical content by computers, and is therefore a necessary condition if we want to do Computer Mathematics. The activity of formalizing informal mathematics bears some similarities to the activity of implementing software systems. in fact, it is similar to going from an informal specification of a computer program to the concrete program code. Because mathematics has been around much longer, and also because of the formal nature of mathematics, the specifications tend to be more clear than the ones in software industry. However, the 2000 years of existence of mathematics are not directed towards full formalization. The most acute problem seems to be that formalizing means making implementation choices. Concepts in informal mathematics are reduced to the primitives of the formal language L. Given a concept in informal mathematics, there are often many different ways to implement it. Such a reduction is a one-way mapping therefore something is lost when we express abstract theories in L. Ideally, mathematics is representation independent, but in practice such fundamental implementation choices do matter. From a verification point of view this is not really a problem. After all, mathematics is conducted on a high level, and only in the end when we want to verify the mathematics, is it formalized and reduced to L to be checked. The formalization is done in such a way that correctness of the formal mathematics implies validity of the informal mathematics. However, in practice the activity of informal theory development and 6 CHAPTER