Théorie des ensembles et logique mathématique
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.
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
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"
J'affirme péremptoirement que toute affirmation péremptoire est fausse
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 ?
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 !
J'affirme péremptoirement que toute affirmation péremptoire est fausse
J'affirme péremptoirement que toute affirmation péremptoire est fausse
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.
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.
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.
Je ne pense pas qu'on puisse démarrer les mathématiques avec des notions formelles.
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.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
Effectivement la théorie des ensembles est la base de toute la théorie du livre d'où ma question.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
J'affirme péremptoirement que toute affirmation péremptoire est fausse
É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)$.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
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).
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.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
Je n'ai pas compris votre remarque sur le flou de l'ensemble des parties
J'affirme péremptoirement que toute affirmation péremptoire est fausse