Lazi

Étude sur l'index de récurrence

Contexte

Pour raisonner par récurrence sur le calcul des formules, il est nécessaire d'avoir un index de récurrence adapté. Pour prouver le théorème des calculs et de l'égalité structurel, il nous faut des propriétés précises sur cette index.

Question

Peut-on indexer les formules calculables par une fonction O de sorte que:

  • deux formules calculables x et y, si y est une sous-formule de x, si y →c z et alors O z < O x et si x≠y O y < O x.
  • si on a :
- x et y sont calculables et ont un index ≤ n+1
- x = $F[ distribute ] +f ax +f bx +f x2
- y = $F[ distribute ] +f ay +f by +f y2
alors on a :
- index de (ax +f x2) +f (bx +f x2) ≤ n
- index de (ay +f y2) +f (by +f y2) ≤ n

Étude

Si le critère de récurrence

Réponse