This is a specific question I have regarding my broader question: How would Hermann Weyl's development of the time "continuum" be handled in contemporary mathematical language?
I've corrected an obvious error in the translation. See the link for the original translation. There may still be a problem with the wording, since it seems to be introducing a proof by contradiction, but then fails to show a contradiction. At the end of this post is a copy of what I believe to be the text that was translated. There is another edition with different wording and ordering.
Time is homogeneous, i.e., a single point of time can only be given by being specified individually. There is no inherent property arising from the general nature of time which may be ascribed to any one point but not to any other; or, every property logically derivable from these two fundamental relations belongs either to all points or to none. The same holds for time-lengths and point-pairs. A property which is based on these two relations and which holds for one point-pair must hold for every point-pair $AB$ (in which $A$ is earlier than $B$). A difference arises, however, in the case of three time-points. If any two time-points $O$ and $E$ are given such that $O$ is earlier than $E$, it is possible to fix conceptually further time-points $P$ by referring them to the unit-distance $OE$. This is done by constructing logically a relation $t$ between three points such that for every two points $O$ and $E$, of which $O$ is the earlier, there is one and only one point $P$ which satisfies the relation $t$ between $O$, $E$ and $P$, i.e., symbolically, $$ OP = t \cdot OE $$ (e.g., $OP = 2 \cdot OE$ denotes the relation $OE = EP$). Numbers are merely concise symbols for such relations as $t$, defined logically from the primary relations. $P$ is the "time-point with the abscissa $t$ in the co-ordinate system (taking $OE$ as unit length)". Two different numbers $t$ and $t^{*}$ in the same co-ordinate system necessarily lead to two different points; for, otherwise, in consequence of the homogeneity of the continuum of time-lengths, the property expressed by $$ t \cdot AB = t^{*} \cdot AB, $$ since it belongs to the time-length $AB = OE$, must belong to every time-length, and hence the equations $AC = t \cdot AB$, $AC = t^{*} \cdot AB$ would both express the same relation, i.e., $t$ would be equal to $t^{*}$.
As I understand this, the definition of $$ OP = t \cdot OE $$ means $t$ can be understood as an "index" to exactly one ordered pair $\left\{OP,OE\right\}.$ But this does not prove that $t$ is unique.
To prove the uniqueness of $t$ we argue as follows: if $$t \cdot AB = t^{*} \cdot AB$$ holds for any time-length $AB,$ homogeneity requires the condition to hold for all time-lengths. It seems to me that this, in itself proves that $t=t^{*}$. At least $t$ and $t^{*}$ are equivalent in the role of indicating a time-point.
If $$P=P^{*}\text{, }t \cdot OE = OP \text{ and }t^{*} \cdot OE = OP^{*},$$ then $$t \cdot OE = t^{*} \cdot OE.$$
This is just an instance of $t \cdot AB = t^{*} \cdot AB$. So if my first conclusion is correct, then the assertion that $P=P^{*}\iff t=t^{*}$ follows. But that doesn't appear to be what was intended.
So what does the proof really mean?
