Lazi

Étude récursivité

Contexte

Le théorème "Toute vérité se calcule en une égalité:Calcul et remplacement" nécessite un raisonnement récursif. Il utilise un 4-uple de formules. Il faut donc définir une liste de uples de formules pour pouvoir appliquer la récurrence dessus.

Questions

  • À partir des 4 formules de départ, quelle est la définition de cette liste ?
  • Prouver que la preuve du théorème utilise une récurrence sur des éléments précédent de la liste.

Étude

Ordre sur les 2-uples

Remarquons qu'à partir de deux ensembles finis totalements ordonés on peut construire un ensemble de couple totalement ordoné et respectant les ordres respectifs des deux ensembles.

Définition de la liste

Essai 1 (rejeté)

Le 4-uples de départ

Soit x1,y1,z1,t1 tels que x1 =c z1 et y1 =c t1.

Quels sont les 4-uples qui doivent être parcourus par la récurrence ?

Lors du calcul de x1 +f y1 et z1 +f t1, on arrive au calcul d'application respectivement a1 +f b1 et c1 +f d1. Le 4-uple est (a1,b1,c1,d1)

Essai 2 (rejeté)

Pour un 4-uple de départ (x,y,z,t), on considère l'ensemble E de tous les couples (a,b) tel que a est utilisé par x +f y et b est utilisé par z +f t.

Comme x +f y et z +f t sont calculables, on peut trouver un ordre O sur E qui respecte la relation "est utilisé par".

Essai 3

Pour un 4-uple (x,y,z,t) tel que

  • x =c z
  • y =c t
  • x +f y est calculable
  • z +f t est calculable

on définie l'ensemble E des 4-uples (a,b,c,d) tels que :

  • a =c c
  • b =c d
  • a +f b est utilisé par x +f y
  • c +f d est utilisé par z +f t

Remarquons que comme x +f y et z +f t sont calculables, E est fini.

Ordre total sur E : comme on peut définir un ordre total sur les formules utilisées par une formule calculable, on peut définir un ordre total sur E respectant la relation "est utilisé par" sur les formules a +f b et c +f d.

Réponse

Voir l'essai 3

@todo