essai 6
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 sont soit toutes les deux calculables, soit toutes les deux incalculables. De plus si elles sont calculables, en les calculant on obtient une certaine partie fonction syntaxiquement identique et des arguments égaux par calcul.
Énoncé
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
- on a x1 =c x2
Démonstration
Recherche d'un contre-exemple (non abouti)
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 "=c"
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.
Comme la vérité b *=* c est prouvée par une preuve strictement plus courte que p, par récurrence on déduit b =c c.
Le théorème "Calcul et remplacement" s'applique, et l'on a donc a +f b =c 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 et on a a1 =c a2
- a *=* x étant déjà une égalité (elle se calcul en elle-même), on a a =c x.
Soit ac et xc les résultats des calculs de a et x. Remarquons que ac = (a1 *=* a2).
Par définition de =c , on a deux cas:
- ac = xc
- comme ac est une application, xc est une application xc1 +f xc2 où:
- $F[ equal] +f a1 =c xc1
- a2 =c xc2
Cas 1:
On a xc = (a1 *=* a2)
On a donc la conclusion voulu: x se calcul en une égalité a1 *=* a2 et on a a1 =c a2
Cas 2:
Comme x se calcul en xc1 +f xc2, le calcul de xc1 est terminé (car xc1 a la position de fonction).
Pour l'égalité $F[ equal] +f a1 =c xc1, on a à nouveau deux cas:
Cas de l'égalité : $F[ equal] +f a1 = xc1 :
Il nous reste à montrer que a1 =c xc2:
Comme $F[equal] a son calcul terminé et n'est pas une application, par définition de =c, on a xc1a = $F[equal].
Donc xc1 = $F[equal] +f xc1b, donc x se calcul en $F[equal] +f xc1b +f xc2.
Il nous reste à montrer que xc1b =c xc2:
encours : faire la conclusion, montrer la commutativité et l'associativité de =c