Lazi

Récurrence pour commutativité

Contexte

Le théorème de commutativité de =c a besoin d'une forme de récurrence.

Question

Quelle récurrence utiliser ?

Étude

Essai 3

La définition de =c est récursive et dans une logique de niveau 1 car on a un test d'égalité, que la notion de calculable est de niveau 1.

Peut-on prouver que si on a une proposition logique de niveau 1 avec une récursivité sur des "or" (la formule contient une infinité de "or"), alors si la proposition est vraie cela implique que la formule est finie ? On retombe sur la nécessité d'une vérité proche de celle que l'on cherche à démontrer de manière plus générale : Toute véritése calcule en une égalité, car à partir d'une vérité (ici une disjonction) on doit montrer qu'elle ne peut provenir que de certaines déductions (ici d'un membre d'une disjonction qui est vrai).
@todo

Ou faut-il limiter les formules avec des "or" pour qu'elles ne puissent pas contenir une infinité de "or" (on a le même problème pour "imply") ?

Essai 2

Peut-on utiliser le fait que si on a xc2 =c yc2 c'est que la proposition logique provenant de la définition de "=c" est finie ? Cela aiderait pour la récurrence.

Raisonnons par l'absurde et supposons que l'on ait x =c y avec une imbrication infinie de cas du split (si on n'a pas cette imbrication infinie, on peut montrer la commutativité car les autres conditions sont symétriques).

Essai 1

Soit I la relation définie sur les couples de formules par : on a I x y ssi:

  • x est calculable
  • x →ct y +f xc2 ou (y calculable et x →ct xc1 +f y).

Il faut que I puisse s'étendre à une relation d'ordre stricte sur un ensemble fini.

Si on avait une boucle: par exemple si x →ct xc1 +f x

Réponse