Lazi

Traduction sans hypothèse

Contexte

La traduction de Lazi.1 passe par la recherche de la déduction d'ajout correspondant à la déduction d'application. Mais cela peut poser des problèmes si :

  • on est sous une hypothèse absurde, car alors on pourrait avoir une vérité Lazi.1 sans déduction d'ajout
  • on est sous une hypothèse qui est une vérité Lazi.1, car alors la déduction d'ajout peut être inaccessible.

Question

Est-il possible de ne faire la traduction que sans hypothèse ?

Étude

Il y a des règles Lazi.0 contenant des hypothèses et des sous-preuves, mais ce sont des règles traduisibles, il faudrait donc les traduire en même temps que Lazi.1.

Traductions des règles Lazi.0 à hypothèse et sous-preuve

On ne peut traduire les déductions provenant de ces règles que si on se trouve dans une preuve sans hypothèse.

Réponse