Lazi

Les points communs aux extensions d'ajout de mot clés

Contexte

Les extensions pour forAll, exists, and, or, imply ont des points communs, que ce soit dans les déductions à ajouter ou les démonstrations de validité.

Question

Quels sont les points communs de ces extensions ?

Étude

L'introduction d'un mot clé pour généraliser une forme de preuve

Chacune de ces extensions ajoute un nouveau mot clé au langage. Il permet de généraliser une forme de preuve. Par exemple:

  • x ∧ y : permet d'assembler deux preuve en une seule
  • x ∨ y : permet de prouver z sans avoir à prouver x ou y mais seulement à prouver que l'un des deux est vraie.
  • ∀ x ;; f x : permet de paramétrer une preuve par une valeur (celle de x).

Déduction d'ajout et d'application

Pour chacun des mots clés les déductions ajoutées par les extensions peuvent être de deux types:

  • déduction d'ajout: elle ajoute une vérité contenant le mot clé en fonction principale
  • déduction d'application: à partir, entre autre, d'une vérité ayant le mot clé en fonction principale, déduit une vérité

Il y a une seule déduction d'ajout et une seule déduction d'application.

Traduction

La traduction des déductions provenant des extensions par mot clés est en deux phrases :

  1. La traduction, en commençant par le début de la preuve, des déductions d'application (dans l'ordre d'apparition, peu importe le mot clé), le résultat d'une traduction d'une déduction d'application devant lui-même être traduit.
  2. L'élimination des déductions devenues inutiles : les déductions d'ajout et les vérités dérivées par "égalité et vérité". En effet, ces vérités contiennent des mots clés et ne peuvent constituer l'objet de la preuve car on traduit une preuve si sa conclusion est une formule sans les mots clés à traduire.

Association de la déduction d'ajout correspondant à une déduction d'application

Pour la traduction on aura besoin de retrouver la déduction d'ajout correspondant à la déduction d'application. Cela implique qu'il y a toujours une déduction d'ajout correspondant et que l'on puisse prouver et trouver effectivement laquelle est-ce. Pour cela nous aurons besoin de traduire les mots clés mais aussi les règles supplémentaires à lazi.0.0 et ce ne sera valable que pour les preuves sans hypothèse.
Nous aurons aussi besoin d'un théorème de consistance pour montrer que les preuves ayant un contexte où l'on pourrait prouver n'importe quoi ne sont pas à traduire, car dans ce cas on n'aurait pas forcément de déduction d'ajout correspondant à une déduction d'application.

Pour trouver la déduction d'ajout correspondant à une déduction d'application, nous montrons qu'une fois la phase 1 de traduction faite jusqu'à la déduction d'application concernée la seule possibilité de dériver une vérité est de prouver une vérité qui se calcul en vérité de même forme (même nom de fonction minmale) et où les arguments sont égaux. Par exemple si la déduction d'ajout est x ⇒ y, alors la vérité dérivée se calculera en une formule x1 ⇒ y1 où x1 = x et y1 = y.
Voir l'étude sur le sujet.

Réponse

Voir l'étude.

@todo