Lazi

Calculabilité d'une formule utilisée dans un calcul

Contexte

Pour trouver un ordre sur les sous-formules d'une formules calculables, il faut différencier les sous-formules ignorées des sous-formules calculées, ces dernières étant calculables (sinon la formule globale ne le serait pas). Nous utiliseront cette propriété pour le théorème Toute vérité se calcule en une égalité:Calcul et remplacement:Ordre total sur les formules utilisées par un calcul.

Énoncé

Soit x et y deux formules.

Conditions

  • x une formule calculable
  • y est utilisée dans le calcul de x

Conclusion

y est calculable

Preuve

On montre par récurrence que si y est utilisée dans le calcul de x alors le calcul de x inclue le calcul de y. Donc pour que x soit calculable il faut que y soit calculable.

@todo