Re: [mizar] Euclid's Elements

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

Dear Andrzej,

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

I always understood it as "as least as long as some given
other line".  So given AB and CD, we get an E such that AB is
an initial part of AE ("B is on AE") and AE is at least as
long as CD.  That would be my formalization.

However I don't know whether this covers the uses that Euclid
makes of it.  I think the postulate is meant to reflect that
using a ruler you can extend a finite line segment arbitrarily
far.  So if a extension of a line segment intersects some
figure, you can find this point of interstection.

Freek