Théorie des modèles/démos : axiomatique ?
Bonsoir ! :-)
Je ne connais pas grand chose à la théorie des modèles et la théorie de la démonstration, mais en ce moment je cherche à en savoir plus.
Seulement, formaliste comme je suis, en lisant des "démonstrations" sur wikipédia ou autre, j'ai l'impression que ces "théories" ne sont pas axiomatisées.
Si elles possèdent des axiomes et règles d'inférences, quels sont-ils ?
Sinon, est-ce que ce n'est pas dérangeant de savoir que le domaine souhaitant rendre les mathématiques rigoureuses n'est lui-même pas rigoureux ?
Si ces théories sont axiomatisables, peuvent-elles s'appliquer à elles-mêmes ? Ces théories font-elles alors parties de celles auxquelles Gödel s'applique par exemple ? Ou encore peut-on trouver un modèle à la théorie des modèles ?
Merci de m'éclairer ^^
Je ne connais pas grand chose à la théorie des modèles et la théorie de la démonstration, mais en ce moment je cherche à en savoir plus.
Seulement, formaliste comme je suis, en lisant des "démonstrations" sur wikipédia ou autre, j'ai l'impression que ces "théories" ne sont pas axiomatisées.
Si elles possèdent des axiomes et règles d'inférences, quels sont-ils ?
Sinon, est-ce que ce n'est pas dérangeant de savoir que le domaine souhaitant rendre les mathématiques rigoureuses n'est lui-même pas rigoureux ?
Si ces théories sont axiomatisables, peuvent-elles s'appliquer à elles-mêmes ? Ces théories font-elles alors parties de celles auxquelles Gödel s'applique par exemple ? Ou encore peut-on trouver un modèle à la théorie des modèles ?
Merci de m'éclairer ^^
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
Pareil pour théorie de la démonstration. Donc il n'y a pas de souci de rigueur ici : la théorie des modèles est juste une collection vague de résultats qui sont ultimately des résultats de théorie des ensembles, comme toutes les maths (officiellement en tout cas)
Le théorème de Gödel s'applique au deuxième mot (c'est un théorème, donc pas trop le choix: il ne peut pas être à propos d'une notion vague), donc à certaines théories au sens précis (précisément celles qui interprètent PA, sont récursivement axiomatisables blabla on se comprend), en particulier pas à la théorie des modèles. Pareil pour un "modèle de la théorie des modèles": ça n'aurait pas de sens.
Cela veut-il dire que pour le premier type de théories, on essaie de prendre de la distance et de voir les choses sous un angle moins formel mais que l'on sait que l'on pourrait formaliser dans une théorie bien sympa (genre ZFC) ?
J'ai en fait une analogie avec les programmes informatiques : ne pourrait-on pas voir les théories au premier sens comme du pseudo-code, c'est-à-dire du code que l'on pourrait formaliser dans un langage de programmation donné ?
Est-ce que l'on ne gagnerait pas en assurance de se placer dans une théorie au deuxième sens plutôt qu'au premier ?
Les théories au premier sens ne peuvent-elles pas toutes s'écrire dans une théorie au deuxième sens (ce qui éviterait de devoir toujours transposer les résultats à ZFC ou autres) ?
Quoiqu'il en soit, je me demande maintenant si la théorie des catégories est une théorie au premier sens ou au deuxième sens...
C'est vraiment 2 mots qui sont très différents, c'est pour ça que je ne suis pas trop à l'aise avec tes analogies et que la réponse à "est-ce qu'on ne gagnerait pas en assurance..." est non : tout est déjà fait rigoureusement dans ZFC, le mot "théorie" dans "théorie des modèles" n'a aucun intérêt mathématique, c'est simplement pour se parler entre humains comme quand on dit "heuristiquement" ou "géométrie algébrique".
Donc non on ne gagnerait pas en assurance parce que ce ne serait pas plus rigoureux, et qu'une théorie du premier ordre mine de rien c'est super faible (prendre pour exemple la "théorie des groupes" où là les deux sens du mots interviennent : c'est à la fois une théorie au sens de collections de résultats, techniques etc et une théorie du premier ordre : pourtant la plupart des résultats qui nous intéressent ne s'expriment même pas au premier ordre (le théorème de Lagrange pour n'en citer qu'un ; les théorèmes de Sylow ; enfin honnêtement je vois peu d'énoncés du premier ordre intéressants sur les groupes - alors qu'étudier leur théorie du premier ordre est intéressant !)
La théorie des catégories, comme la théorie des groupes, c'est deux choses : l'une de ces choses a un sens précis (théorie du premier ordre etc.) et l'autre non (collection de résultats, de techniques, d'idées, de personnes, etc.)
Il ne me reste plus qu'à me plonger dans les bouquins de Cori, Lascar et Krivine cet été pour m'assurer que je comprends bien tous vos propos !
Cependant l'une de vos remarques m'a frappé. Est-il vraiment possible de tout formaliser dans $ZFC$ ? Peut-être vouliez-vous dire presque tout ? Ou peut-être parliez vous simplement des résultats de la théorie des modèles et de la théorie de la démonstration ?
Car dans certaines théories, on peut par exemple construire un ensemble univers (comme dans $GPK_{\infty}^+$ ou encore $NF(U)$ et ses extensions), ce qui n'est pas possible dans $ZFC$ (difficile de manipuler des prédicats comme des objets).
J'espère que je ne dis pas trop de bêtises !
J'aurais dû préciser, mais au sens où tu l'entends sûrement, alors oui c'est un "presque tout". De même qu'en théorie des ensembles il y a souvent des axiomes supplémentaires, typiquement de grands cardinaux (quoiqu'on peut se dire que ça reste dans ZFC et que l'énoncé devient "si tel grand cardinal alors blabla"), mais globalement toutes les maths "usuelles" disons.
Le livre de Marker, "An introduction to model theory" est également bien, mais un peu plus fouillis par endroits.
Tu confonds plusieurs choses, comme la suite de ce que tu écris le montre. ZFC est une liste d'axiomes. On ne formalise pas les choses dans une liste d'axiomes. Ca ne veut rien dire.
Ce que tu voulais demander est "est-il possible*** de tout formaliser dans le langage de ZFC (ZF, etc)?" et la réponse est évidemment oui, en fait ce n'est même pas une possibilité, c'est qu'il n'est tout bêtement pas possible de "formaliser" la science autrement qu'en l'écrivant dans ce langage (éventuellement en remplaant le $\in$ par $space$ ou $chr(32)$.
Bien entendu on peut gagner du temps en "faisant semblant" qu'un prédicat n'est pas un ensemble, mais c'est un maquillage qu'on peut en gros qualifier de "politique", c'est tout.
Le truc que tu crois difficile est en réalité une question de grammaire enfantine: quand tu mets des mots des signes à se suivre, tu as un "statut" de l'espace entre eux (qui est synonyme de $\in$. La science mettant en gras tout ce qui n'est pas prouvé ou défini, au lieu de la cacher dans un petit coin, on a certes décidé que "Médor mange" s'écrirait $Medor\in manger$, mais ça ne va pas plus loin, il n'y a pas de "fond" derrière. On aurait pu aussi gardé l'espace, ou pire, statuter aussi l'espace entre $x$ et $\in$ dans $x\in y$ et écrire $x\in_2 \in_1 \in_2 y$, mais comme c'est idempotent on s'en est tenu à une seule explicitation te non pas deux, qui serait devenue stupide.
*** Par contre, il n'est pas possible de "tout trancher par preuve" dans ZF. ZF(C), comme toute autre théorie récursive admet des énoncés, tout à fait "banals", mais a priori indécidables. Seules les théories extrêmement faibles dans lesquelles on ne peut quasiment rien faire sont récursives même au niveau de leurs théorèmes.