Lazi

essai 1

5.1 Toute vérité se calcul 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.

Énoncé

Condition

p est une preuve lazi.0.0 et x la formule objet de p.

Conclusion

x se calcul en une égalité

Démonstration

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

Si la longueur de p est 1

Alors l'unique déduction ne peut avoir de condition, et donc elle déduit une égalité. Une égalité est un calcul terminé.

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 n'est pas une déduction "égalité et vérité" alors l'objet de p est une égalité et donc on a la conclusion voulue.

Si d est une déduction "égalité et vérité" : Soit a la première condition de cette déduction. On peut tronquer p pour que son objet soit a, par récurrence on déduit que a se calcul en égalité.