Re: [mizar] Euclid's Elements

[Freek Wiedijk <freek@cs.kun.nl>]

Dear Andrzej,

>There is no concept of (straight) line in Elementa, only
>arbitrary long segment.

Yup.  That's why there's "postulate 2" which reads: "To
produce a finite straight line continuously in a straight
line."  (Where Euclid says "straight line", read "straight
line segment".)

>So, while doing a construction we take the segment e.g.
>going through 2 points, it must be long enough,

No.  Because with postulate 2, you can always extend it.

I like Tarski's foundations for geometry better than
Hilbert's, if you want to formalize Euclid.  Hilbert has two
"sorts": points and (infinite) lines.  Tarski only has one:
points.  That feels much closer to Euclid, although I doubt
that that was Tarski's reason.

Tarski's axiomatizations of plane geometry is one of the most
elegant pieces of mathematics that I've ever seen.  I
recommend everyone to take a look at it.

Freek