Théorie des modèles/démos : axiomatique ?

La "théorie" des modèles n'est pas une théorie au sens de...la théorie des modèles :-D Il faut bien faire attention au double-sens du mot "théorie" ici : l'un est un mot pas technique, qu'on emploie pour désigner un ensemble de résultats, de techniques, de personnes éventuellement, au même titre que théorie des nombres analytique, ou théorie de Galois etc. ; l'autre est un mot technique (utilisé en particulier par les gens qui étudient la "théorie" des modèles, au sens pas technique) qui a donc une définition précise etc. : ensemble de formules etc.

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.

On peut tout formaliser dans ZFC actuellement (et beaucoup moins selon ce qu'on appelle "formaliser"), donc ce n'est pas trop ça la question. En fait tout est déjà formalisé dans ZFC.

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.)

En fait ça dépend de ce qu'on appelle formaliser.
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.

Est-il vraiment possible de tout formaliser dans ZFC

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.