How can we point to a specific element of an abstract mathematical space that has no distinctive elements with respect to the space's structure?

Question

An example of such a space is a Euclidean affine space. Consider the statement "point O is the origin of the system". How could we clearly specify and convey what point O is supposed to be, given that this space is "homogeneous" or "isotropic", i.e., everything "looks" the same? The structure a point "sees" in the space it "lives" in is the same for every point, so there is no distinguishing point. This is different from, for example, the natural numbers, where 0 is axiomatically distinct from the other numbers, and the other numbers in turn are distinct from other numbers in how they relate to 0.

One possible way to reason about this is that "O" is simply a label for an element of the space, much like "1" is a label for the successor of 0, whose label, "0", represents the first element. But in the case of natural numbers, we're attaching labels to elements which possess specific properties that can be expressed unequivocally in terms of the definitions and axioms of the natural numbers. We can't do this for an affine space.

Another way to look at it could be that we're not specifiying any particular point. The statement "point O is the origin the system" should then be understood as a tacit agreement between the participants of a hypothetical conversation: "pick whatever point you like and call it O". Since all relations in geometry are relations between at least two elements of the space, not "absolute" relations, and this space is homogeneous, whatever reasoning that follows "pick whatever point you like and call it O" would unwind in the same manner for any chosen point. This has the benefit of making applications to physics sound, by mapping the chosen point, which could be any point, to a particular point in reality, such as "point O is an abstract representation of the corner of this platform, to which the robot is attached, closest to the red door". But this still hasn't addressed the issue that I can't, in a clear sense, pick a point, once again unlike "picking" the number 3, or 228, or 784248, since to pick a point, I should have someway of distinguishing it from others.

How is this issue addressed?

Answer 1

Formally, there is no confusion between the assumptions of an argument and the actual result of the argument itself. In the language of type theory, you would write

X : AffineSpace, O : X ⊢ ℐ(O)

where ℐ is a judgement parametrised on an arbitrary point O of an arbitrary affine space X, to translate something like "let O be a point; then, ℐ(O)...". By contrast, the judgement

X : AffineSpace ⊢ O : X

or equivalently

⊢ f : (X : AffineSpace) → X

means that you can construct an explicit point of any arbitrary affine space. In univalent foundations, it should be possible to prove that this type is empty by transporting f(ℝ) along the identification ℝ = ℝ (as affine spaces) induced by a translation (+1) to get f(ℝ) = f(ℝ) + 1, a contradiction: this means that you cannot construct such an f.¹

On the other hand, you can prove that every affine space is merely inhabited (in the sense of the HoTT book), that is

X : AffineSpace ⊢ O : ∥ X ∥

Intuitively, this means that there is at least one point in every affine space X, but any choice is as good as any other.

Finally, if you fix an affine space X (say X = ℝ) then it might be possible to exhibit a point of that particular X (say 0):

⊢ ℝ : AffineSpace

⊢ 0 : ℝ

or equivalently

⊢ (ℝ, 0) : (X : AffineSpace) × X

Note that now both the space and the point are results/outputs instead of being assumptions/inputs.

---

¹ In ZFC set theory, you can probably abuse the axiom of choice to choose a point in every affine space, but this is not very satisfying.