Se calcul et calculabilité

Contexte

Théorème de base sur la relation entre le calcul (→c) et la calculabilité.

Énoncé

Variables

x, y

Conditions

• x et y sont des formules
• x →c y ou y →c x

Conclusion

La calculabilité de x et y sont identiques.

Preuve

Supposons x calculable et x →c y : alors il existe z qui est un calcul terminé et tel que x c→ z. Comme x →c y et que le calcul est linéaire (il n'y a pas le choix de la manière de calculer), on déduit que l'on a soit y = z soit y →c z. Dans les deux cas on déduit que y est calculable.

Supposons x calculable et y →c x : y est alors clairement calculable.

Par symétrie des propriétés utilisées dans l'énoncé, si y est calculable alors x est calculable.