The reason the congruence was put in the dist slot is so that if the space happens to already have a proper metric, it will agree with the geometry by definition. In this case, I think the most practically useful approach is to just start saying "dist is a metric" at some point in the development. You can say "but wait we've lost generality" and that's true, but the point of "the construction" is to show that once you have all of Tarski's axioms the space of possible distances is isomorphic to RR, so it's not actually a loss to say that it is RR.
But somehow this is less than satisfying, since this is basically bringing in a whole bunch more axioms unrelated to Tarski's, which are conservative but we haven't shown it, so we've cheated in a sense. Where is the space for a proof? What can be done is to have a structure builder that takes a "pure-Tarski" geometric space and a unit segment in it, and produces a real geometric space on the same set of points. Now you can prove that the constructed real geometry is isomorphic to the original geometry, and the unit segment has length 1 in the real geometry. On Thu, May 23, 2019 at 1:44 AM Thierry Arnoux <[email protected]> wrote: > 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 > . > -- 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/CAFXXJStXHMGGtx88qOFdAi%3D%2Bs0vBkjKDb4b8_5K7tcFPCjL_Vg%40mail.gmail.com.
