Intersection de sous-classes selon NBG

Palabra
Palabra
Modifié (January 2022) dans Fondements et Logique
Bonjour
Dans mon travail, je dois fréquemment considérer des classes propres et effectuer des manipulation élémentaires avec. Donc je travaille avec la théorie des ensembles NBG : " Neumann-Bernays-Gödel " (avec l'axiome de choix global, ou de "limitation de taille").
Je dois parfois considérer la plus petite sous-classe $Y$ d'une classe $X$ telle qu'une condition $\psi[Y]$ dans le langage de NBG (avec un prédicat $\operatorname{Set}$ et un seul type) est satisfaite, sachant que $\psi[X]$ est satisfaite. Dans les cas qui m'intéressent, je peux toujours me débrouiller pour construire $Y$ comme union d'une famille croissante de sous-classes indexée par les ordinaux. Mais je me demande s'il est aussi possible de considérer directement l'intersection des sous-classes $Z$ de $X$ satisfaisant à $\psi[Z]$. Ma question est donc: NBG prouve-t-elle l'existence de cette intersection en général ?
Les théorèmes de compréhension / spécialisation dans NBG imposent que la formule selon laquelle on "spécialise" ne quantifie que sur des ensembles, ce qui n'est pas le cas pour la formule en $y$ 'pour toute sous-classe $Z$ de $X$, si $Z$ satisfait à $\psi[Z]$ alors $y$ est dans $Z$'. En même temps, j'ai souvent été surpris par ce que des théories des ensembles en apparence peu puissantes étaient capables de prouver. J'imagine que l'obstruction principale (en plus des simples limitations de NBG) serait d'utiliser ces intersections de sous-classes (donc unions de sous-classes) pour définir la satisfaction des formules dans tous les modèles.
En dernière remarque, je m'attendrais plutôt à ce que l'existence, si elle est prouvable, le soit sans utiliser l'axiome de limitation de taille ou l'axiome du choix.

Réponses

  • Martial
    Martial
    Je ne suis pas spécialiste de NBG mais à la lecture de ton post je me pose la question bête suivante : puisqu'apparemment ton seul souci est de manipuler des classes propres, pourquoi ne travailles-tu pas directement dans Morse-Kelley ? Là, tu as le schéma de compréhension plein pot, avec possibilité de quantifier même sur les classes.
    Bon, je dis peut-être une c...rie, peut-être que cela t'embête d'utiliser une Kalashnikov pour dégommer une mouche...
  • Palabra
    Palabra
    Disons que je n'en ai pas besoin, donc tant qu'à faire je préfère travailler dans une extension conservative de ZFC, qui plus est un peu plus connue je crois que Morse-Kelley ou des trucs sympas mais un peu exotiques comme la théorie des ensembles d'Ackermann! De plus certains travaux dans mon domaine ont été faits selon NBG.

    C'est juste que j'aimerais quand-même éclairer le lecteur sur cette question, et ne pas dire une connerie en prétendant qu'on ne peut pas toujours définir ces intersections, si c'est en fait toujours possible.
  • Thierry Poma
    Thierry Poma
    Modifié (January 2022)
    Bonjour
    Analyser ceci, où l'on prendra soin de remarquer ce qui suit :
    Note that the created class only contains sets, in particular there is no class of all classes. MK is obtained by removing the "first-order" restriction in class comprehension, i.e. second-order formulas are now allowed.
    Le chat ouvrit les yeux, le soleil y entra. Le chat ferma les yeux, le soleil y resta. Voilà pourquoi le soir, quand le chat se réveille, j'aperçois dans le noir deux morceaux de soleil. (Maurice Carême).
  • Martial
    Martial
    Merci Thierry pour le lien, ça m'évitera de le chercher quand j'en aurai besoin pour NBG. Bon, faut d'abord que j'en finisse avec Russell, alors c'est pas tout à fait pour demain.
  • Palabra
    Palabra
    Merci Thierry Poma. En fait dans ce lien ils semblent dire que dans NBG on a la compréhension pour toutes les formules (du premier ordre). Ca me semble un peu douteux tout de même parce que du coup avec ça je ne vois pas ce qui empêche de contredire le théorème d'indéfinissabilité de Tarski. Bon il faut que j'en lise plus sur NBG, tout cela n'est pas très clair.
  • Martial
    Martial
    Modifié (January 2022)
    @Palabra : Dans NBG le schéma de compréhension sur les classes ne te permet de quantifier que sur les formules du 1er ordre, contenant éventuellement des paramètres du second ordre. En gros, en notant les ensembles par des minuscules et les classes par des majuscules, le schéma ne s'applique qu'aux formules du type
    $$Q_1x_1\cdots Q_nx_n \varphi(x_1,\ldots,x_n, Y_1,\ldots,Y_k),$$
    où les $Q_i$ sont des quantificateurs et $\varphi$ une formule sans quantificateurs.
    C'est pour ça qu'il n'y a pas de contradiction.
  • Palabra
    Palabra
    Oui c'est bien ce que j'ai lu ailleurs. Ok en fait c'était implicite dans le lien de Thierry Poma puisqu'ils utilisent un petit $x$ qui est donc une variable de type ensemble. Mais du coup cela laisse la question ouverte...
  • Foys
    Foys
    Modifié (January 2022)
    Sauf erreur NBG peut s'exprimer en logique du premier ordre (sans types) sur la signature  $(\in,=)$, "$Set(x)$" étant l'abréviation de $\exists y(x \in y)$.
    On abrège par "$A \subseteq B$" l'énoncé "$\forall x (x\in A \Rightarrow x \in B )$".
    Soient $\psi$ une formule à une variable libre $Y$ et $\Gamma$ une formule à une variable libre $X$ ne contenant pas $Y$.
    $\forall X\left [\left ( \psi[Y:=X] \wedge \forall Y (\psi \Rightarrow X \subseteq Y)\right ) \Rightarrow \Gamma \right ]$ signifie intuitivement que
    "la plus petite classe $Y$ telle que $\psi(Y)$ satisfait $\Gamma$".
    L'énoncé "$\exists X\left [ \psi(Y:=X) \wedge \forall Y (\psi \Rightarrow X \subseteq Y)\right ]$" signifie intuitivement qu'il existe une plus petite classe satisfaisant $\psi$.
    Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
  • Thierry Poma
    Thierry Poma
    Foys : bonsoir. J'espère que tu vas bien. Où as-tu trouvé ces quelques éléments que tu évoques et qui ne me laissent pas indifférent ? Je te remercie pour ta réponse.
    Sinon, l'on pourra étudier avec profit ceci.
    Le chat ouvrit les yeux, le soleil y entra. Le chat ferma les yeux, le soleil y resta. Voilà pourquoi le soir, quand le chat se réveille, j'aperçois dans le noir deux morceaux de soleil. (Maurice Carême).
  • Palabra
    Palabra
    Merci Foys pour ces compléments, oui on peut écrire NBG dans le langage ensembliste classique, je trouve seulement le prédicat Set pratique pour exposer notamment la convervativité au-dessus de ZFC.

    Je ne comprends pas en revanche où tu veux en venir. Pour moi le problème n'est pas de formuler "$X$ est la plus petite classe satisfaisant $\psi[Y:=X]$" dans NBG mais plutôt la question de l'existence qui ne semble pas se déduire facilement des axiomes de NBG ni des théorèmes de base, ni de la conservativité au dessus de ZFC...

    Peut-être que le dernier lien de Thierry Poma (merci!) répond à ma question (positivement) puisque je vois qu'on y considère des intersections. Encore qu'il semble s'agir d'intersections de familles de classes, ce qui ne fonctionnerait pas dans ce cas puisqu'il n'y a pas de façon de faire de la "famille des sous-classes de $X$" un objet du langage (une classe).
  • Foys
    Foys
    Modifié (January 2022)
    Bonjour
    @Palabra en fait je m'égare, j'ai inconsciemment fait qu'il suffisait de l'exprimer en formule pour prouver l'existence d'une classe (alors que non, il faudrait relativiser ladite formule à $Set$ ... ça doit être le piège classique).
    Il n'y a pas toujours de plus petite classe vérifiant une propriété donnée. Soit par exemple $E$ un ensemble et $F:= \{x\mid x\notin E\}$ sa classe complémentaire.
    Soit $F_y:= \left \{x\mid x\notin E \cup \{y\}\right \}$. Alors $F_y$ est une classe propre. Il n'existe pas de plus petite classe propre contenant $E$ puisqu'alors elle serait contenue dans $E=\bigcap_{y\in F} F_y$.
    Mais dans mon message plus haut, en gros, je montre comment construire pour toutes propriétés $\psi(.),F(.)$,une formule qui, lorsqu'il existe une plus petite classe vérifiant $\psi(.)$, signifie exactement que cette plus petite classe vérifie $F(.)$. Ladite formule existe constructivement, qu'il y ait bien une plus petite telle classe ou non.
    Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
  • Palabra
    Palabra
    Ah, génial Foys, je n'y avais pas du tout pensé!

    En fait je me rends compte que j'avais mal formulé ce que je cherchais, car je veux seulement considérer l'intersection des classes satisfaisant à $\psi$, sans forcément que cette dernière satisfasse elle-même à $\psi$ (car je le montre après).

    Donc en tout cas merci beaucoup pour vos réponses, ça va sûrement m'aider à trancher mon autre question.
  • Foys
    Foys
    Modifié (January 2022)
    Bonjour @Thierry Poma
    L'encodage de NBG en logique du premier ordre sans sortes est fait dans le livre de R.Smullyan et M.Fitting: Set Theory and the Continuum Problem (mais aussi dans le lien que tu as posté).

    Si tu es intéressé par l'expression de définitions en logique c'est un peu devenu un gros point aveugle en maths. En effet il sévit dans le monde académique une mode d'antiformalisme féroce, atteignant les logiciens et set theorists eux-mêmes et disant en gros que décrire explicitement comment les mathématiques sont formalisables/formalisées dans les systèmes de base "c'est pas bien" ou pire, que "Gödel l'aurait interdit" (alors qu'ils sont les mieux placés pour savoir que les résultats d'indécidabilité ne disent pas ça). A cause de cette mode, le mode d'emploi de la très sobre logique du premier ordre n'est jamais vraiment explicité nulle part dans les cursus ou les livres au delà d'éléments introductifs et in fine les gens se retrouvent avec sur les bras:
    1°) une production mathématique courante pléthorique,
    2°) un formalisme (logique du premier ordre sur la signature "$\{\in,=\}$"+axiomes) extrêmement dépouillé (pas de symboles de fonctions/opérations notamment, en contraste saisissant avec la pratique normale des mathématiques où les introductions de définitions et de formules pour dénoter des objets se produisent à chaque ligne).
    3°) un slogan ("la quasi-totalité des maths s'exprime dans la théorie des ensembles/ZF(C)/le jeu d'axiomes que vous voudrez" )
    et RIEN pour faire le lien entre ces trois points et notamment comment traduire dans 2°)
    les propos tenus dans le cadre de 1°).

    ######################
    Je vais essayer d'apporter des éléments de réponse à ta question:

    On se place en logique du premier ordre sur une signature quelconque avec égalité $=$ (et la règle de Leibniz). On emploie mettons la déduction naturelle comme système de preuve

    Soit $P$ une formule, on note $\exists ! xP$ l'énoncé $(\exists x P)\wedge \forall y \forall z ((P[x:=y]\wedge P[x:=z] ) \Rightarrow y = z)$
    (qui se lit également "il existe un $x$ unique tel que $P$" et autres variantes).

    Soit $\Gamma$ un ensemble de formules ne contenant pas $x$ comme variable libre. Alors
    Si $\Gamma \vdash \exists !xP$ alors pour toute formule $G$, il existe une formule $G'$ ne contenant pas $x$ parmi ses variables libres, et telle que $\Gamma \cup \{P\} \vdash G\Leftrightarrow G'$.
    D'autre part (c'est l'élimination du quantificateur existentiel qui l'entraîne), si $\Gamma \cup \{P\}\vdash G'$ alors $\Gamma \vdash G'$.


    Pour la formule $G'$ on peut prendre  $G':=\forall x \left (P \Rightarrow G \right )$. La preuve des affirmations ci-dessus est un exo de déduction naturelle sans prise d'initiative.
    On note ici $G[x:= Def_x(P)]$ cette formule $G'$. Si $H$ est une autre formule où ne figure pas $x$ (on pourra toujours renommer $x$ dans $P$ au préalable si nécessaire), et $y$ une variable, on notera aussi $H[y:=Def_x(P)]:=\forall x(P \Rightarrow H[y:=x] $).

    L'intérêt de cette construction est que $[y:=Def_x(P)]$ se comporte comme une substitution explicite:
    en effet, étant données des formules $A,B,C$ et une lettre $z\neq y$ non libre dans $\Gamma$ et $P$, on a (sous les hypothèses de $\Gamma\cup \{P \}$ ) les équivalences entre:
    (i) $ \left ( A \Rightarrow B\right )[y:=Def_x(P)]$, $(A\Rightarrow B )[y:=x] = A[y:=x]\Rightarrow B[y:=x]$, et $A[y:=Def_x(P)]\Rightarrow B[y:=Def_x(P)]$
    (ii) lorsque $y$ n'est pas libre dans $A$ (et donc que $A=A[y:=x]$ à alpha-équivalence près, ce qui arrive notamment quand $A=\perp$),  $A[y:=Def_x(P)]$ et $A$ 
    (iii) $\left (\forall z C \right )[y:=Def_x(P)]$, $(\forall z C)[y:=x]=\forall z \left (C[y:=x] \right )$ et $\forall z\left ( C[y:=Def_x(P)]\right )=\forall z\left (\forall x (C[y:=x]\Rightarrow P) \right )$.
    Toutes les formules pouvant s'exprimer avec les connecteurs $\Rightarrow, \forall, \perp$, on peut appliquer ce qui précède à n'importe quelle formule (du reste le mécanisme marche pour n'importe quels connecteurs).

    Ainsi on a un moyen simple d'exprimer des formules disant que "l'unique objet tel que ceci vérifie cela", par exemple soit $\mathfrak P(x,y):=\forall z(z\in x \Leftrightarrow z \subseteq y)$ ("$x$ est l'ensemble des parties de $y$") et, étant donné$\varphi$ une fonction $\mathfrak F(a,b):=  (a,b)\in \varphi$, l'énoncé $\varphi(t)\in \mathcal P(y)$ n'est autre que $(v \in w)[v:=Def_s(\mathfrak F (t,s))][w:=Def_x\left ( \mathfrak P(x,y)\right)]$.

    On obtient une formula à rallonge $$\forall x \left (\forall z(z\in x \Leftrightarrow z \subseteq y) \Rightarrow \forall s  \left ((t,s)\in \varphi \Rightarrow s \in x \right ) \right )$$
    La notation couple est elle aussi éliminable (il y a un énoncé $\mathfrak C(p,q,r)$ qui signifie "$r$ est le couple formé par $p$ et $q$").

    J'ai trouvé la formule du post plus haut essentiellement grâce à cette idée.

    Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
  • Thierry Poma
    Thierry Poma
    Modifié (January 2022)
    Bonsoir Foys
    Je te remercie vraiment beaucoup d'avoir pris de ton temps pour rédiger ton dernier message que je lirai à tête reposée, avec, à côté, l'ouvrage que tu cites et que je possède.
    Amitiés
    Thierry
    Le chat ouvrit les yeux, le soleil y entra. Le chat ferma les yeux, le soleil y resta. Voilà pourquoi le soir, quand le chat se réveille, j'aperçois dans le noir deux morceaux de soleil. (Maurice Carême).
Connectez-vous ou Inscrivez-vous pour répondre.

Bonjour!

Pour participer au forum, cliquer sur l'un des boutons :

Connexion S'inscrire

Catégories

In this Discussion

Qui est en ligne 4

Amadou +3 Invités