page 1  (15 pages)
2to next section

A Constructive Theory of Euclidean Geometry: The first

twenty-eight theorems

D. E. Stevenson 442 R. C. Edwards Hall Department of Computer Science Clemson University
PO Box 341906
Clemson, SC 29634-1906
telephone: 803-656-5880 fax: 803-656-0145
e-mail: [email protected]

December 18, 1995


We report on our efforts to explore geometry using constructive mathematics and intuitionistic logic. Such an approach differs greatly from from classical Greek[13] and modern geometry[23]. This change impinges on the theory of computability that uses classical logic and the Church-Turing-Chomsky foundations. We follow the constructive philosophy begun by Bishop[5]. This philosophy is explained in some detail. We hold that these ideas are more natural for computing than classical theories.

It is difficult to see how constructive theories are meant to work. We present new ideas based onconstructive proofs of Euclid's Elements. Such work sets a new foundation for geometry and, hence, for graphics and visualization.
CR Categories J.2 Computational Science and Engineering, F.4.1 Mathematical Logic, F.1.1 Models of Computation, F.3.1 Reasoning about Programs.

1 Introduction

The life which is unexamined is not worth living." Plato, Apology.

It appears to me that if one wants to make progress in mathematics, one should study the masters and not the pupils." N. H. Abel

1.1 Motivation

Graphics is a major computing application. In the engineering and physical sciences, we extend graphics to get to visualization. Virtual reality is becoming more important in scientific (including mathematical) visualization.

Graphics requires a good understanding of geometry (both synthetic and analytical), linear algebra, and vector analysis. The latter two are university-level fare, but the geometric foundations are generally high school fare. In the author's experience, the level of instruction of high school students in classical geometry is woefully inadequate. The problem is exacerbated by the modern calculus sequence which never gives the student a strong background in analytical geometry. To deal with advanced concepts in graphics, we must also pass onto projective geometry. Recently, we at Clemson have been exploring 4-dimensional space, making foundations even more important.