Mot "type" dans la théorie des ensembles — Les-mathematiques.net The most powerful custom community solution in the world

Mot "type" dans la théorie des ensembles

Bonjour,

Quelqu'un peut m'expliquer ce qui est entendu par le mot "type" dans le 1er chapitre du livre de P. Dehornoy : https://www.lmno.cnrs.fr/archives/dehornoy/Surveys/DehornoyChap1.pdf ?

Je viens de le survoler, et cela devient très obscur à partir de l'"ébauche d'une théorie des ensembles" (paragraphe 3) !
J'ai l'impression que, faute de pouvoir donner une définition au mot "ensemble" (au sens mathématique), on introduit le mot "type", qui n'est pas non plus défini (au sens mathématique), et qui est utilisé dans toute la suite du chapitre, pour introduire les premiers axiomes de la théorie des ensembles.

Ce n'est pas tout : les mots "fonction", "élément", "propriété", "vrai", "faux", "axiome", "existence", "unicité", "définir", ... que sais-je encore, sont introduits de la même façon.

Le paradoxe de Berry m'interpelle, vu déjà qu'on n'a pas "défini" ce que veut dire "définir", et même si cela étant, la phrase "$n$ est un entier définissable par une phrase française d'au plus cent caractères" est très ambigüe : si on trouve une phrase de 105 caractères par exemple qui définit un entier $n$, comment savoir si on peut la réduire ou non ; il me semble qu'on fait appel à notre logique commune (savoir si on peut la réduire ou non) pour essayer de s'en affranchir (trouver des ensembles qui n'existent pas). Il me semble que cela ne peut donner rien de bon.

Puis "signature" qui est une "liste" (définition ?), puis une "suite" (définition ?), les deux mots ne semblant pas recouvrir la même notion, une "liste" s'apparentant davantage (il me semble) à la notion d' "ensembles" où l'idée d'ordre n'existe pas.

Puis "symbole", "variables", opérations", "relations" d'une "signature", etc...

Peut-être en comprenant ce que veut dire précisément le mot "type", tout s'éclairera. Ainsi que savoir que, à défaut d'une définition, les mots employés ont le sens que leur donne la langue française habituellement (ma devise est : "on ne dit jamais l'évidence", parce qu'elle est évidente justement). Sauf que "type", "signature", "propriété", etc... ont un sens très ambigu, difficilement transposable en mathématiques, sans une définition précise.

Merci d'avance.

Réponses

  • Bonjour Julia,

    Ici (car ailleurs il peut avoir un autre sens), ce n'est pas un mot "mathématique" mais français, Dehornoy est clair dès le paragraphe 2 :
    Les mathématiques étudient des objets appartenant à des types variés : entiers, réels, points,fonctions, etc.
    L'intérêt du "paradoxe de Berry" est de montrer la nécessité d'une définition mathématique, la définition naïve ne suffisant pas (amène à des contradictions)

    Pour la signature, là encore les mots suites, listes, etc sont à prendre dans leur sens français.

    Les autres mots que vous citez sont du vocabulaire de la logique à voir avant la théorie des ensembles.

    Quant à type, il est utilisé ici dans un sens que l'on peut formaliser à l'aide d'une relation unaire (il a aussi d'autres significations, que vous verrez peut-être plus tard), par exemple en géométrie on manipule des objets de plusieurs types : points, droites, plans, d'ailleurs Hilbert disait qu'on aurait pu tout aussi bien les nommer tables, chaises et rond de bière sans rien changer à la géométrie. La très grosse majorité des théories sont mono-type.

    Il me semble que vous êtes dans une phase où vous voudriez que tout soit parfaitement défini, malheureusement écrire un dictionnaire où chaque mot est défini exclusivement à l'aide des mots précédents est impossible.

    De plus si je vous dit que l'appartenance est une relation entre deux "objets" pensez-vous qu'il soit nécessaire d'avoir défini l'arithmétique avant ?
  • Merci Médiat. Si je comprends bien, le mot "type" est à prendre au sens français, sans définition mathématique ? Dès lors, des questions se posent : est-ce qu'un même objet (on comprend plus ou moins ce que cela veut dire : $3$, un point, ...) peut avoir différents types ? est-ce que les types forment une hiérarchie (par exemple, dans le type "entier", il y a les entiers naturels, et les relatifs, ou dans le type droite, il y a les droites vectorielles, affines, projectives, dans un espace de dimension 2, 3 , ..., n, infinie) ? etc...

    Il me semble qu'il pourrait être dit une fois pour toutes, qu'on admet en général le consensus sur la signification des mots apportée par la langue française, qui bien sûr se définissent les uns et les autres, quitte à préciser si ambiguïté, et quand on passe dans le domaine mathématiques, les axiomes sont énoncés avec des mots (ou des formules) compréhensibles par notre sens commun sans ambiguïté (toujours le consensus).

    Pour moi, les mathématiques sont basées sur le langage. Je ne comprends pas qu'une théorie soit développée sur un mot qui n'est pas défini mathématiquement, au moins par une phrase compréhensible par notre sens commun. Des exemples ne suffisent pas, d'autant plus s'ils sont ambigus.

    Ou bien, je n'ai pas la maturité suffisante pour comprendre ce passage, il faut déjà connaître la théorie des ensembles, ou bien la logique si je comprends bien, pour comprendre cette approche, d'abord naïve de la théorie des ensembles, qui ne donne pas satisfaction (dixit l'auteur), alors on passe sur le système de Cantor en utilisant les mêmes mots (type, ensemble d'objets d'un certain type... ?), qui lui non plus ne donne pas satisfaction (à cause du paradoxe de Berry), toujours en utilisant les mêmes mots, pour aboutir à des axiomes qui les utilisent encore.

    Le paradoxe, c'est que le paradoxe de Berry montre la nécessité d'une définition mathématique des mots qu'on utilise de la langue française (s'ils sont ambigus ; par exemple le mot "$2$" tout le monde voit ce que cela veut dire), et que ce principe n'est pas appliqué au tout début de cette théorie avec le mot "type", qui lui est plus qu'ambigu dans la langue française !
  • Je ne comprends pas qu'une théorie soit développée sur un mot qui n'est pas défini mathématiquement,

    Mais ce n'est pas les cas ; la théorie des groupes ou celle des ensembles ou n'importe quelle autre sont écrite à l'aide de formules totalement issues de la logique (à voir avant comme je vous le disais), et utilisant le langage spécifique de la théorie sans un mot de français.


    Si on définissait ZF sans un mot de français, mais exclusivement avec les axiomes, cela ferait de très petits bouquins, que peu de personnes comprendaient (même si à un moment ou un autre on doit en passer par là)
  • Une théorie énoncée sans un mot de français doit être illisible. Je plains ceux qui s'amusent à faire cela, ou qui se contraignent ensuite à lire un tel texte.

    Pour la théorie des groupes : https://fr.wikipedia.org/wiki/Groupe_(mathématiques), heureusement il y a quelques mots ... Maintenant, qu'on puisse le faire sans mot, pourquoi pas, mais bof.

    Euclide a utilisé des mots pour énoncer les axiomes d'Euclide. Il me semble qu'un texte mathématique énoncé sans mots est une théorisation sans intérêt.

    Par contre, des démonstrations sans un mot, où tout est formalisé dans le moindre détail, cela doit rallonger les textes ?

    Bon, je ne peux pas comprendre ce passage sans avoir vu la logique avant. Je laisse tomber.
  • Une théorie énoncée sans un mot de français doit être illisible
    Il y a 2 aspects à prendre en compte :

    1) La communnication, et sans un mot de français, on court à l'échec
    2) Les mathématiques, et là l'utilisation d'un langage naturel est la porte ouverte aux ambigüités (donc aux erreurs)
  • Mais si j'ai bien compris, on peut prendre des mots issus de la langue française, et avec le vocabulaire, les codes et les formules de la logique (je n'y connais rien), bâtir une théorie où plus un seul mot n'est employé, écrit uniquement dans le formalisme de la logique, donc une théorie qui pourrait n'avoir aucun sens intuitif. Je ne vois pas l'intérêt.

    C'est comme si on voulait s'affranchir de notre condition d'être humain, pour essayer de raisonner comme des extra-terrestres. Il me semble que cette tentative est vouée à l'échec. Comment pourrait-on avoir cette certitude qu'on s'est bien affranchi de cette condition ? Par exemple, puisque notre condition d'être humain fait que nous sommes des êtres bornés, comment comprendre l'infini ?

    Je m'arrête là, on tombe dans le débat philosophique qui ne m'intéresse pas.
  • une théorie qui pourrait n'avoir aucun sens intuitif. Je ne vois pas l'intérêt.
    C'est ce que je vous disais : 2 aspects !

    A partir de l'intuition, et par un processus d'abstraction, on construit une théorie, et là, seulement là on fait des mathématiques.
  • D'accord avec toi pour ton message intermédiaire. Il faut donc un mélange des deux. Mais il me semble qu'au bout du bout, c'est notre raisonnement logique (avec des mots français) qui va l'emporter sur le formalisme mathématique. Mais encore une fois, je dis ça, mais je ne connais rien en logique, la logique et son langage peut permettre de lever directement les ambiguïtés.
  • Ok, on ne s'amuse pas à construire une théorie qui n'aurait aucun sens intuitif.
  • @Julia : ne te prends pas trop la tête sur ce chapitre 1. Je n'ai jamais compris pourquoi Patrick s'est senti obligé de perdre de la place pour nous raconter toutes ces histoires, ni pourquoi il nous saoule avec le "type" ensemble. Pour moi l'unique intérêt de ce chapitre est de prouver l'insuffisance (voire l'inconsistance) de la théorie naïve (paradoxe de Berry, je ne me rappelle plus s'il parle du paradoxe de Russell), mais j'ai l'impression qu'il s'y prend mal.

    Fondamentalement, tout ce qui est écrit dans le chapitre 1 (Cantor-Bernstein, bijection entre $\mathbb{N}$ et $\mathbb{N}^2$ etc), tu le sais. A part peut-être la partie consacrée aux algèbres de Boole, mais de toutes façons il n'en parle plus après.
    Tu peux donc développer 2 stratégies :
    1) Soit tu es pressée de te familiariser avec la théorie basique des ensembles, auquel cas tu commences par lire les chapitres 2 à 5, qui n'utilisent pour ainsi dire pas de logique.
    2) Soit tu désires acquérir d'abord les bases de la logique, et tu commences par les chapitres 6 et 7, qui sont largement abordables, pour revenir ensuite au chapitre 2.
  • Ok, on ne s'amuse pas à construire une théorie qui n'aurait aucun sens intuitif.
    Je n'ai aucune référence pour ce que j'écris ci-dessous.

    Les mathématiciens Russes auraient généré aléatoirement des théories, mais cela n'aurait rien donné.

    C'est une des beautés des mathématiques que de s’appuyer sur l'intuition pour mieux s'en affranchir.
  • Bonjour

    Définition provisoire : Considérons le type de base principal $\mathbf{Ens}$ (car ici, l'on ne considère que des théories des univers constitués d'ensembles)(**). L'on considère une liste $T_0$ constituée de types de bases auxiliaires, à l'exception du type de base principal. L'on définit la liste $T$ des types au moyen de la grammaire\[T=\mathbf{Ens}|T_0|\mathbf{Ens}_T\]Exemples : voici quelques types que l'on peut concevoir à partir de cette grammaire, en ne considérant que la liste réduite suivante, liste que l'on peut enrichir\[T_0=\mathbf{Ent}|\mathbf{Bool}|\mathbf{Fonc}|\mathbf{Point}|\mathbf{Droite}\]
    1. Si l'on considère la séquence $T\rightarrow\mathbf{Ent}$, l'on obtient le type "entier" $\mathbf{Ent}$.
    2. Si l'on considère la séquence $T\rightarrow\mathbf{Ens}_T|T\rightarrow\mathbf{Fonc}$, l'on obtient le type $\mathbf{Ens}_{\mathbf{Fonc}}$, i.e. le type $\mathbf{Ens}$ dont les objets sont de type "fonction" $\mathbf{Fonc}$.
    3. Si l'on considère la séquence $T\rightarrow\mathbf{Ens}_T|T\rightarrow\mathbf{Ens}_T|T\rightarrow\mathbf{Droite}$, l'on obtient le type $\mathbf{Ens}_{\mathbf{Ens}_{\mathbf{Droite}}}$.

    (**) Dans un autre univers, l'on aurait pu avoir les types de bases principaux $\mathbf{Ens}$ et $\mathbf{Cls}$.
  • Merci mille fois Martial. Tu me rassures. Ma stratégie va être d'aller sur un autre livre, par exemple le Krivine, qui m'a l'air plus simple. Ce 1er chapitre m'a fait me méfier du Dehornoy. Un mot sur son utilisation, et son utilité (qui m'est passée complètement au-dessus de la tête), aurait été bien utile (il figure peut-être en préface de ce livre, que je n'ai pas).
  • Je suis un enfant de Krivine et j'ai commencé ZF dans son livre (Edition 1972) je ne vais pas en dire du mal; mais le Dehornoy ne mérite pas d'être jeté aussi vite.
  • Merci TP. Ton message a le mérite de me donner un aperçu en levant un coin du voile.
  • Médiat, en maths, tout le problème est de trouver le bon texte au bon moment. Je garde le Dehornoy pour après éventuellement.
  • @JP : je n'ai rien fait de plus que d'utiliser un concept fondamental de la théorie des compilateurs, pour le transposer en théories des ensembles ou théorie des univers. Je pense que dans le Dehornoy, il doit y avoir une allusion à la programmation et à la typification des variables utilisées. En C++, l'on se doit de typer un symbole de variable qui va jouer un certain rôle dans le programme, même si le C++ permet de changer ce rôle en cours d'exécution (opérateur de cast). Cela dit, je peux écrire $\forall\,\alpha:\mathbf{Ord}$, pour indiquer que mon scopage universel s'opère sur le symbole de variable $\alpha$ dont le type affecté est "ordinal" ; je ne retiens que cela et rien d'autres. Selon Krivine, qui écrit $\forall\alpha\in{}On$, le scopage universel porte toujours sur le symbole de variable $\alpha$ restreint aux seuls points de la partie $On$ au sens intuitif de l'univers $\mathscr{U}$.

    Contrairement à ce que tu peux penser, le Krivine, qui est excellent, est de lecture difficile. Vas-y !
  • Julia Paule a écrit:
    Ma stratégie va être d'aller sur un autre livre, par exemple le Krivine, qui m'a l'air plus simple.

    J'ai les deux et j'ai lu une partie des deux sans en finir aucun. Je crois pouvoir dire sans me tromper que le Krivine est plus hard.

    Dehornoy commence depuis le début du début, lorsque tout n'est pas encore formalisé de la façon qu'on connait actuellement, pour montrer les difficultés rencontrées à l'époque où la théorie des ensemble naissait. Il a une démarche qui "justifie" l'introduction de certains axiomes. Mais à la fin on retrouve le ZFC qu'on connait et il montre comment on peut construire la majorité des objets mathématique que l'on manipule à l'aide de la théorie des ensembles.

    La critique que je ferais au Dehornoy est qu'il est plus difficilement consultable. Si on cherche une définition par exemple c'est beaucoup plus difficile car justement il y a une première partie où il montre d'autres piste qu'il écarte par la suite.
  • Thierry Poma a écrit:
    Contrairement à ce que tu peux penser, le Krivine, qui est excellent, est de lecture difficile.
    Plus que le Dehornoy (en tous cas la version 72)
  • @Julia : bien entendu tu fais ce que tu veux, mais perso je ne crois pas que ce soit une bonne idée de lâcher Dehornoy pour Krivine. J'ai le Krivine depuis des siècles, et je n'ai réussi à en tirer profit qu'une fois que j'avais acquis un peu de bouteille en théorie des ensembles. Je pense qu'il est fait pour des gens qui ont déjà des bases solides en TDE, et qui veulent approfondir. Pour info, le dernier mec qui m'a dit avoir lu Krivine en sup et avoir à peu près compris le livre a fini 1er à Ulm.

    Tandis que Dehornoy fait comme moi (enfin, c'est plutôt moi qui fait comme lui) : il te mène par la main en partant de presque rien et en allant quand même assez loin. Il y a peut-être quelques écueils sur la route, comme le chapitre 1 qui n'est pas sa meilleure réussite. (Le chapitre 12 sur le forcing laisse à désirer aussi, mais on n'en est pas là). Mais globalement c'est un bon livre, très pédagogue.
  • Merci beaucoup à vous.

    Martial, ok pour le Dehornoy à partir du chapitre 2 ! Il semble qu'il n'utilise plus le vocabulaire de la logique (type, ...). J'ai imprimé le 1er chapitre du Krivine. Bah je verrai. En fait, j'ai terminé le Halmos qui m'a donné un bon aperçu de la théorie des ensembles. Il faut que je passe maintenant aux catégories.

    TP, ah d'accord, ce vocabulaire est issu de la programmation, avec des déclarations de variables selon des types.

    Dans le Krivine, au moins le début est compréhensible. Dans le Dehornoy, le chapitre 1 démarre plutôt bien, bien que je trouve ses exemples inutilement difficiles (par exemple, l'intérêt des ensembles), puis il pose des questions auxquelles il ne répond pas, il répond à d'autres, il démontre des premières propositions (pourquoi celles-là et pas d'autres ?), ensuite il passe aux algèbres de Boole, intéressant mais pourquoi ici, quel est l'intérêt au début de la théorie des ensembles ?

    EDIT : ah si, c'est pour dire qu'on fait rapidement le tour de la théorie des ensembles finis, et que la théorie des ensembles trouve son intérêt principalement dans les ensembles infinis. Mais bon, une phrase aurait suffit.

    Bref, le Dehornoy au chapitre 1, on ne sait pas ce qu'il fait.
  • Martial, ton chapitre 0, que j'ai lu entièrement est lui au moins, compréhensible et bien fait. Si je peux me permettre, j'y ai relevé une petite lacune (idée que j'avais lue en logique et qui m'a beaucoup aidée), à savoir que quand on écrit une proposition, sans plus de précisions, on suppose qu'elle est vraie ; ou bien, on peut appuyer en précisant : cette proposition (ou cette assertion) est vraie, ou elle est fausse, mais si on ne précise pas en l'écrivant, cela veut dire qu'elle est vraie. Cela parait évident, mais sans cela, on ne comprend pas pourquoi on énonce parfois des propositions sans rien préciser, et parfois on précise leur véracité.
  • Tu ne peux pas juger le Dehornoy sur son chapitre 1, qui est une mise en bouche informelle tout au plus et qui est essentiellement indépendant du reste. Si tu te lances dans le Krivine, je pense que tu vas vite renoncer, il est vraiment difficile d'accès. Le Dehornoy est, lui, d'une clarté rare étant donné le sujet abordé.
  • Julia Paule a écrit:
    à savoir que quand on écrit une proposition, sans plus de précisions, on suppose qu'elle est vraie
    L'adjectif "vrai" n'a aucun sens absolu en mathématiques. C'est le théorème de Tarski.
  • @Poirot : 100% d'accord avec toi.

    @Foys : ne va pas semer le trouble dans l'esprit de Julia. Le théorème d'indéfinissabilité de la vérité n'apparaît qu'au Chapitre 8 du Dehornoy, Julia a largement le temps de s'y préparer psychologiquement.
  • Martial a écrit:
    @Foys : ne va pas semer le trouble dans l'esprit de Julia. Le théorème d'indéfinissabilité de la vérité n'apparaît qu'au Chapitre 8 du Dehornoy
    C'est un résultat technique certes mais il dit déjà pourquoi certaines approches ne pourront pas fonctionner. On trouve de plus des versions vulgarisées correctes de ce théorème dans les bouquins de Smullyan (son intérêt et son champ d'application dépassent le cadre de la théorie des ensembles).

    Il est important que les gens comprennent qu'une preuve mathématique est un objet syntaxique (c'est littéralement une suite de symboles satisfaisant certains critères vérifiables par une machine), et non pas sémantique (alors que la notion de vérité l'est).

    Il n'y a en particulier aucune référence à une quelconque notion de vérité dans la définition de ce qu'est une preuve (sauf digression réthorique pour faciliter la lecture).
  • Moi, ce que j’aime bien dans les Disquisitiones Arithmeticae, c’est que le grand Gauss éclaire chacune de ses idées nouvelles au moyen d’un exemple numérique.
    C’est une façon de procéder qui me semble proscrite aujourd’hui : Si un énoncé est clair, il n’y a pas besoin d’exemple !
    Les temps changent. En mieux ou en moins bien.
  • Je ne sais pas où tu es allé chercher ça, mais les exemples sont tout aussi important aujourd'hui qu'hier.
  • @Foys : je ne pense pas que la question de la vérité soit vraiment un problème. Dans mon livre le théorème de Tarski n'apparaît qu'au chapitre 15, et encore je l'ai rajouté a posteriori quand je me suis rendu compte que j'en avais besoin pour les grands cardinaux. On peut très bien, dans un premier temps, démontrer des choses très intéressantes en théorie basique des ensembles sans se poser de questions métaphysiques sur qu'est-ce que c'est exactement que la vérité.

    Mais je comprends ton point de vue : au vu du fil que tu viens de créer sur "qu'est-ce qu'une démonstration ?" j'en déduis que tu es féru de syntaxe, ce qui n'est pas mon cas. J'en parle, certes, mais seulement quand j'y suis obligé.
  • Martial a écrit:
    j'en déduis que tu es féru de syntaxe
    Je pense que c'est plus simple. Après ce qui est simple ou non dépend des gens évidemment.
    Et puis la théorie des ensembles est (sémantiquement) simple en surface, puis on s'aperçoit qu'il y a des univers qui en contiennent d'autres, comme classes voire carrément comme ensembles (les conversations ensemblistes pros parlent beaucoup de ça j'ai l'impression) et si on ne sait pas sur quel plan de méta-langage se placer (donc on ne peut faire l'économie de la syntaxe finalement ;-)) ça devient assez vite incompréhensible.
  • @Julia : j'ai lu un peu plus haut que tu regrettais de ne pas posséder la préface du livre de Dehornoy. En fouillant dans mon pc je me suis aperçu que je l'avais... et de façon tout à fait légale : elle était en libre téléchargement sur amazon quelques semaines avant la sortir du livre, en même temps, je crois, que le chapitre 1. C'était un "aperçu" offert par les éditions Calvage & Mounet.

    La voici donc.
  • J'aurais évidemment préféré joindre la préface de la deuxième édition du livre, car à la fin de ladite préface il me remercie chaleureusement, ainsi qu'un autre membre du forum dont je tairai le pseudo, oeuf corse... Mais ça, je n'ai pas le droit.
  • Merci Martial. Je cite un passage de la préface du livre :

    "Dans la partie A (chapitres I à V), on expose la théorie élémentaire
    des ensembles sans supposer aucun prérequis, en particulier de
    logique."

    Hum.
  • C'est complètement vrai. J'ai la sensation que tu y mets de la mauvaise volonté. Tu voudrais qu'on te serve le cours parfait sur un plateau. On te dit que tu ne trouveras pas plus clair que Dehornoy. Si son livre ne te convient pas, on ne peut rien pour toi.
  • Poirot, pas du tout, je n'y mets pas de la mauvaise volonté. Je parle du chapitre I uniquement (je n'ai pas lu les autres), qui est englobé dans la partie A (chapitres I à V), au cas où tu ne l'aurais pas remarqué.

    En fait, je m'en fous, je suis passée à autre chose, je ne comprends pas simplement pas comment on ose dire qu'il ne faut aucun prérequis pour lire ce chapitre ; ou plutôt si je le comprends, on est tellement aveuglé par ses connaissances approfondies dans le domaine qu'on n'a plus la capacité suffisante pour se mettre à la portée d'un débutant de la matière.
  • @Julia : Poirot a raison. Pour simplifier on va dire que le chapitre 1 est une espèce d'overview de la partie A, voire du livre tout entier, c'est peut-être ça qui le rend un peu chelou. Mais je te promets qu'il n'y a absolument pas besoin de connaître la logique pour lire les chapitres 2 à 5.
  • Bon alors, juste par curiosité, expliquez-moi la notion de "type" en mathématiques : http://www.les-mathematiques.net/phorum/read.php?16,2296466,2296534#msg-2296534
  • En logique du 1er ordre on peut distinguer des objets du modèle appartenant à différent types c'est à dire "appartenant à différentes relations unaires, comme en géométrie (comme je vous l'ai déjà dit).
  • @JP : un segment d'énoncé "pour tout ordinal $\alpha$, $\cdots$", ou encore un segment d'énoncé "pour toute droite $D$ d'un plan $\mathcal{P}$, il existe un point $p$ de $\mathcal{P}$ n'appartenant pas à $D$" ne t'interpelle pas. En utilisant les quantificateurs $\forall$ et $\exists$, comment traduirais-tu le deuxième énoncé, où je te fais grâce du type "plan" ?
  • La notion de type est censée/supposée représenter l'idée intuitive que des objets sont de natures différentes.

    Par exemple : (référence à l'autre fil) un groupe n'est pas un ensemble, "puisque" il y a une multiplication, donc une structure additionnelle. Si je te donne un ensemble $X$ et $x,y\in X$, tu ne peux pas me dire "qui est $xy$", d'ailleurs la question n'a même pas de sens. Alors que si $X$ est un groupe, soudain tu peux, et la question a un sens ! Le fait que la question ait un sens pour l'un et pas l'autre suggère une différence de nature.

    Ainsi, une personne avide de types te dira que c'est normal : il y a un "type" des ensembles, et un "type" des groupes, et un groupe est un "objet du second, mais pas du premier".

    D'un certain point de vue, le mot "type" peut être synonyme de "catégorie", mais ce n'est pas tout à fait vrai, et c'est un point de vue biaisé (on se demande pourquoi :-D )

    Si tu travailles dans une théorie typée, et que tu déclares une variable ("Soit $x$ ..."), tu vas en principe la déclarer avec son type : "soit $G$ un groupe".

    Par exemple, si je te donne l'énoncé suivant : "soit $G$ un groupe et $x,y \in G$. Alors $xy$ est conjugué à $yx$".
    Bon, bah, ensemblistement il manque plein plein plein d'informations, pourtant tu comprends ce que j'entends par "$x$ multiplié par $y$", c'est sous-entendu par la déclaration que $G$ est un groupe. Formellement, ce n'est pas une déclaration de type (il n'y a pas de types en théorie des ensembles, enfin il n'y en a qu'un : les ensembles), mais à nouveau si tu as un esprit "théorie des types" tu vas y penser comme telle (et si tu travailles dans autre chose que ZF, ça pourrait littéralement être une déclaration de type).
  • Merci énormément Maxtimax ! Ah théorie des types : https://fr.wikipedia.org/wiki/Théorie_des_types
    Je m'empresse d'aller voir ce que c'est.

    Du coup, l'ébauche de la théorie des ensembles du chapitre 1 du livre de P. Dehornoy commence à s'éclairer (bien que je ne comprends pas pourquoi aller chercher la notion de type pour cette introduction). Merci encore.
  • Julia: je précise que par "théorie typée" je ne voulais pas forcément dire théorie des types (d'ailleurs même quand j'ai dit "théorie des types" je ne pensais pas forcément au terme technique), mais seulement une théorie dans laquelle il n'y a pas qu'un type, et chaque objet vient accompagné d'une "étiquette" qui te dit "ah oui, cet objet est de type bidule".

    Par exemple, on peut faire des théories du premier ordre typées, même des théories équationnelles (e.g. la théorie des catégories est une théorie équationnelle du premier ordre typée - qu'on peut rendre non typée mais il faut procéder à différents encodages, comme souvent)
  • Merci Maxtimax. Peu importe théorie typée ou théorie des types pour moi, j'ai compris d'où sortait la notion de "type". Du coup, je comprends tous les messages de ce fil.
Connectez-vous ou Inscrivez-vous pour répondre.
Success message!