É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 :- x = $F[ distribute ] +f ax +f bx +f x2
- y = $F[ distribute ] +f ay +f by +f y2
- index de (ax +f x2) +f (bx +f x2) ≤ n
- index de (ay +f y2) +f (by +f y2) ≤ n
- index de (ay +f y2) +f (by +f y2) ≤ n
Étude
Si le critère de récurrence