Lazi

Recherche d'une preuve

Partir de seulement "toute vérité se calcul en une égalité"

L'idée, pour trouver le critère de récurence, est de partir d'un minimum et de grossir la propriété. On part de "toute vérité se calcul en une égalité".

Voyons suivant la dernière déduction de la preuve, ce que l'on doit ajouter au critère.

Si la dernière déduction est ...

Une déduction déduisant une égalité

Donc la preuve déduit une égalité.

égalité et vérité

Par récurrence a se calcul en une égalité. Nous avons besoin de la propriété:

Si a se calcul en une égalité et a *=* b est prouvé alors b se calcul en une égalité.

Mais prouver cette propriété par récurrence entraînera de devoir prouver une propriété plus grande. Je pense qu'il faut que la propriété (que l'on nomera P) soit :
Si a est calculable et que a se calcul en une formule ac ayant une fonction minimale qui soit un mot passif, alors b se calcul en une formule bc telle que :

  • bc a une fonction minimale qui soit la même que celle de ac
  • ac et bc ont le même nombre d'argument
  • pour chaque paire d'arguments x,y correspondants, on a P x y

Reprenons la démonstration avec P

Si la dernière déduction est une déduction sans condition

Dans ce cas on déduit une égalité et le calcul des deux membres aboutit à la même valeur, donc la propriété est prouvée.

Si la dernière déduction est "arguments égaux"

On a a *=* b, donc on a par récurrence P a b. Il nous faut prouver P (c +f a) (c +f b). Supposons que c +f a soit calculable et se calcul en une formule cac ayant une fonction minimale qui soit un mot passif. Le calcul de a ou b aboutit à une formule ac ou bc ayant une fonction minimale passive. Il en résulte que le calcul de c +f a est identique au calcul de c +f b hormis la partie calcul de a ou b. Donc si l'un est calculable alors l'autre aussi, de plus les deux formules sont identiques sauf le remplacement de a par b et le remplacement de ac par bc. Donc la fonction minimale est identique (a ne peut être une fonction du résultat du calcul car il serait calculé), les deux ont le même nombre d'arguments. Comme chaque argument est identique au remplacement pret on a P sur chaque paire.

Si la dernière déduction est "fonctions égales"

Les calculs de a +f c et b +f c aboutissent à ac +f c et bc +f c, comme on a P c c , on a P (ac +f c) (bc +f c)

Si la dernière déduction est "égalité et vérité"

Par récurrence on a P a b. De plus par récurrence a se calcul en une égalité a1 *=* a2. Comme on a P a b, b se calcul en une égalité b1 *=* b2 et on a P a1 b1 et P a2 b2. Comme on a P a1 a2, on déduit que l'on a P b1 b2, par symétrie et transitivité de P.

Donc il faut que P soit une relation symétrique. Pour cela il faut ajouter que la première condition soit symétrique.

Généralisation avec =c

Idée

Essai 2

L'essai 1 était trop général car les propriétés à prouver étaient fausses pour certaines valeurs de R. On reprend la construction de l'essai 1 mais pour un R particulier correspondant à =c.

Soit R la relation définie sur les formules : R x y ssi on a la disjonction :

  • x et y sont calculables et ont le même résultat de calcul.
  • x et y sont incalculables.

Soit =c la relation définie sur les formules : x =c y ssi on a la disjonction :

  • R x y
  • x, y sont des applications x1 +f x2, y1 +f y2 et R x1 y1 et R x2 y2

On montre que R est une relation d'équivalence.
On montre que =c est une relation d'équivalence.
On montre que si x =c y et si x ou y est calculable de calcul xc et yc alors :

  • la fonction minimale de xc et yy est un mot identique
  • xc et yc ont le même nombre d'arguments
  • chaque couple d'arguments correspondant vérifie la relation =c

Essai 1

La relation P définie ci-dessus est proche de =c. Il me parait possible d'utiliser plutôt =c , ce qui donnerait un résultat plus puissant car il y a moins de contraintes sur =c.

On utiliserait les théorème suivant:

Si R est une relation d'équivalence sur les formules tel que:
  • si x →c y alors R x y
  • si x et y sont deux mots clés différents alors on ne peut avoir R x y

Pour une telle relation R, nous définissons une relation dérivée C R, deux formules sont en relation si on peut obtenir la même formule en remplaçant des sous-formules par des versions équivalentes par R. Définissons plus formellement C. Pour R une relation sur les formules , on définit la relation C R sur les paires de formules par la plus petite relation telle que :
  • si x, y sont des formules telles que R x y, alors C R x y
  • si x,y,z,t sont des formules tq C R x z et C R y t, alors C R (x +f y) (z +f t)

Alors soit x, y,xc,yc tq C R x y, x →c xc et y →c yc. On a alors C R xc yc.

À partir de ce théorème, pour R qui rend équivalent les formules non calculables, on prouve une propriété de décomposition.

On a alors les théorèmes nécessaires pour utiliser la démonstrations décrite ci-dessus avec une version de P plus large.