SMS scnews item created by Andrew Mathas at Thu 14 May 2015 1349
Modified: Thu 14 May 2015 1408; Mon 18 May 2015 1528; Tue 26 May 2015 1250
Expiry: 26 May 2015
Calendar1: 26 May 2015 1600-1700
CalLoc1: Seminar Room 444, New Law Annexe
CalTitle1: Euclids Elements as an Equational Theory
Auth: firstname.lastname@example.org (assumed)
Euclids Elements as an Equational Theory
Professor Vaughan Pratt
Book I of Euclid's Elements axiomatizes the planar geometry of lines and circles in terms of their points of intersection, based on five postulates including the celebrated Parallel or Fifth Postulate. The emergence of formal logic in the 19th century motivated Pasch, Peano, Hilbert, Tarski and others to develop what Hilbert christened Foundations of Geometry, axiomatizing Euclidean geometry in a suitable formal logic. Hilbert used a second order logic of points, lines, and planes, which Tarski simplified to a first order logic of points alone with the structural elements expressed in terms of predicates of congruence and betweenness.
Noting that structures such as groups, rings, vector spaces, etc. admit a quantifier-free equational axiomatization, it is natural to ask whether lines and circles in the plane can be similarly axiomatized. We give a straightforward axiomatization of the affine part of Euclidean geometry as defined by Euclid's postulates 1, 2, and 5 suitably reinforced, based on a binary operation of geodesic extension and a family of n-ary operations of centroid of n points. We show that its models and their homomorphims form precisely the category of affine spaces over the rationals, in apparent contradiction to the upward Loewenheim-Skolem theorem.
We then extend the language with four partial ternary operations giving respectively the circumcenter of a triangle and three ways of specifying one end of a chord of a circle. Ordinarily partial operations are handled with universal Horn or conditional equations; instead we introduce a binary functional whose effect is to paste functions together at their domain of agreement, allowing the axiomatization to consist of a set of equations as for total operations. We show using several constructions that this language forms a complete basis for the constructions of Book I.
Professor Pratt was
a resident of International House in 1968 and 1969 and is an alumnus of the University.
As a student, he took double honours in pure mathematics and physics and a master's
degree in computer science. After graduation, Prof. Pratt went on to manage the
Stanford University Network (SUN) workstation project, and helped found Sun Microsystems
in 1982. He is listed in the University of Sydney’s Hall of Fame and is currently an
Emeritus Professor at Stanford University. He maintains active research interests in
concurrency theory, algebraic logic, autonomous driving, and global environmental
This seminar is being run by the Faculty. Please come if you are able to.