I consider the constructive nature of Euclid's geometric reasoning in the light of E, a formal analysis of the diagrammatic proofs in the early books of the Elements. E is a proof system developed from the initial work of Manders, and the later work of Mumma, on the role of diagrams in Euclid's proofs. I present the key ideas of this work, and then describe how they are embodied in E as a formal system. After sketching the proof of E's completeness relative to modern axiomatizations, I close with a discussion of what seems to emerge as distinctive to reasoning about exact geometric constructions with inexact geometric diagrams: the introduction of points that are not the result of exact, determinate procedure, but instead are simply stipulated to satisfy general positional conditions.
I will survey the programme of quantifier-free axiomatizations of plane geometries in languages containing only operation symbols which are invariant under a certain group of geometric transformations and individual constants. The programme was set in motion in 1968 with a paper by Nancy Moler and Patrick Suppes. On the one hand it raises new questions, which are still open, regarding the need for certain operations in universal axiomatizations, and on the other hand it answers questions regarding the natural nature of certain fragments of Euclidean and hyperbolic geometry which look artificial when encountered in their traditional axiomatization in languages without operation symbols.
I discuss Kant's views on geometry against the background of some recent work on diagrammatic reasoning. I argue that Kant's conception should not be assimilated to recent diagrammatic views, because Kant's view of (Euclidean) geometrical constructions as taking place in what he calls our pure intuition of space is involved with some larger philosophical issues: in particular, with a Leibnizean view of concepts (for Kant, geometry involves the construction of what he calls pure -- a priori -- sensible concepts) and with a Newtonian view of space as the "divine sensorium" (for Kant, space is our -- human -- sensorium rather than God's). These two features of Kant's conception help to explain why geometry is both a priori and necessarily applicable to all possible objects of human perception. They also bring to light an interesting connection between his view of Euclidean constructions and the (group-theoretical) structure of what we might call "perspectival space.”
Euclidean geometry, as presented by Euclid, consists of straightedge-and-compass constructions and rigorous reasoning about the results of those constructions. A consideration of the relation of the Euclidean “constructions” to “constructive mathematics” leads to the development of a first-order theory ECG of the “Euclidean Constructive Geometry”, which can serve as an axiomatization of Euclid rather close in spirit to the Elements of Euclid. In previous work, we have shown that ECG corresponds well to Euclid’s reasoning, and that when it proves an existential theorem, then the things proved to exist can be constructed by Euclidean ruler-and-compass constructions. In this talk we take up the formal relationships between three versions of Euclid’s parallel postulate: Euclid’s own formulation in his Postulate 5, Playfair’s 1735 version, which is the one usually used in modern axiomatizations, and the version used in ECG. We completely settle the questions about which versions imply which others using only constructive logic: ECG’s version implies Euclid 5, which implies Playfair, and none of the reverse implications are provable. The three versions or the parallel axiom correspond to constructively different notions of "Euclidean field".
A number of different examples will be given of using algebra (NOT via cartesian coordinates) in proving geometric theorems. The first method uses vector analysis in a pretty standard way, but the examples might be amusing. The second method uses complex numbers based on the insight they give to 2D rotations. The third method uses symbolic polynomial calculations in 2D complex projective geometry putting a special emphasis on duality. All of the methods show that algebra can be constructive in actually finding formulas for the answers to certain kinds of problems. This often makes it possible to use computer graphics to draw accurate pictures.