Étude des contraintes sur =c
Contexte
La définition actuelle de =c ne semble pas valide car il ne semble pas y avoir de critère de récurrence valide. Le problème vient, lors du calcul de =c, de l'imbrication infinie d'arguments sans qu'il y ait pour autant de formule incalculable.
Question
Comment palier au problème de récurrence invalide ?
Étude
Le problème de récurrence infini lors du calcul de =c
Voir essai 3/L'algorithme se termine-t-il toujours ? de la page Recherche d'une preuve.
Les contraintes sur =c
Ces contraintes découlent de l'utilisation de =c dans le théorème "Toute vérité se calcule en une égalité"
- =c doit être une relation d'équivalence.
- Si x =c y et z =c t alors x +f z =c x +f t.
- Pour des formules x et y qui sont des mots, si x =c y alors x = y.
- Pouvoir faire des preuves par récurrence.
Les formules contenant une imbrication infinie d'arguments peuvent être calculées.
Soit x,y 2 formules et z une formule contenant une imbrication infinie d'arguments.
On peut avoir z +f x →c 1b et z +f y →c 0b.
Donc contrairement aux formules incalculables, elles peuvent être utilisées dans des calculs. C'est le cas si à un certain niveau le paramètre qui s'auto-imbrique n'est pas pris en compte.
Nouvelle définition de =c
Pour x et y deux formules, et x =c y ssi on a la disjonction:
- x = y
- si il existe xc1 tq x →c1 xc1 : xc1 =c y
- si il existe yc1 tq y →c1 yc1 : x =c yc1
- si x et y sont des applications x1 +f x2 et y1 +f y2 : x1 =c y1 et x2 =c y2
Étude de la nouvelle définition
La définition est en logique de niveau 0.
Si on prouve x = y alors x =c y.
Si x =c y alors x = y.
Si x =c if y z t où x est un mot alors if y z t →c x
Réponse
Par une nouvelle définition de =c , voir la section "Nouvelle définition de =c".