É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".