Lazi

Liens entre les déductions d'ajout et d'application

Contexte

Pour la traduction des extensions des quantificateurs et imply, on aura besoin d'informations de la déduction d'ajout correspondant à la déductions d'application.

Question

Quels sont les théorèmes à démontrer pour prouver la validité et traduire.

Étude

Quoi traduire

On ne peut traduire que les preuves :

  • sans condition : car une condition peut oblitérer l'accès à une déduction d'ajout, mais aussi parce que cela pourrait permettre de déduire des déducitons d'application sans qu'il y ait de déduction d'ajout correspondante.
  • où l'objet de la preuve ne contient pas les mots clés dont on traduit les extensions.

Ce qu'il faut prouver

  • Généraliser le théorème "toute vérité lazi.a.0 se calcule une égalité" par le théorème "toute vérité lazi.0.0 + ajout"| fait | 2019
  • Prouver que l'on puisse extraire les preuves d"égalité des argument à partir de la preuve d'égalité entre formules ayant un mot clé ajout : théorème de preuve d'égalité sur les arguments. | fait | 2019
  • À partir de la preuve précédante, extraire une méthode de calcul de ces preuves. Nécéssaire pour la traduction.| à faire | 2019
  • Prouver la traductabilité des règles de déduction ajoutées à lazi.0.0 pour construire lazi.1.0. | à faire | 2019
  • Si on a dans une preuve une déduction d'application, alors c'est qu'il y a une déduction d'ajout qui prouve une vérité égale.| à faire | 2019
  • Une certaine méthode permet de produire la preuve de l'égalité des arguments entre la vérité produite par une déduction d'ajout et une vérité dérivée de cette formule (car cette vérité peut être utilisée pour la déduction d'application et il faut prouver les liens entre ces deux vérités).| à faire | 2019

Réponse

@todo