Lazi

imply

Contexte

Il s'agit d'ajouter les règles de déduction pour introduire le mot clé pour l'implication ("imply").
Voir aussi "Comment définir les extensions nécessaire ?"

Question

Comment définir l'extension pour ajouter le mot clé "imply" ?

Étude

Ce que l'on voudrait

L'usage attendu de "imply", qui est celui des mathématiques classique, est le suivant :

Déduction d'ajout :

  • une formule x
  • une formule y
  • une preuve p de y
Ayant pour objet une ctruth :
  • conditions : celles de p moins la condition x
  • conclusion : y

Déduction d'application :

  • une formule x
  • une formule y
Ayant pour objet une ctruth :
  • conditions : x
  • conclusion : y

Traduction de la déduction d'ajout :

rien

Traduction de la déduction d'application :

le p de la déduction d'ajout

Le problème

Exemple 1 : A = (A ⇒ (1b = 0b)), preuve de A ⇒ (1b = 0b)

Soit A tq A = (A ⇒ (1b = 0b) ).

Preuve de A ⇒ (1b = 0b) :

Supposons A, on a alors A ⇒ 1b = 0b, donc on a 1b = 0b

Application :

Comme on a A ⇒ 1b = 0b et A = (A ⇒ 1b = 0b), on a A. On déduit donc 1b = 0b.

Traduction de la déduction d'application de A ⇒ (1b = 0b) :

On remplace par la preuve, qu'il faut traduire.
On doit traduire la déduction d'application de A ⇒ (1b = 0b), mais elle fait appel à la déduction d'ajout : on boucle.

Exemple 2 : A = (A ⇒ (1b = 1b)), preuve de A ⇒ (1b = 1b)

Preuve de A ⇒ (1b = 1b)

Supposons A, comme "=" est une relation d'équivalence on a 1b = 1b

Application :

Comme on a A ⇒ (1b = 1b) et que A = A ⇒ (1b = 1b), on a A. En appliquant A ⇒ (1b = 1b) on déduit 1b = 1b.

Traduction de la preuve :

La traduction la déduction d'application ne pose pas problème.
On remplace aussi le mot "imply" par n'importe quel mot (par exemple 0b) on élimine les vérités déduites en utilisant les vérités provenant des déductions d'ajout. Donc la sous-preuve déduisant A est éliminée.
Il n'y a donc pas de problème de traduction.

Exemple 3 : A = A ⇒ (1b = 0b), preuve de (1b = 1b ⇒ A) ⇒ (1b = 0b)

Preuve de (1b = 1b ⇒ A) ⇒ (1b = 0b) :

De 1b = 1b ⇒ A on déduit A, donc on déduit A ⇒ (1b = 0b), donc on déduit 1b = 0b

Application :

Prouvons 1b = 1b ⇒ A, en supposant 1b = 1b :
Pour prouver A, prouvons A ⇒ (1b = 0b) en supposant A :
Comme on a A, on a 1b = 1b ⇒ A, comme on a (1b = 1b ⇒ A) ⇒ (1b = 0b), on déduit 1b = 0b

Traduction de la déduction d'application de (1b = 1b ⇒ A) ⇒ (1b = 0b) :

On remplace par la preuve, qu'il faut traduire.
On doit traduire la déduction d'application de A ⇒ (1b = 0b), mais on ne peut pas car on n'a pas de déduction d'ajout correspondante.

Exemple 4 : A = (A ⇒ (1b = 0b)) , preuve de (∀ x | A) ⇒ (1b = 0b)

Preuve de (∀ x | A) ⇒ (1b = 0b) :

De ∀ x | A, on prend x = 1b et on déduit A, donc on déduit A ⇒ (1b = 0b), donc on déduit 1b = 0b

Application :

Prouvons ∀ x | A
Il nous faut prouver A, prouvons A ⇒ (1b = 0b) en supposant A :
Comme on a A on a ∀ x | A. Comme on a (∀ x | A) ⇒ (1b = 0b) , on a 1b = 0b

Traduction de la déduction d'application de (∀ x | A) ⇒ (1b = 0b):

On remplace par la preuve, qu'il faut traduire.
Il faut traduire la déduction d'application de ∀ x | A, on remplace donc la preuve de ∀ x | A en remplaçant x par 1b :
Il faut traduire la déduction d'application de (∀ x | A) ⇒ (1b = 0b) : on boucle

Exemple 5 : A = (A ⇒0 (1b = 0b)) , preuve de (A ⇒1 (1b = 0b)

Soit A tq A = (A ⇒0 (1b = 0b)).
Preuve de A ⇒1 (1b = 0b) :

Supposons A, on a alors A ⇒0 1b = 0b, donc en appliquant ⇒0 on a 1b = 0b

Application :

On a A ⇒1 (1b = 0b) et A = (A ⇒0 (1b = 0b)). On est coincé pour montrer A car A ⇒0 (1b = 0b) ne peut se prouver à partir de A ⇒1 (1b = 0b)

Exemple 6 : A = (∀x|A) ⇒ (1b = 0b), preuve de A ⇒ (1b = 0b)

Preuve de la déduction d'ajout , supposons A :

On a donc (∀x|A) ⇒ (1b = 0b). Comme on a A, on a (∀x|A), donc on a 1b = 0b

Preuve de la prémisse (∀x|A) :
On a (∀x|A) ⇒ (1b = 0b), donc on a A, d'où l'on déduit ∀x|A.

Exemple 6 : A = (∀x|A) ⇒ (1b = 0b), preuve de (∀x|A) ⇒ (1b = 0b)

Preuve de la déduction d'ajout , supposons (∀x|A) :

On a donc A (on prend par exemple x=0b). Par égalité on a (∀x|A) ⇒ (1b = 0b). Par application on a 1b = 0b

Preuve de la prémisse (∀x|A) :

On a (∀x|A) ⇒ (1b = 0b), donc on a A, d'où l'on déduit ∀x|A.

Recherche d'un critère de validité

Essai 4

Différence par rapport au 3 : on le revoit pour le rendre plus claire.

Recherche de déductions :

Quand on liste / désigne les déductions vérifiant certaines caractéristiques dans une preuve, on ne se réfère pas aux sous-preuves.

Preuve et récurrence :

La preuve de la validité de la traduction est une preuve par récurrence sur une mesure de la preuve, car la traduction est une fonction récursive.
Remarquons qu'une preuve de mesure 1 est valide car elle ne peut avoir une déduction d'ajout et d'application, on montre facilement qu'elle ne peut avoir de déduction d'application et qu'une déduction d'ajout seule ne peut déduire une vérité sans mot clé. Il nous reste à prouver la validité dans le cas où la mesure de la preuve est n+1 et où la validité est prouvée jusqu'à n. Cas dans lequel nous nous plaçons pour la suite.

La dernière déduction et la preuve précédente :

Si la dernière déduction n'est pas une déduction d'application "imply", alors le cas est traité par le reste de la preuve sur la validité des extensions des mots clés (forAll, exists, imply). Nous supposeront donc désormais que la dernière déduction est une déduction d'application "dap". Par récurrence nous pouvons supposer que les déduction d'application précédentes sont traduites. On peut montrer qu'il existe une déduction d'ajout d'un imply "daj" reliée par une chaîne "égalité et vérité" à dap. Soit paj la sous preuve de daj et ij l'objet de daj de prémisse pij. Soit ip l'implication utilisée par dap, et pip saprémisse.

Définition d'utilisation réelle d'une vérité :

Soit p une preuve d'objet c et v une vérité déduite au cours de l'exécution de la preuve. Si les conditions de p augmentent ou si p devient invalide si l'on supprime les déductions déduisant v ainsi que toute celles récursivement l'utilisant, alors on dit que v est une vérité réellement utilisée par p.

Traduire dap :

Si la sous-preuve prouvant pip n'utilise pas réellement ij, alors cette sous preuve suivie de paj est une preuve valide sans la condition pip. En effet, on a une preuve paj valide sous la condition pij que l'on fait précéder d'une preuve valide de pip. (relier pij et pip)

Essai 3 (à améliorer)

Soit daj la déduction d'ajout de preuve p et déduisant i.
Soit dap la première déduction d'application de daj. Soit pi sa prémisse.

On suppose que la première phase de traduction de preuve est faite jusqu'à dap. Il n'y a donc plus, pour les déductions sur les mots clés, que les déduction d'ajout.

Par construction les preuves contenues dans les déductions d'ajout des imply sont valides si la prémisse est prouvée. L'invalidité possible provient du fait que la preuve de la prémisse peut se situer après daj car alors la preuve de la prémisse peut utiliser la vérité déduite par daj.
Remarquons que sans cette utilisation de la vérité déduite par daj, p est valide à l'endroit de dap. Nous n'avons donc qu'à étudier le cas où la preuve de la prémisse utiliser la vérité i.

Pour la preuve de la prémisse, i ne peut être utilisées que par des déductions "égalité et vérité" ou des déduction d'ajout (par exemple déduire "∀x i" à partir de "i"), voir l'exemple 6 ci-dessus.

i peut être utilisée mais son utilisation peut être détruite par la deuxième phase de la traduction. Comme i contient un mot clé (imply) à traduire, c'est le cas s'il n'y a pas de déduction d'application dans les déductions reliées à l'utilisation de i. Hors il n'y a pas d'autre déduction d'application que dap.

Si l'utilisation de i disparait à la seconde phase de la traduction. Ce cas est possible car on peut toujours ajouter dans une preuve une déduction basée sur une vérité sans en utiliser le résultat. Il n'y a donc aucunne conséquence et donc la traduction de dap par p est valide pour la même raison que l'on a déjà donné quand i n'est pas utilisé.

Donc le seul cas où on peut avoir une incohérence est quand l'utilisation de i ne disparait pas à la seconde phase de la traduction. Comme les vérités dérivées de i par des déductions "égalité et vérité" et les déductions d'ajout contiennent "imply", et que imply est un mot à traduire, cela implique qu'une déduction d'application est utilisée. Hors la seule déduction d'application est dap. Donc une vérité dérivée de i est utilisée comme prémisse de dap.

Voir l'étude sur les théorèmes à prouver pour raisonner sur nombre d'imply.

Voir l'étude sur le critère à utiliser pour blocker les prémisses contenant une infinité d'imply.

Essai 2 (à revoir)

Soit daj la déduction d'ajout de preuve p et déduisant i.
Soit dap la première déduction d'application de daj. Soit pi sa prémisse.

On suppose que l'on emploie des imply avec des indices, c'est à dire qu'à chaque mot clé imply est accolé un entier naturel qui ne peut être modifié, ou autrement dit qu'il y a une infinité de mot "imply".

Remarque : les formules en argument de dap (prémisse et conclusion) sont égales à celles de daj mais pas forcément syntaxiquement égales.

Pour traduire p nous avons besoin que la prémisse soit prouvée car p peut contenir des déductions d'applications sur elle.

Remarquons que pour toute déduction d'application on peut remonter — après traductions des déductions d'application précédantes — à la déduction d'ajout car les seules déductions possibles sont des "égalité et vérité". Donc lors d'une traduction, quand on traduit une déduction d'application c'est que l'on a déjà traduit ce qui précède, et donc on peut remonter à la déduction d'ajout juste en suivant les déductions "égalité et vérité". On peut donc savoir lors d'une traduction si une certaine déduction d'ajout est utilisée pour la traduction.

Si lors de la traduction de p à l'endroit de dap la déduction d'ajout daj est utilisée :

Alors comme daj se traduit en p cela implique que la traduction de p inclut la traduction de p et donc il y a une boucle. La traduction est donc impossible car on a une incohérence logique.
Mis à part par la prémisse, p ne peut faire appel à son propre daj, donc la traduction de déduction d'application provenant à la base de pi font appel à daj. Donc lors de cette traduction, une phrase égale (au sens lazi.0.0) à i est fournie par la traduction. Donc après des traduction cette phrase est reliée par des déduction d'égalité et vérité à daj.
Or d'après le théorème ??? on en déduit que pi contient le mot "imply" de même indice que celui de daj. Comme pi égalie au sens lazi.0.0 à la prémisse de daj, on déduit que la prémisse de daj contient un "imply" de même indice que celui de daj.

Donc en ayant en contrainte que la prémisse de la déduction d'ajout n'a des imply que d'indice différent à l'indice de la déduction, on a alors p traduisible et valide.

Problème : si on est dans un let le théorème ??? invoqué est faux car on peut avoir un Let I = implyI.

Essai 1 (échec)

Pour simplifier le raisonnement, dans un premier temps supposons pour la suite qu'il n'y ait que les déductions imply (pas d'autres mots clés).

Soit daj la déduction d'ajout de preuve p et déduisant i.
Soit dap la première déduction d'application de i.

Si i est utilisé en tant que vérité pour prouver la prémisse :

Comme i est un imply, il ne peut être utilisé que par la déduction d'application et la déduction "égalité et vérité". Or il n'y a pas de déduction d'application puisque dap est la première (on traduit les déductions d'applications dans l'ordre d'apparition). Si elle utilise i alors c'est par la déduction "égalité et vérité". Et comme le y déduit par cette déduction est de la même forme que i (une implication égale), on déduit alors que la prémisse est égale à i. Donc la prémisse contient un imply (et de même indice si ce sont des imply indicés).

Si i n'est pas utilisé en tant que vérité pour prouver la prémisse :

Alors il n'y pas de d'incohérence à traduire dap par p car :
- il n'y a pas de boucle sur p dans la traduction de p car il y a nulle part de référence à daj.
- après les traductions des déductions d'application daj peut être éliminées ainsi que les déductions en ayant besoin (car il n'y a pas de conséquences d'une implication qui soit sans imply hormis les déductions d'application).

@todo
@extension