[!proposition] schéma mu borné
Soit A \subseteq \mathbb{N}^{p+1} un ensemble récursif primitif
La fonction f \in \mathscr{F}_{p+1} définie comme suit est fonction récursive primitive :
f(\overline{x}, z) = 0 s'il n'existe pas d'entier t \leq z tel que (\overline{x}, t) \in A
- sinon
f(\overline{x}, z) est égal au plus petit des entiers t \leq z tels que (\overline{x}, t) \in A
- i On utilisera la notation :
\boxed{f(\overline{x}, z) = \mu t \leq z ((\overline{x}, t) \in A)}
[!definition] Définition formelle
La fonction f est définie par récurrence, fonction récursive primitive#^schema-par-cas, et par fonction récursive primitive#^somme-et-produits-limites :
f(\overline{x}, 0) = 0
f(\overline{x}, z+1) = f(\overline{x}, z) si \sum\limits_{y=0}^{z} \Big( \chi _{A}(\overline{x}, y) \Big)\geq 1 (permet de tester si au moins un y \leq z est dans A)
f(\overline{x}, z+1) = z+1 sinon et si (\overline{x}, z+1) \in A
f(\overline{x}, z+1) = 0 dans les autres cas
^main