Lazi

essai 5

Toute vérité se calcule en une égalité

Contexte

Pour raisonner par récurrence sur les preuves lazi.0.0, nous allons déjà trouver des propriétés de base sur les vérités de cette mathématique.

Ce théorème peut se transcrire ainsi en langage courant: au fond les seules vérités sont des égalités. Remarquons que l'égalité renferme toute la complexité de l'existence, par exemple on peut se demander si la fonction "il existe une preuve de" (cette fonction peut tester toutes les preuves possibles) retourne 1b avec comme argument l'énnoncé d'un théorème très complexe.
Ce théorème exprime aussi que deux choses égales dont l'une est calculable sont toutes les deux calculables et ont une partie des formules syntaxiquement égales du côté des fonctions et des arguments (de la fonction trouvée égale) sémentiquement égaux.

Énoncé

Définition locale

Pour deux formules x et y on définit x *=s* y par la disjonction:

  • x = y
  • x est une application x1 +f x2, yc est une application y1 +f y2 et on a:
    • x1 *=s* y1
    • il exite une preuve lazi.0.0 de x2 *=* y2

Condition

p est une preuve lazi.0.0 sans condition et x la conclusion de p.

Conclusions

  • x se calcul en une égalité x1 *=* x2
  • si x1 ou x2 est calculable alors x1 et x2 sont calculables, soit x1c et x2c les calculs de x1 et x2, on a x1c *=s* x2c

Démonstration

Nous démontrons le théorème par récurrence sur la longueur de la preuve p.

Si la longueur de p est 1

Alors l'unique déduction ne peut avoir de condition, c'est donc l'application de l'une des deux règle "if" ou de la règle "distribute". Donc elle déduit une égalité. Comme le calcul des deux membres de l'égalité aboutit au même calcul, les autres conclusions sont vérifiées:

  • si un des membres est calculable alors l'autre aussi
  • les calculs des deux membres sont syntaxiquement identiques et vérifient donc la relation "*=*"

Si le théorème est montré pour les preuves de longueur <n

Soit p une preuve de longueur n. Soit d la dernière déduction de p.

Si d est une déduction provenant des 3 règles sans condition

On peut utiliser le même raisonnement que pour le cas où la longueur de p est 1.

Si d est une déduction "arguments égaux"

x se calcul en une égalité puisque c'est une égalité de la forme a +f b *=* a +f c.

Montrons que si l'un des membres est calculable alors l'autre aussi.

Comme a = a et que b *=* c est déduit par p, on a a +f b *=s* a +f c

Si d est une déduction "fonctions égales"

x se calcul en une égalité puisque c'est une égalité de la forme b +f a *=* c +f a. Comme b *=* c est démontré par une troncature stricte de p et se calcul en lui-même, on peut appliquer l'hypothèse de récurrence et on obtient b *=s* c. D'autre part il existe une preuve lazi.0.0 de a *=* a (réfléxivité de l'égalité). Donc par définition de la relation "*=s*", on déduit que l'on a b +f a *=s* c +f a.

Si d est une déduction "égalité et vérité"

Montrons que x se calcule en une égalité: soit a la valeur de la variable "x" de la règle. Comme a et a *=* x sont prouvés par des troncatures strictes de p, par récurrence a et a *=* x vérifient les conclusions du théorème. Donc a se calcul en une égalité a1 *=* a2. Comme a se calcule en une application et que l'on a a *=* x , par l'hypothèse de récurrence on déduit que x se calcule en une application x0 +f x2 avec $F[ equal] +f a1 *=* x0 et a2 *=* x2. On a une preuve (scrictement plus courte que p) de $F[ equal] +f a1 *=* x0, on peut réappliquer la récurrence. On obtient au final que x se calcule en une formule $F[ equal] +f x1 +f x2 et qu'il existe des preuves plus courtes que p de a1 *=* x1 et a2 *=* x2.

Définisson localement la relation "S" : S x y = les conjonctions :

  • si x se calcule en un mot alors y se calcule en un mot
  • si x se calcule en une application alors :
    • y se calcule en une application
    • il existe des preuves de l'égalité entre:
      • les fonctions de x et y
      • les arguments de x et y
  • S n y x

Montrons que S est une relation transitive. Soit a,b et c des formules telles que S a b et S b c. Si a se calcul en un mot alors b et donc c aussi et donc c aussi. Si a se calcul en une application alors b aussi et donc c aussi. Soit a1,a2,b1,b2,c1,c2 tel

D'après l'hypothèse de récurrence, si on a x *=* y par une preuve de longueur m<n, alors on a S m x y .

Montrons que l'on a S n x1 s2: comme on a a1 *=* x1 par une preuve de longueur <n, on a par hypothèse de récurrence S n x1 a1. Comme on a a1 = a2 par une preuve de longueur <n, on a S n a1 a2. Comme on a a2 = x2 par une preuve de longueur <n, on a S n a2 x2. Comme S n est une relation transitive, on a S n x1 x2.