Lazi

Théorème toute vérité lazi.0.0 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é possible : on peut définir la fonction sur les représentations de formules f = x→ "il existe une preuve de x" qui retourne 1b si elle trouve une preuve de x (elle pourra parcourir et tester toutes les preuves possibles), savoir si un énoncé x est prouvable revient à savoir si on a l'égalité f x = 1b.

Remarquons que ce théorème prouve la cohérence de lazi.0.0 puisque si on pouvait prouver 1b = 0b alors on pourrait prouver autre chose que des égalités.

Énoncé

Variables

p,a

Condition

  • p est une preuve lazi.0.0 sans condition
  • a est la vérité déduite par p

Conclusion

Il existe des formules a1,a2 tq :

  • a →c[univocal] (a1 *=* a2)
  • a1 =c a2

Preuve

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

Preuve du théorème pour les preuves de longueur 1

Nous étudierons le cas un peu plus général où la dernière déduction n'a pas de condition. C'est toujours le cas pour les preuves de longueur 1 car pour qu'il y ait une condition il faut au moins une autre déduction précédant la déduction (rappelons que p est sans condition).

L'unique déduction provient de l'une des deux règle "if" ou de la règle "distribute". Donc elle déduit une égalité. Donc a se univocal-calcule en une égalité a1 *=* a2 puisque c'est une égalité et un calcul terminé.

Comme a1 →c[univocal]1 a2, on a a1 →c[loose] a2 donc on a a1 =c a2.

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. Nous avons déjà prouvé les conclusions si la dernière déduction de p n'a pas de condition. Il nous reste à traiter les autres cas:

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

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

Comme x *=* y est une condition de la déduction, elle est démontrée par p, donc on peut extraire de p une preuve de longueur <n de cette condition. Donc par récurrence on déduit x =c y. Donc il existe t tq x →c[loose]= t et y →c[loose]= t. De par les règles du calcul loose, on déduit que z +f x →c[loose]= z +f t et z +f y →c[loose]= z +f t, donc par définition de =c on a z +f x =c z +f y.

Si d est une déduction "fonction égale"

La démonstration est similaire au cas "arguments égaux".

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

Soit x et y les variables de la déduction, donc p prouve x et x *=* y. D'autre part, comme a est par hypothèse la conclusion de la déduction on a y = a.

p contient une sous-preuve de longueur < n de x, donc par récurrence il existe x1,x2 tq x →c[univocal] (x1 *=* x2) avec x1 =c x2, ce qui implique x =c (x1 *=* x2).
p contient une sous-preuve de longueur < n de x *=* y, donc par récurrence on a x =c y.

Comme =c est une relation d'équivalence, de x =c (x1 *=* x2) et x =c y on déduit y =c (x1 *=* x2).

Comme on a y =c (x1 *=* x2), d'après le théorème d'égalité des arguments pour un calcul terminé , il existe y1 et y2 tq :

  • y →c[univocal] (y1 *=* y2)
  • y1 =c x1
  • y2 =c x2

Comme x1 =c x2, x1 =c y1 et x2 =c y2, =c étant une relation d'équivalence on déduit y1 =c y2.

Comme y = a, on a la conclusion voulue : a se univocal-calcule en une égalité y1 *=* y2 et y1 =c y2.

Étude

Recherche d'une preuve