Supprimer la règle d'extension lazi.1.0

Contexte

Cette règle extensionT semble inutile, elle permetrait de déduire avec moins de calculs des vérités venant de preuves réalisées dans des extensions, mais faudrait-il encore que l'on n'ai pas à vérifier toutes les conditions nà chaque fois.

Question

Faut-il supprimer cette règle ?

Étude

Soit M1 une extension de M0.
Supposons que dans M1 on crée une extension M2.
On aimerait avoir dans M1 une vérité ∀p; dom p ⇒ f₁₂₁ p où f₁₂₁ traduit la conclusion de la preuve p.
où dom p est une condition éventuellement plus restrictive que "être une preuve en M2 sans condition" et où f p traduit la conclusion de la preuve p.

Si M1 ne se connait pas lui-même, c'est impossible. Mais il est possible qu'il ait une connaissance de lui-même en définissant une variable spéciale et une règle M0, mais c'est tordu.
Mais M0 connait M1 et M2. M0 peut montrer ∀p; dom p ⇒ tr p est une preuve M1.

Réponse

oui