Lazi

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