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