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) :
Application :
Traduction de la déduction d'application de A ⇒ (1b = 0b) :
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)
Application :
Traduction de la preuve :
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) :
Application :
Traduction de la déduction d'application de (1b = 1b ⇒ A) ⇒ (1b = 0b) :
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) :
Application :
Traduction de la déduction d'application de (∀ x | A) ⇒ (1b = 0b):
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) :
Application :
Exemple 6 : A = (∀x|A) ⇒ (1b = 0b), preuve de A ⇒ (1b = 0b)
Preuve de la déduction d'ajout , supposons A :
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) :
Preuve de la prémisse (∀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 :
Preuve et récurrence :
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 :
Définition d'utilisation réelle d'une vérité :
Traduire dap :
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 :
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 :
Si i n'est pas utilisé en tant que vérité pour prouver la prémisse :
- 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