Assume I want to define length of plane curves axiomatically. It seems to be reasonable to assume that

- The length of a unit segment is 1;
- Congruent curves have equal lengths;
- Length is additive with respect to concatenation.

However this is not enuf to define length completely: many different length-like functionals satisfy these properties.

What would be a complete set of axioms?

**Motivation.** I noticed that many (if not all) proofs of the Crofton formula cheat by assuming implicitly that there is a unique length functional that satisfies the above property, which is wrong. The problem is easy to fix, but the proof I see relies on the constructive definition of length; therefore this extra argument has to be repeated in each variation of the Crofton formula, which is not nice.

**P.S.** It seems that the following set of axioms solves the problem (thanks to Taras Banakh):

- The length of any curve is non-negative and invariant with respect to reparametrizations.
- The length of a unit segment is 1;
- Congruent curves have equal lengths;
- Length is additive with respect to concatenation;
- Length is lower semi-continuous with respect to pointwise convergence.

15more comments