Finite Recursion Theorem Does there exists a version of the Recursion Theorem for finite totally ordered sets (instead of natural numbers)?
There are many cases where we have a finite totally ordered set and we have to define a thing recursively over that set, but how can it be formalized?. For example, if we have an ordered sequence $({x}_{i})_{i\in I}$ in a group, where $I$ is a finite totally ordered set, how can we formalize the definition of product of that family?

Any finite strictly totally ordered set has a unique strict order-isomorphism to a unique initial segment of $\mathbb N$. More precisely: If $(I; \prec)$ is a strict finite total order there is a unique $n \in \mathbb N$ (namely $n = \operatorname{card}(I)$) with a unique strict order isomorphism
$$
\pi \colon (I; \prec) \to ( \{1,2, \ldots, n \}; <),
$$
given by 


*

*$\pi(\min(I; \prec)) = 1$ and 

*$\pi(\min(I \setminus \pi^{-1}\{1, 2, \ldots, k \}; \prec)) = k+1$. (*)


Now use the regular Recursion Theorem.
(*) On the surface it seems like I'm using the Recursion Theorem for $(I; \prec)$ to define $\pi$ but I really don't. The existence of $\pi$ follows easily by picking any bijection $f \colon I \to \{1, 2, \ldots, n\}$ together with a permutation $\sigma \colon \{1,2, \ldots, n \} \to \{ 1,2, \ldots, n\}$ such that for all $i,j \in I$
$$
i \prec j \iff \sigma(f(i)) < \sigma(f(j)).
$$
The existence of $\sigma$ can be proved by the regular Recursion Theorem.
