Finitude de la traduction de imply par tr1

Contexte

Voir la page parent. Nous sommes dans le contexte de chercher à prouver que tr1 produit des preuves finies. tr1 pourrait boucler car il reprend des sous-preuves antérieures. Voir aussi les déductions pour imply.

Question

Dans le cas de la traduction de la déduction d'application de "imply", peut-il en résulter une preuve infinie ?

Étude

Soit q la preuve de x ⇒ y de la déduction d'ajout correspondante. Si nous montrons que pour traduire q,

Par construction, tr1 a déjà traduit toutes les déductions d'applications jusqu'à celle en cours de traduction. Donc dans la preuve déjà traduite par tr1, il ne peut y avoir de déduction d'application.
Si nous montrons que la vérité x ⇒ y ne peut être utilisée pour déduire x,

Soit q la preuve de x ⇒ y. Nous allons montrer que q peut être traduite dans la preuve générale où la déduction d'ajout de x ⇒ y est supprimée, cette preuve étant plus courte, on pourra utiliser la récurrence pour prouver la validité.

Réponse

@todo