Théorie des ensembles et logique mathématique

arnaud_s · November 2022

Bonjour

J'essaie de trouver une construction formelle de la théorie des ensembles et de la logique.

Je commence par la théorie des ensembles avec le livre de Jean-Louis Krivine. Il semble très bien mais il prétend la logique mathématique acquise pour décrire la théorie des ensembles.

J'ai donc mis la théorie des ensembles en pause pour me tourner vers la logique mathématique avec le livre de Daniel Lascar et Rene Cori.

Dès le début du livre, on parle de théorie des langages, qui dépend de la théorie des ensembles. (je vais l'étudier avec le livre de Olivier Carton.)

Je me trouve donc dans une boucle ou pour décrire formellement A je dois décrire B qui dépend de C qui lui-même dépend de A.

Est-il possible de décrire formellement ces notions au fur et à mesure ?

La notion d'inclusion en théorie des ensembles à besoin de la logique mathématique pour être décrite formellement, mais la logique mathématique à besoin de la théorie des ensembles pour décrire formellement une syntaxe valide...

Merci.

Médiat_Suprème · November 2022

Je ne possède pas le Lascar-Cori, dans quelle circonstance voyez-vous que la syntaxe de la logique a besoin de la théorie des ensembles ?

D'un point de vue général, j'ai l'impression que vous cherchez un moteur immobile, ou encore un dictionnaire qui ne serait pas en ordre alphabétique, mais où chaque mot ne serait défini qu'à l'aide des mots précédents.

Vous pouvez aussi chercher le "trilemme de Münchhausen"

arnaud_s · November 2022

La théorie des ensembles est utilisée à travers la théorie des langages pour définir une syntaxe valide de la logique mathématique.

Je me suis fait cette remarque du dictionnaire mais ma question ne me semble pas dénuée de sens.
Si je prouve un théorème A en utilisant un théorème B qui prend pour acquis que A est vrai, que me direz-vous ?

708 · November 2022

Bonjour,
je me suis posé la même question que toi. La meilleure solution que j’ai trouvée est Bourbaki, livre 1. J’ai été bluffé quand je l’ai lu !

Médiat_Suprème · November 2022

arnaud_s a dit :

La théorie des ensembles est utilisée à travers la théorie des langages pour définir une syntaxe valide de la logique mathématique.

J'aimerais savoir comment ...

Foys · November 2022

On peut faire de la logique formelle avant la théorie des ensembles. La théorie des ensembles se base sur la logique classique du premier ordre avec le seul symbole de prédicat $\in $ (l'énoncé $Ext:=\forall x \forall y ((\forall z, z\in x \leftrightarrow z \in y) \to (\forall z, x \in z \leftrightarrow y \in z))$ s'appelle axiome d'extensionnalité; si on pose $"x = y":= \forall z (z\in x \leftrightarrow z \in y)$, on peut montrer par induction sur la taille de la formule $P$ le théorème $Ext \to x_1 = y_1 \to x_2 = y_2 \to ... \to x_n = y_n \to (P \leftrightarrow P[x_1 := y_1,...,x_n := y_n]) $ où $x_1,...,x_n$ contient toutes les variables libres de $P$; ainsi $=$ satisfait les axiomes d'une théorie égalitaire).

La grande difficulté (jamais vraiment avouée) de ZF est d'exprimer des formules de mathématiques "normales" avec symboles de fonctions, d'opérations, des choses comme "$\{x \mid \Phi\}$", malgré le fait que rien de tout ceci n'est techniquement disponible dans la description "officielle" de la théorie des ensembles comme théorie logique telle que présentée ci-dessus. Dans Bourbaki, il y a un symbole de description indéfinie donc il n'y a pas de problème. Mais Bourbaki n'est pas la théorie des ensembles usuelles.

Voilà une façon de faire (qui est très lourde - en fait il va falloir transpirer pour écrire les preuves d'énoncés très basiques- mais qui marche in fine et est à mon avis intuitive: voir le livre de Golbdblatt: "Topoi" où il l'évoque brièvement. Voir aussi les livres de théorie des ensembles d'Azriel Levy, et en particulier celui de Takeuti et Zaring où cela est détaillé).

On supppose la gestion des variables libres/liées maîtrisée du lecteur. On appelle "terme" toute lettre ou tout couple $\{x|P\}$ où $x$ est une lettre et $P$ une formule. Ensuite si $a$ est une lettre et $T$ un terme, on pose:

$a \in T:= P[x:=a]$ si $T=\{x|P\}$, et $a \in T:= a \in b$ si $T$ est la lettre $b$.

On pose pour tous termes $A,B$, $A = B:= \forall x, x \in A \leftrightarrow x \in B$ (cette définition généralise aux termes l'égalité pour des lettres définie plus haut).

Si $P$ est une formule, $x$ une lettre et $T$ un terme, on pose $\{x\mid P\}:= \exists y \left ( t = \{x\mid P\} \wedge y \in T \right )$ (on prend bien sûr $y\neq x$ et $y$ non libre dans $T$).

Ainsi, $A\in B$ et $A = B$ sont définies pour tous termes $A,B$. L'énoncé $\exists x (x = A)$ se dit "$A$ est un ensemble".

Avec ces considérations, si un terme appartient à un autre, le premier est donc toujours un ensemble. De plus les quantifications ne portent que sur des ensembles. L'axiome d'extensionnalité est supposé dans tout ce qui suit.

On note pour tous termes $A,B$, $\{A,B\}:= \{x \mid x = A \wedge x = B\}$. L'axiome de la paire dit: pour tous $u,v$, $\{u,v\}$ est un ensemble.

On note pour tous terme $A,B$, $A \subseteq B:= \forall x, x \in A \to x \in B$.

On note pour tout terme $A$, $\mathcal P (A):= \{x \mid x \subseteq A\}$ et $\bigcup A := \{x \mid \exists y, y \in A \wedge x \in y\}$.

L'axiome des parties dit que pour tout $x$, $\mathcal P(x)$ est un ensemble. L'axiome de la réunion dit que pour tout $x$, $\bigcup x$ est un ensemble.

On note $\{x \in E\mid \mathcal P\}:= \{x \mid x \in E \wedge P\}$ pour tout terme $E$ et toute formule $P$. Le schéma de compréhension dit que si $E$ est un ensemble alors $\{x \in E \mid P\}$ en est également un.

Soit $R(x,y)$ une formule dont $x,y$ sont parmi les variables libres et son distinctes. Soit $T$ un terme. On note $\{R(x) \mid x \in T\}:= \{y \mid \exists x, x \in T \wedge R(x,y)\}$. La phrase "$R$ est une relation fonctionnelle" abrège $\forall x \forall y \forall y', R(x,y) \to R(x,y') \to y = y'$.

Le schéma de substitution dit que si $R$ est une relation fonctionnelle et si $T$ est un ensemble (en fait il ne s'énonce que quand $T$ est une lettre mais cela revient au même) alors $\{R(x) \mid x \in T\}$ est un ensemble.

Les autres axiomes de ZF/ZFC ne posent pas de problème de notation particulier (infini, fondation, choix... ).

L'intention originelle de la théorie des ensembles était d'avoir "un ensemble = une propriété formelle". Depuis le paradoxe de Russell on sait que ce n'est pas possible cependant ceci est une façon de s'en approcher le plus possible sans problèmes immédiats. En construisant un terme représentant un ensemble donné, en pratique on construit la formule qui caractérise ses éléments.

Médiat_Suprème · November 2022

Je ne sais pas si c'est le problème de arnaud_s, mais j'ai souvent vu ce genre de réaction à la lecture de phrases comme "un ensemble de variables", alors qu'il n'est nul besoin de théorie des ensembles pour écrire cette phrase.

Foys · November 2022

@Médiat_Suprème dans "ensemble des variables", on peut facilement substituer liste informatique à ensemble.

Il y a d'autres références aux ensembles plus embêtantes comme les références continuelles aux notions de théorie des modèles (mais qui -sacrilège!- ont aussi des solutions syntaxiques).

troisqua · November 2022

Comment montrer des formules par induction portant sur des entiers sans avoir défini les entiers préalablement ?

Foys · November 2022

@troisqua il s'agit d'induction au sens informatique ce qui n'est pas engageant.

On considère les règles suivantes:

- $\mathbf o$ est une variable

-si $\Box$ est une variable, $'\Box$ est une variable

-si $\Box, \diamondsuit$ sont des variables, $E\Box \diamondsuit$ est une formule

-si $\Box,\diamondsuit$ sont des formules, $\mathbf D \Box \diamondsuit$ sont des formules

-si $\Box$ est une formule et $\diamondsuit$ est une variable alors $\exists \diamondsuit \Box$ est une formule.

Une formule est n'importe quelle suite de caractères obtenue par applications successives de ces règles et rien d'autre. On décrète que les constructions précédentes ne s'appliquent qu'aux objets qu'on peut qualifier de formules et de variables via ces règles.

($"a \in b":= Eab$, $"nand (f,g)" := \mathbf D f g$ etc).

Les preuves dites par induction sur la taille des formules sont des "recettes" que l'usager peut appliquer aux formules pour écrire des théorèmes (le programme informatique correspondant termine à chaque fois).

[Utilisateur supprimé] · November 2022

@troisqua
La théorie naïve des ensembles précède la théorie des modèles qui précède la théorie formelle des ensembles.
Cependant, pas besoin des entiers pour prouver par induction, puisque le théorème d'induction est une propriété des bien-fondées set-like. L' ensemble des formules peut être muni naturellement d'une relation bien-fondée : pour définir cette relation sur les formules, on utilise la fonction profondeur, une formule est strictement inférieur à une autre si la profondeur de la première est strictement inférieur à celle de la seconde. La fonction profondeur a pour but l'ensemble des entiers 😓, mauvais exemple d'induction "sans" entiers.

Foys · November 2022

Deux mots sur le soufflé de la théorie des modèles qui précéderait la théorie des ensembles.

Les notations sont celles de mon long post.

Soit $X$ un terme et $R$ une formule ayant deux variables libres $x,y$. On pose:

-$(X,R)\vDash a \in b := a \in X \wedge b \in X \wedge R[x:=a,y:=b]$

-$(X,R) \vDash nand (\Phi;\Psi):= nand ((X,R) \vDash \Phi; (X,R) \vDash \Psi)$

-$(X,R) \vDash \exists y \Theta := \exists y, y \in X \wedge \Theta $

Après ça, n'importe quel résultat de théorie des modèles s'importe dans la théorie des ensembles par cette traduction. Pour les plus lourds (Lowenheim Skolem etc) il convient de définir "l'ensemble des formules". C'est un terme $F$ qui a entre autres les propriétés suivantes. Pour toute formule $G$ au sens précédent, il y a un terme $\#G$ ("numéro de Gödel" )appartenant à $F$ et pour tous $X$ termes et $R$ relation, il existe un terme $V(X,R)$ tels que $\#G \in V(X,R)$ si et seulement si $(X,R) \vDash G$.

troisqua · November 2022

Foys parlait de "montrer par induction sur la taille de la formule [...]" mais à ce stade de la construction des mathématiques a-t-on défini ce qu'est "la taille d'une formule" ? C'était le sens de ma question.

Foys · November 2022

Il s'agissait d'une formulation réthorique de ce que j'ai dit dans le message suivant.

708 · November 2022

Foys a dit :
Mais Bourbaki n'est pas la théorie des ensembles usuelles.

Ce n’est pas grave : une fois la théorie des ensembles de Bourbaki construite, on peut construire proprement la théorie des modèles, dans laquelle on construit ZFC.

[Utilisateur supprimé] · November 2022

@troisqua, à ce stade on dispose déjà de la théorie naïve des ensembles, donc on peut définir la "taille" d'une formule, d'ailleurs on a le même soucis pour définir les formules elles mêmes.
En gros la base de la logique c'est exactement la même chose que la base des autres branches des mathématiques: la théorie naïve des ensembles qui n'appartient pas plus au logicien qu'à l'algébriste.

708 · November 2022

cohomologies a dit :

En gros la base de la logique c'est exactement la même chose que la base des autres branches des mathématiques: la théorie naïve des ensembles qui n'appartient pas plus au logicien qu'à l'algébriste.

Pas d’accord : Bourbaki par exemple qu’on peut définir proprement les mathématiques sans théorie naïve des ensembles.

Thierry Poma · November 2022

@arnaud_s : à la page 4, Introduction, les auteurs R. Cori et D. Lascar précisent ceci :

Image: https://les-mathematiques.net/vanilla/uploads/editor/nf/1duwz5p8jcbk.png

Foys · November 2022

Il n'y a pas besoin de "théorie des modèles en amont" pour définir la théorie des ensembles (pas plus qu'il "n'a fallu la main de Dieu au préalable pour construire des ordinateurs") ni de "théorie naïve des ensembles" (qui ne veut rien dire). Il y a besoin de savoir ce qu'est une suite de symboles, afin de comprendre ce genre de messages: https://les-mathematiques.net/vanilla/index.php?p=/discussion/comment/2391718/#Comment_2391718

Thierry Poma · November 2022

@708 : Pour Bourbaki, je t'invite à lire E I.9 à E I.12, ainsi que E I.42 concernant leur Caractérisation des termes et des relations, où le vocable "poids" est à remplacer par le vocable "arité". Nous retrouvons ainsi la même chose développé par Cori-Lascar, concernant la règle des poids.

708 · November 2022

Certes, la pratique mathématique est nécessaire pour lire Bourbaki. Pour moi, la notion de nombre entier ne l’est pas ni celle d’ensemble. J’irai voir tes références.

[Utilisateur supprimé] · November 2022

@Foys
La théorie naïve des ensembles, c'est la théorie informelle des ensembles, sans notion de formule. Cela correspond en quelques sortes à ce dont mon ancien prof M.René Cori parle dans son livre, surtout dans la version partagée par @Thierry Poma.
Je ne comprends pas ton appel à l'informatique pour définir des notions mathématiques.
Aussi, dis moi comment tu définis ce qu'est une suite avec ton approche.

Foys · November 2022

@cohomologies dans la "théorie naïve des ensembles" y a-t-il un ensemble des ensembles qui ne s'appartiennent pas eux-mêmes et (quelle que soit la réponse) pourquoi ?

Et sinon il existe un site internet de maths entièrement formalisées, que voici: https://us.metamath.org/mpeuni/mmset.html

S'il était impossible pour des raisons fondamentales de fonder les mathématiques sans "théorie des ensembles préalable" ce site n'existerait pas.

IL N'EXISTERAIT PAS PHYSIQUEMENT !!!

Et ne me ressortez pas la vieille antienne "oui mais ouin ouin ce n'est pas pédagogique": c'est hors-sujet ici, en faisant ça vous déplacez le débat de "il est fondamentalement impossible de fonder les mathématiques" à "cette présentation est difficilement compréhensible", une phrase qui veut dire quelque chose de TOTALEMENT DIFFÉRENT (et qui est vraie mais hors-sujet dans le fil).

[Utilisateur supprimé] · November 2022

La théorie naïve des ensembles, c'est exactement ZF, sauf que c'est informel, pas de notion de formule. En gros c'est ZF présenté sous la même forme que les éléments d'Euclide.
Je ne pense pas qu'on puisse démarrer les mathématiques avec des notions formelles.

Thierry Poma · November 2022

@708 : notons $n:S\to\N,\,s\mapsto{}n(s)$ l'application qui associe à chaque signe $s\in{}S$ son arité et par $p:S\to\Z,\,s\mapsto{}n(s)-1$ l'application qui associe à chaque signe $s\in{}S$ son poids (remarquer que $l(s)=1$).

Conformément à la définition de Bourbaki sur les mots équilibrés, écrite autrement, un mot $A\in{}L_{\mathrm{o}}(S)$ est dit équilibré s'il possède les deux propriétés suivantes :

$-1=n(A)-l(A)=p(A)$ (ce qui implique que $A$ n'est pas vide).
Pour tout segment initial propre $B$ de $A$, l'on a $0\leqslant{}n(B)-l(B)=p(B)$.

Comparer ce qui précède avec le texte de Cori-Lascar :

Manifestement, dire que $M$ satisfait la règle des poids revient à affirmer qu'il est équilibré. Cori-Lascar auraient-ils plagié Bourbaki ?

Foys · November 2022

@cohomologies une "suite finie de caractères" est par exemple un texte obtenu à l'aide des règles suivantes : le symbole $0$ ou bien $(1,x)$ où $x$ est une suite finie.

Foys · November 2022

@cohomologies le caractère "naturel" de ZF ne va pas de soi comme on le voit sur les 20 ou 30 ans d'âpres débats ayant précédé la proclamation des axiomes de ZF ainsi que des prises de position de certains mathématiciens de l'époque (comme le rejet de l'axiome des parties par Lebesgue par exemple: cet axiome est déjà un gros producteur de problèmes puisque étant donné un ensemble $y$ la propriété portant sur $x$ "$x$ est l'ensemble des parties de $y$" n'est pas absolue: on peut changer son sens en changeant l'univers -un ensemble transitif mettons- ambient).

arnaud_s · November 2022

708: J'avais pensé aux Bourbaki mais le nombre de critiques dessus m'ont fait chercher une autre alternative, je vais peut-être me lancer.

Mediat_supreme: Voici un extrait du livre qui je l'espère, réponds à ta question

Foys: C'est intéressant merci, je relirais tranquillement ce week-end et j'irais regarder tes références.

Media_supreme: Je considère que l'on fait de la théorie des ensembles à partir du moment où l'on parle d'un ensemble de variables $A$ avec une notion d'appartenance de la variable $x$ à l'ensemble $A$ sauf si une autre définition est donnée comme Foys au-dessus.

C'est peut être une erreur de ma part.

Foys: Je fais la même remarque qu'au-dessus, une liste c'est ni plus ni moins qu'un ensemble avec une notion d'appartenance, donc de la théorie des ensembles.

Encore une fois c'est peut-être une mauvaise interprétation de ma part.

Thierry Poma: J'ai effectivement lu ce paragraphe mais l'objectif de ma question est de savoir s'il est possible de faire cette construction en partant de 0.

Thierry Poma · November 2022

@arnaud_s : à mon avis, tu ne donnes pas la partie la plus significative. Voici une partie plus significative du livre où il s'agit de construire de bas en haut les termes du langage $\mathcal{L}$ :

L'on note l'emploi prédominant d'ensembles, d'entiers et de l'induction.

Médiat_Suprème · November 2022

Foys a dit :

@Médiat_Suprème dans "ensemble des variables", on peut facilement substituer liste informatique à ensemble.

Ou liste, ou collection, ou ... Ce n'est pas moi qui ai le problème. J'ai même vu une réaction à "$\in$ est une relation entre deux ensembles" sous la forme "il faut l'arithmétique avant ZF, ce qui est, bien sûr, crétin.

arnaud_s · November 2022

Thierry Poma : Merci d'avoir complété mon message.

Effectivement la théorie des ensembles est la base de toute la théorie du livre d'où ma question.

Médiat_Suprème · November 2022

arnaud_s a dit :

Media_supreme: Je considère que l'on fait de la théorie des ensembles à partir du moment où l'on parle d'un ensemble de variables $A$ avec une notion d'appartenance de la variable $x$ à l'ensemble $A$ sauf si une autre définition est donnée comme Foys au-dessus.
C'est peut être une erreur de ma part.

Oui, c'est bien une erreur, et profonde si ce n'est grave, une théorie des ensembles permet de faire beaucoup de chose avec les ensembles, parler d'un ensemble de variables (d'un paquet de variables) permet juste de dire qu'il y en a 2 quand on en a besoin de 2 ou 104 quand il y en a besoin de 104.

Médiat_Suprème · November 2022

Je viens de parcourir le texte de Cori-Lascar, c'est un peu plus complexe que dans mon message précédent mais cela reste du même domaine.

Thierry Poma · November 2022

@arnaud_s : Bourbaki utilise le concept de construction formative qui consiste à construire termes et relations, de bas en haut, liés à leur langage ; cela se fait inductivement. Partir de ex nihilo est un pur fantasme.

[Utilisateur supprimé] · November 2022

Foys a dit :

@cohomologies une "suite finie de caractères" est par exemple un texte obtenu à l'aide des règles suivantes : le symbole $0$ ou bien $(1,x)$ où $x$ est une suite finie.

Je ne veux pas être antagoniste, mais je doute qu'on puisse donner un sense d'emblée à cette définition. Il faut carrément un théorème pour montrer que cette définition défini bien quelque chose: en gros là il s'agit de l'intersection de la classe des ensembles qui contiennent $\{0\}$ et sont stables par $x\mapsto (1,x)$, ça c'est la définition par le haut, sinon la définition par le bas utilise les entiers je crois.
Édit. Pour la définition par le haut, il faudrait d'abord montrer qu'il existe une un ensemble contenant $\{0\}$ et stable par $x\mapsto (1,x)$.

[Utilisateur supprimé] · November 2022

Thierry Poma a dit : https://les-mathematiques.net/vanilla/index.php?p=/discussion/comment/2391771/#Comment_2391771

[Inutile de recopier un message présent sur le forum. Un lien suffit. AD]

Je crois que $n$ et son prolongement en morphisme de monoïde sont notés par le même nom. Idem pour $p$.

Foys · November 2022

cohomologies a dit:
Je ne veux pas être antagoniste, mais je doute qu'on puisse donner un sense d'emblée à cette définition. Il faut carrément un théorème pour montrer que cette définition défini bien quelque chose:

Le constructeur qui a produit le PC depuis lequel tu t'exprimes n'a pas eu besoin d'un tel théorème pour faire marcher son appareil et afficher des suites de caractères ou compiler des programmes. Comment a-t-il fait? C'est aussi pour cela que je fais référence à l'informatique.

Foys · November 2022

Il y a bien des références aux concepts ensemblistes dans les livres de logique mais ils sont faits pour inspirer les bonnes idées (sans les employer on se retrouverait avec des périphrases interminables), pas pour invoquer la théorie des ensembles dans toute sa lourdeur.

708 · November 2022

L’introduction du livre 1 de Bourbaki parle de cette question. De mémoire, il dit qu’une compétence requise pour le mathématicien est la capacité de reconnaître un symbole.

samok · November 2022

Bonsoir,

il est question de langage, aussi un détour par le langage courant permet d'expliquer ce qui se passe.

Peut-on apprendre à parler avec un dictionnaire. Non, une grammaire structure les mots. Grammaire qui utilise des mots du dictionnaire n'est-ce pas ?

Après former des phrases est une chose, la comprendre en est une autre. C'est là que notre petite tête intervient, le mystérieux processeur qui s'accommode de tout ça compte tenu de son expérience.

Ainsi je pense que c'est dans notre petite qu'il y a une possibilité d'intégrer cette espèce d'Orouboros à plusieurs têtes et et plusieurs queues.

Le détour par l'informatique de Foys est aussi éclairant, je trouve. Il y a bien des transistors et un langage qui agissent sur les transistors. Langage qui peut définir des variables et des fonctions avec des portées dans les différents types de mémoire. Et le langage peut autoriser un retour en arrière avec un nouveau mot clef, la récursion devient possible.

Mais ce détour a ses limites, à ce jour, il n'existe pas à ma connaissance de vraie machine de Turing car nos ordinateurs sont des machines de Turing avec un ruban fini.

Aussi, on ne manipule que des ensembles finis ou alors des infinis potentiels. Dans le passage du Cori-Lascar de Thierry Poma, il y a clairement de l'infini actuel.

Bref tout comme arnaud_s je pense qu'il y a effectivement quelque chose qui se mord la queue, du point de vue d'un édifice conceptuel mais que notre petite tête s'en accommode.

Foys · November 2022

Il n'y a jamais besoin d'infini actuel dans les présentations sur les formules. Les développements qui précèdent montrent des séries d'étapes à faire sur un élément de texte qui, si elles aboutissent, établissent qu'un objet donné est une formule.

Quant aux histoires de ruban fini, une machine de Turing qui termine sur une entrée donnée ne consomme qu'une quantité finie de ruban.

Les seules fonctions qui sont envisagées pour la construction des objets de la logique sont toutes récursives primitives (parcourir des strings et réaliser des opérations sur des sous-textes).

Foys · November 2022

Petit sondage: pensez-vous que la multiplication de deux entiers à 10^100000 chiffres en base 10 n'existe pas parce qu'il n'y a que 10^50 atomes sur terre (donc un problème pour réaliser l'ordinateur correspondant)? @samok ?

Médiat_Suprème · November 2022

Un moyen simple que j'ai utilisé pour faire comprendre un point similaire est la notion de schéma d'axiomes, qui couvre une infinité d'axiomes, mais dans une démonstration, seul un nombre fini d'axiomes va être utilisé, et donc, pour chaque démonstration, on peut écrire la liste finie des axiomes nécessaires.

[Utilisateur supprimé] · November 2022

Foys a dit :

Il y a bien des références aux concepts ensemblistes dans les livres de logique mais ils sont faits pour inspirer les bonnes idées (sans les employer on se retrouverait avec des périphrases interminables), pas pour invoquer la théorie des ensembles dans toute sa lourdeur.

En ce qui me concerne, je différencies la théorie naïve de la théorie formelle, on peut bien entendu affaiblir la théorie naïve et c'est ce que font beaucoup.
Bref, les proof-theorists ont une autre vision de la théorie des ensembles, c'est une vision que je ne partages pas. Ma vision c'est celle du Cori-Lascar.
Édit. Je parle de la conception de la théorie des ensembles d'un de mes amis set-theorists qui fonde la théorie des ensembles avec la théorie de la démonstration, je pense que c'est assez proche de ce que tu fais (excuse moi si je me trompes là dessus).

samok · November 2022

$A$ parce que $B$ me bloque pour évaluer l'expression.

Après c'est facile, pour moi

$A$ est fausse, la multiplication de deux entiers à $10^{100000}$ chiffres existe
$B$ est vraie car je te crois et le pose comme axiome

Que vaut $A$ parce que $B$ ? tu me le diras quand tu m'auras défini ce connecteur

(et si tu réponds vite, je vais te faire scier avec la définition d'un atome, non je rigole

)

arnaud_s · November 2022

Médiat_Suprème : J'ai inclus la notion d'appartenance et c'est justement ça qui me fait parler d'ensemble.

Thierry Poma : Je vais lire Bourbaki pour me faire une idée.

Médiat_Suprème · November 2022

Parler d'ensembles ne pose pas de problème, c'est parler de théorie des ensembles qui est inutile.

Foys · November 2022

Médiat_Suprème a dit :

Parler d'ensembles ne pose pas de problème, c'est parler de théorie des ensembles qui est inutile.

À condition qu'on comprenne de quoi il s'agit quand le mot ensemble est prononcé. Les pathologies exhibées par la théorie des ensembles formelle montrent déjà qu'on est dans le flou quand on parle d'ensemble des parties d'un ensemble.

Médiat_Suprème · November 2022

arnaud_s parlait de la phrase "ensemble de variables", je ne vois vraiment pas la pertinence d'une quelconque TDE ici, l'expression "paquet de variables" marche tout aussi bien.

Je n'ai pas compris votre remarque sur le flou de l'ensemble des parties

Thierry Poma · November 2022

La reproduction ci-jointe montre la manière dont le couple Cori-Lascar s'y prend pour construire de bas en haut l'ensemble des termes sur le langage $L$ :

Image: https://les-mathematiques.net/vanilla/uploads/editor/z8/6ing52h947zc.png

Cette façon de procéder me parle et a le mérite d'être succincte, sans pour autant mettre en péril la suite du traité, y compris celle consistant à fonder la théorie des ensembles (même si cette fondation est déplorable dans le cas de Cori-Lascar, mais passons...). Inutile d'être hypocrite, l'arsenal de la théorie des ensembles a été abondamment utilisé pour décrire ce qui me préoccupe ici ; cela ne me gêne pas du tout, car mon parcours scolaire m'a fourni la grammaire ou le code me permettant de décoder ce qui est écrit. Cette histoire de fondation est un faux problème. L'on ne peut humainement rien faire ex nihilo.

Foys · November 2022

@Médiat_Suprème imaginons qu'il y ait au moins une structure ($U$ avec relation binaire $R$) qui satisfasse ZF. Alors il y en a automatiquement une abondance dont certaines contenues les unes dans les autres et qui peuvent être dans $U$ un ensemble transitif $M$ dénombrable dans $U$. C'est un artifice dont le forcing se sert. Alors tout élément $x$ de $M$ est tel qu'il existe un ensemble des parties $\mathcal P^M(x)$ de $x$ dans $M$ et un ensemble des parties $\mathcal P(x)$ dans $U$, et chaque fois que $x$ est infini on a $\mathcal P(x) \neq \mathcal P^M(x)$ puisque $\mathcal P^M (x)$ est dénombrable dans $U$ (tout ceci peut se trouver dans le livre de théorie des ensembles de J.-L. Krivine).

Toutes les théories récursives exprimant l'arithmétique prêtent le flanc au théorème d'incomplétude de Gödel et, via le théorème de complétude on se retrouve avec aucun ou plusieurs modèles différents de telles théories mais avec les ensembles apparaissent de véritables pathologies affectant des objets aussi simples (en apparence en tout cas) que l'ensemble des parties d'un ensemble (là où Peano se contente d'exhiber de modestes entiers non standards).

L'autre point gênant est le fait que le théorème de complétude est faux en logique d'ordre supérieure lorsqu'on impose d'interpréter $\{0,1\}^x$ par $\mathcal P(x)$ aux notations près ou plus généralement $A \to B$ par $B^A$ (qui est ambigu lui aussi pour les mêmes raisons).

Théorie des ensembles et logique mathématique

Réponses

Lettre d'information