Voir aussi le théorème de définissabilité de Beth
Là l'objectif est de définir un objet mathématique par récurrence au delà du fini. Ceci en exhibant une fonction construisant un objet mathématique nouveau à partir d'un autre préalablement défini. Cela passe par la démonstration de l'existence et de l'unicité de la fonction.
Et là encore un théorème dérivé du précédant le permet.
Nous nous restreindrons à ne l'énoncer que pour la classe (mais via valable aussi pour les ensembles) des ordinaux (mais donc aussi généralisable via le théorème de Zermelo à tout ensemble bien ordonné).
Principe de définition par récurrence sur la classe des ordinaux
Soit F(x, y, z) une formule avec x, y, z comme variables libres, telle que :
∀x∀y (On (x) et y est une application de domaine x) ⇒ il existe un unique z tq F(x, y, z)
Alors il existe une et une seule fonction g, à paramètres dans On, telle que :
Pour tout ordinal α, g(α) est l'unique ensemble u tel que F[α, g|α, u].
( Où « g|α » signifie « g restreint à α », « On(x) » signifie « x est un ordinal » et « On » désigne la classe des ordinaux. )
Soit V la classe de tous les ensembles, et On la classe des ordinaux, on a théorème :
Soit f une fonction de On * V dans V, alors il existe une unique fonction g de On dans V telle que pour tout ordinal α :
g(α) = f(α, g|α).
( Où « g|α » signifie « g restreint à α », et où f et g correspondent à l'extension de la notion de fonction des ensembles aux classes. )
- On appelle ∈-récursion la généralisation de ce théorème avec f fonction de V * V dans V et g fonction de V dans V.