
A Constructive Theory of Euclidean Geometry: The first
twentyeight theorems
D. E. Stevenson 442 R. C. Edwards Hall Department of Computer Science
Clemson University
PO Box 341906
Clemson, SC 296341906
telephone: 8036565880 fax: 8036560145
email: [email protected]
homepage: http://www.cs.clemson.edu/~steve/
December 18, 1995
Abstract
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 ChurchTuringChomsky 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 universitylevel 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 4dimensional space, making foundations even more important.