Skip to main content
main-content

Über dieses Buch

There seems to be no doubt that geometry originates from such practical activ­ ities as weather observation and terrain survey. But there are different manners, methods, and ways to raise the various experiences to the level of theory so that they finally constitute a science. F. Engels said, "The objective of mathematics is the study of space forms and quantitative relations of the real world. " Dur­ ing the time of the ancient Greeks, there were two different methods dealing with geometry: one, represented by the Euclid's "Elements," purely pursued the logical relations among geometric entities, excluding completely the quantita­ tive relations, as to establish the axiom system of geometry. This method has become a model of deduction methods in mathematics. The other, represented by the relevant work of Archimedes, focused on the study of quantitative re­ lations of geometric objects as well as their measures such as the ratio of the circumference of a circle to its diameter and the area of a spherical surface and of a parabolic sector. Though these approaches vary in style, have their own features, and reflect different viewpoints in the development of geometry, both have made great contributions to the development of mathematics. The development of geometry in China was all along concerned with quanti­ tative relations.

Inhaltsverzeichnis

Frontmatter

Author’s note to the English-language edition

Abstract
Mechanical theorem proving (MTP) is a traditional topic of mathematical logic. In contrast to the usual approaches to MTP by mathematical logic, approaches using algebraic methods seem to be originated in the paper by the present writer (Wu 1978). In 1984 appeared the present book “Basic Principles of Mechanical Theorem Proving in Geometries” devoted to a systematic exposition of such algebraic methods for MTP. The book, written in Chinese and published in China, was little known beyond China. The method became widely known owing to papers by Wu (1978, 1984a) and Chou (1984) published in the anthology edited by Bledsoe and Loveland (1984). Since that time the algebraic methods of treating MTP have been developed rapidly and vigorously in various directions. For example, in 1986 there appeared several papers on MTP based on Gröbner basis method and others (e.g., Kutzler and Stifter 1986, Kapur 1986). In this note we shall give a brief review of the achievements of MTP in recent years restricted, however, to the methods as exhibited in the present book alone. Thus it may serve merely as complement and addendum to the original version of the book.
Wen-tsün Wu

1. Desarguesian geometry and the Desarguesian number system

Abstract
What we call ordinary geometry in this book is the usual Euclidean geometry.
Wen-tsün Wu

2. Orthogonal geometry, metric geometry and ordinary geometry

Abstract
In Desarguesian (plane) geometry which takes Hilbert’s axioms of incidence H I, (sharper) axiom of parallels HIV, the axiom of infinity D and Desargues’ axioms D as its basis, one can uniquely determine a Desarguesian number system N, called a geometry-associated Desarguesian number system, as has been exhibited in the previous sections. This number system is actually a skew field (of characteristic 0) and in general it does not satisfy the commutative axiom of multiplication N 13 of the complex number system. In order to let the commutative axiom of multiplication be satisfied, too, so that N becomes a number field, we must introduce other axioms in this geometry. One way, as shown in Hilbert’s “Grundlagen der Geometrie,” is to introduce the so-called Pascalian axiom. What Hilbert called the Pascalian axiom is actually a special case of the theorem commonly named after Pappus. It is also a special case of Pascal’s theorem in usual projective geometry where the conic section degenerates into two lines. To distinguish the axiom considered by Hilbert from the general Pappus’ and Pascal’s theorems, we call it the linear Pascalian axiom, stated as follows.
Wen-tsün Wu

3. Mechanization of theorem proving in geometry and Hilbert’s mechanization theorem

Abstract
Generally speaking, Euclid’s “Elements” is the origin of axiomatization of mathematics. However, from the viewpoint of rigor, it has many blemishes. This has been recognized for thousands of years. In the middle and late nineteenth century a critical movement attesting the very foundation of mathematics began. Mathematicians made a comprehensive analysis of the axioms besides the independence problem of the axiom of parallels in the “Elements.” This movement was initiated in Germany and Italy by Pasch and Peano, followed by others and epitomized later on by Hubert. He classified the axioms of Euclidean geometry into five groups (cf. Sect. 1.1) as the basis and starting point of all theorem proving so that Euclidean geometry has had a rigorous foundation ever since. However, even though there is a rigorous axiom system as the basis of all reasoning and proving, by using the Euclidean proof method for geometric theorems it is still impossible to reach an extent of rigor without flaws. This opposes all conventional understandings, as it seems that nobody has ever precisely pointed out or even recognized this fact. This section focuses on explaining this issue.
Wen-tsün Wu

4. The mechanization theorem of (ordinary) unordered geometry

Abstract
This is the principal chapter of the book. It aims to prove that if the associated number system of a certain geometry is a number field, i.e., multiplication is commutative, then the proving of theorems whose hypotheses and conclusions can be expressed as polynomial equality relations is mechanizable. This class of theorems will be called theorems of equality type. In fact, this class contains most of the important theorems in elementary geometries though it excludes theorems involving order relations and thus polynomial inequalities in the algebraic relations. However, the latter does not often occur except in high school Euclidean geometry. In modern geometries such as algebraic geometry, the associated number fields are usually the complex field and arbitrary fields of characteristic 0, so no order relation is involved. Therefore it is compatible with the current state of geometry to restrict mechanical proving to theorems that can be expressed by means of only equalities.
Wen-tsün Wu

5. Mechanization theorems of (ordinary) ordered geometries

Abstract
The geometries, such as unordered Pascalian geometry and orthogonal geometry, which were considered in Chaps. 3 and 4 do not assume any relation of order. In geometries of this kind the statement of theorems, after fixing the coordinate system, involves only some equality relations. We have proposed a mechanical method which usually is quite efficient and can be used to prove rather difficult theorems. Practice will show the extent of efficiency of our method for unordered geometries. In the book “Theory, Method and Practice of Mechanical Theorem Proving in Geometries” (under preparation), we shall explain in detail the algorithmic procedure, implementation and computer experiments of this method and give more examples. This book is restricted only to the basic principles. If a geometry assumes an order relation and the statement — especially the conclusion part — of a theorem involves such an order relation, then the situation becomes not only much more complicated but also different in essence. In this case, there are methods for mechanical proving in theory, but their efficiency is not high. It still seems difficult to prove non-trivial theorems by using these methods.
Wen-tsün Wu

6. Mechanization theorems of various geometries

Abstract
We introduced the concept of geometry from the viewpoint of axiomatization in Sect. 2.6 and the concepts of mechanical methods and mechanizability of theorem proving in geometry in Sect. 3.3. Furthermore, in Chaps. 3–5 we showed the mechanizability and presented the corresponding mechanical methods for some geometries or some classes of theorems. From the axiomatization to the mechanization, we have roughly gone through such a path as Axiomatization → Algebraization → Coordinatization → Mechanization.
Wen-tsün Wu

Backmatter

Weitere Informationen