Lazi

4 Retrouver la déduction d'ajout

Contexte

Pour les mots clés, la traduction des déductions d'application utilise souvent des arguments de la déduction d'ajout correspondante.

  • prouver qu'il y a une déduction d'ajout correspondante
  • déterminer comment la retrouver.

Question

Comment prouver qu'il y a une déduction d'ajout correspondant à une déduction d'application ? Et comment la trouver ?

Étude

Remarques

  • Entre la déduction d'ajout et la déduction d'application, le mot clé peut être remplacé par une variable (grace à un ∀) pour raisonner sur la formule.
  • La formule n'a pas de sens en dehors de la déduction d'ajout et d'application, mais on peut faire des remplacements par égalité. Par exemple forAll f = if 1b forAll exists f
  • On peut avoir plusieurs déduction d'ajout équivalentes pour une seule déduction d'application.
  • On peut supposer que la preuve précédente ne contient plus de déduction d'applications (car déjà traduites). C'est donc, du point de vue des modifications de formules par égalité, du lazi.0.0

Idée de solution

On peut généraliser le théorème "vérité et égalité" pour montrer que la vérité utilisée par la déduction d'application ne peut provenir que:

  • soit directement de la déduction d'ajout
  • soit du x de la déduction "égalité et vérité"

Ainsi on peut remonter à une déduction d'ajout et prouver qu'il y a égalité entre la vérité produite par la déduction d'ajout et celle utilisée par la déduction d'application. C'est en même temps la preuve qu'il y a une déduction d'ajout correspondante.

Réponse

@todo