[FOM] A Formal System for Euclid

[Arnon Avron]

In connection with the discussion concerning the status of
arguments in Euclid's elements, I would like to recommend
a recent paper which describes a very serious and extensive
logical investigation into this matter:

J. Avigad, E. Dean, and J. Mumma
"A Formal System for Euclid's Elements",
The Review of Symbolic Logic, Vol. 2, December 2009,
 pp. 700-768.

It presents a *formal* system which is faithful to Euclid's
reasoning, including its diagrammatic part.

Arnon


Quoting "Vaughan Pratt" <pratt at cs.stanford.edu>:


[Hide Quoted Text]


On 7/13/2010 8:46 PM, Monroe Eskew wrote:

On the other hand, one can point to certain
arguments in Euclid's Elements which are not valid as ordinary
mathematical arguments (i.e. not valid when charitably formalized into
classical first order logic).  Therefore since he singled out Euclid
he probably meant to refer to these defects rather than the lack of
explicit deduction rules.

It's hard to separate these.  Ignoring the complaints about Proposition
1, which I've never understood, and the awful but technically correct
proof of Proposition 2 (there is a *much* simpler proof), to my thinking
the problem happened at Proposition 16, "In any triangle, if one of the
sides is produced, then the exterior angle is greater than either of the
interior and opposite angles."  The relevant figure and argument can be
seen at

http://aleph0.clarku.edu/~djoyce/java/elements/bookI/propI16.html

The problem comes at the step "join FC".  Postulate 5 ruled out
hyperbolic geometry but not elliptical.  On the sphere, if the distance
from F to C is more than half the circumference the segment FC will be
the complete line FC less the segment drawn by Euclid in the diagram.
This screws up the angles in the rest of the argument.

People over the last half millennium or so have excused this on the
ground that Postulate 2, that you could extend a line segment
indefinitely, meant that it would never meet itself if you did.  Suppose
that was what Euclid in fact intended.  How does Proposition 16 follow
under that assumption?  It just doesn't make any sense.

If Euclid had had explicit and sound deduction rules, and stuck to them
like a leech, this problem would have come to light.  Had they been
unsound the unsoundness would have come to light.  Without formality one
is thrown back on common sense, which is what the argument above
depended on.  As such it is open to attack, which I'm happy to field.

Vaughan Pratt
_______________________________________________
FOM mailing list
FOM at cs.nyu.edu
http://www.cs.nyu.edu/mailman/listinfo/fom