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.
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.
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
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 :
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 ?
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 !
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à)
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.
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)
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.
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.
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.
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.
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}\]
(**) Dans un autre univers, l'on aurait pu avoir les types de bases principaux $\mathbf{Ens}$ et $\mathbf{Cls}$.
Contrairement à ce que tu peux penser, le Krivine, qui est excellent, est de lecture difficile. Vas-y !
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.
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.
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.
@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.
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).
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.
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é.
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.
La voici donc.
"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.
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.
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).
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.
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)