Lazi

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 ⇒ f121 p où f121 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