Re: [mizar] Euclid's Elements

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

Freek Wiedijk wrote:

> 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.

Interesting. But I could not imagine (I do not claim that it is
impossible) how to formalize the postulate 2. It sounds like
       'we may assume that the segment is long enough'
but what it means 'long enough'

Andrzej