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