Lazi

essai 7

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.

Nous ajoutons cette définition qui sera utilisée dans l'énoncé:

Définition d'équilibré

Soit x et y deux formules, on dit que x et y sont équilibrés ssi:

  • si x ou y est calculable alors x et y sont calculables
  • si x et y est calculable, soit xc et yc les résultats respectifs des calculs, si xc ou yc a pour fonction "=", alors:
    • Les deux ont pour fonction "=".
    • Les deux ont le même nombre d'arguments .
    • Chaque paire d'arguments correspondants de xc et yc sont équilibrés.

De plus on note "x et y sont équilibrés" "x =e y"

É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
  • x1 =e x2

Étude préliminaire

Recherche d'un contre-exemple (non abouti)

Quel critère de récurrence

Pour pouvoir être utilisé pour la règle du tiers exclu il faut que:

  • la calculabilité d'un des termes de l'égalité entraîne la calculabilité des deux
  • il faut une propriété sur les deux termes telle que si l'un se calcule en un mot clé alors l'autre ne peux se calculer en une application

Lors de la récurrence, le critère doit permettre:

  • pour la règle
"arguments égaux" :
  • si l'un des termes se calcule en 1b ou 0b, alors l'autre aussi
  • si b =e c , alors a +f b =e a +f c
  • pour la règle "fonction égale": si b =e c , alors b +f a =e c +f a
  • pour la règle "égalité et vérité" :
    • une vérité se calcule en une égalité x *=* y équilibrée, donc comme x est équilibré, y aussi.

Démonstration

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

Si p est de longueur 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
  • si les deux membres sont calculables, comme les résultats de leur calcul sont syntaxiquements égaux, ils sont équilibrés.

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 =e c.
Le théorème "Calcul et remplacement" s'applique, et l'on a donc a +f b =c a +f c.