[FOM] Standard Language of Euclid
joeshipman at aol.com
Sun Sep 27 15:16:23 EDT 2009
Your point is well-taken, but you are mistaken about Euclid's diagram
logic not having been formalized. A very good formal system for
Euclid's elements which respects the distinction between diagrams
serving a purely illustrative function and diagrams carrying essential
information is given in "A formal system for Euclid's Elements" by
Jeremy Avigad, Edward Dean, and John Mumma, available at
Another interesting point about the analytic answerability of questions
in geometry as that, even though the full formal theory requires
algorithms of exponential or superexponential complexity, many theorems
reduce to polynomial identities which can be checked in random
polynomial time (see J.T. Schwartz, "Fast Probabilistic Algorithms for
Verification of Polynomial Identities", Journal of the ACM Vol. 7 #4
(October 1980) pp. 701-717).
Of course we know that some decidable theories still have open
questions (for example, nobody knows whether there exists a projective
plane of order 12). Am I correct in surmising that there is no question
that can be stated in the language of elementary algebra and geometry
which is currently regarded as both open and interesting?
From: A. MANI <a_mani_sc_gs at yahoo.co.in>
You are not being very correct in using "standard language of Euclid".
In the original language of Euclid it is not possible to remove the
figures from the proof. It definitely possess a 'logic of diagrams'
It seems nobody has actually formalized it. 'School geometry' like in
the older British texts (Hall & Stevans for e.g) is in the language you
More information about the FOM