Hi all, Later on in the development of elementary geometry, we shall be able to define the “length” of a segment. This goes by comparing the segment with a reference unitary segment. The question is “where does the unitary segment come from?”. It is not part of Tarski’s axioms. I have two proposals here:
- I believe we will have to define this “Unit” as two new slots (one for a zero, one for a one), since they cannot be derived from other slots. One may also think about a way to introduce multi dimensional coordinates here. - Thanks to those, we shall be able to derive a distance function. Retrospectively, I think the choice of ‘ dist ‘ for the congruence relation might be problematic here, since the constructed geometric distance shall really be the structure’s ‘ dist ‘ slot. It might be better to define a new slot for congruence, to avoid the conflict. An alternative would be to define the distance builder as a function of the geometry and the two unit points, which itself builds a distance operation. This would be nearer to the development of Schwabhaeuser, who uses “oe” (0- Einheit) indices everywhere (ch14 and ch15), but seems more complicated. Any thoughts? BR, _ Thierry -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/B590B30A-90AB-4377-A2FB-315035FA468B%40gmx.net.
