A mon sens, il n'y a pas vraiment de "théorie naïve de ZF", mais,
- Soit une "théorie naïve des ensembles" qui, si on gratte un tout petit peut est franchement contradictoire.
- Soit la "vrai" théorie axiomatique de Zermelo-Franckel qui est quand même extrêmement difficile à comprendre.
Donc il me semble que le choix pédagogique quasi obligatoire, c'est de rester sur du "naïf" et... de pas trop gratter...
Concernant les quantificateurs, dans "la vraie" théorie (de la logique), on n'a nul besoin de leur donner "du sens" : ce sont uniquement des symboles (au même sens que les lettres d'un alphabet) et il y a un certain nombre de règles "bètes et méchantes" décrivant quels sont les "phrases" (i.e. suites de symboles) qui sont acceptables dans le langage, c'est à dire quels sont les suites de symboles qui vont être appelés des "propositions" et quels sont les suites de symboles qui ne sont pas des propositions par exemple, "
", est une "phrase" du langage mathématique, mais ce n'est pas une proposition.
Au sens naïf du truc, on résume ça en disant que ce que j'ai écrit, "ça ne veut rien dire", mais de façon théorique, on s'exprime en disant que "ça ne respecte pas telle ou telle propriété donc ça ne vérifie pas la définition qui caractérise les "proposition" parmi les phrases quelconques"
A mon avis, il ne faut pas que tu vois le cours de logique que tu suis comme étant rigoureux (il ne l'est pas...), mais comme un cours qui est là pour te permettre d'écrire plus rigoureusement qu'au Lycée les définitions des objets manipulés, pour écrire sans hésiter la négation d'une proposition, pour comprendre de façon un peu "carré" ce qu'est un raisonnement par l'absurde, une contraposée, pour éventuellement mieux comprendre la différence entre une implication et une équivalence, etc...