Lazi.1 et les formules infinies

Contexte

Pour que les règles sur ⇒ soient valides, il faut ajouter des conditions, cela peut se faire en autorisant dans la règle que les formules ne contenant qu'un nombre fini de ⇒.
Pour le ∨, un problème se pose avec les formules en contenant une infinité, par exemple comment montrer que ⊥ ∨ ... ∨ ⊥ déduis ⊥ ?

Question

Doit-on poser des contraintes sur les formules Lazi.1 dans les règles Lazi.1, de sorte d'éviter la récurrence sur des formules purement Lazi.1 ?

Étude

Interdire les ∨ infinis est-il gênant ?

Comparaison avec la théorie des ensembles

L'axiome de la réunion permet de créer une union d'ensembles (c'est à dire une expression "∨" infinie). J'ai l'impression que l'on peut utiliser une telle construction en Lazi.1, et donc il n'y aurait pas besoin d'expression "∨" infinie.

Pour l'expression de =c

On peut toujours définir =c

Réponse

@todo