Théorème de preuves d'égalités sur les arguments
Contexte
Quand on a des vérités dérivées, en lazi.0.0, d'une formule prouvée par une déduction d'ajout, comme ces vérités peuvent servir à une déduction d'application, il faut pouvoir non seulement retrouver la déduction d'application, mais aussi prouver l'égalité entre les arguments. En effet, cela est nécessaire pour la traduction. Nous cherchons ici à prouver que l'on peut extraire une preuve d'égalité pour chaque argument.
Énoncé
Variables
m, p, f, n, a1, ..., an, b1, ..., bn
Conditions
- f est un mot non lazi.a.0
- m est la mathématique lazi.a.0 où des mots — dont f — sont ajoutés.
- n ∈ ℕ
- p est une preuve dans m
- l'objet de p est $CT[ (f +f a1+f ... +f an ) ⊢ f +f b1+f ... +f bn ]
Conclusion
Pour tout 1 k ≤ n il existe une preuve dans m qk sans condition et ayant pour objet ak *=* bk.
Preuve
Soit ma la mathématique m où l'on ajoute une déduction déduisant uniquement f +f a1+f ... +f an.
D'après le théorème "toute vérité lazi.0.0 + ajout", pour 1 ≤ k ≤ n on a ak =c bk.
D'après le théorème de la preuve de l'égalité par calcul il existe pour 1 ≤ k ≤ n une preuve dans m de ak =c bk.
CQFD
Recherche d'une preuve
Forme de la preuve
Soit d la dernière déduction de p. Une vérité dont la fonction minimale n'est pas l'égalité ne peut provenir que de la règle "égalité et vérité". Soit x et y les variables de la règle. D'après le théorème "toute vérité lazi.0.0 + ajout, x se calcule en une formule de fonction minimale f, donc la fonction minimale de x ne peut être l'égalité.
Donc par récurrence il existe une liste de formule v1,...,vm tq v1 = f +f a1+f ... +f an, vm = f +f b1+f ... +f bn et tq pour 1 ≤ k < m vk p contienne la déduction égalité et vérité ayant pour valeur de variables $T[ vk , vk+1 ].
Essai 1
D'après le théorème de remplacement de variable, si on remplace f dans p par une formule au sens m, alors p reste valide et son objet est celui de p ayant subi le même remplacement.
Pour 1 ≤ k ≤ n, soit qk = p où l'on remplace f par $F x1,...,xn → xk = ak .
Et si ak contient f ?