1.3. Structure des théories

Nous allons d'abord évoquer plusieurs théories et leurs modèles, donc nous situer en théorie des modèles. Puis concentrer l'étude sur une théorie (des ensembles) avec un modèle supposé fixe: les variables «théorie» et «modèle» étant fixées, nous serons en théorie du modèle.
Chaque théorie a ses propres notions, couramment désignées par des noms communs, et désignant dans chaque modèle les domaines possibles de ses variables. La théorie des modèles admet les notions de théorie et de modèle, invisibles en théorie du modèle du fait de leur fixation.
Tout modèle M d'une théorie T donne un modèle M1=[T,M] à la théorie du modèle (T1). Les noms communs des notions de T1 désignant normalement leur interprétation dans M1, on leur ajoutera le préfixe méta- pour désigner leur interprétation dans l'autre modèle [T1,M1] de T1.
Un objet (d'une théorie dans un modèle), est tout élement d'une notion (valeur possible d'une variable). Par cette notion d'objet, la théorie du modèle distingue les objets de T dans M parmi ses propres objets dans M1 (les méta-objets). Tout objet est donc un méta-objet; mais en pratique on réservera le nom de méta-objet à ceux d'entre eux qui ne sont pas des objets. Contrairement à la théorie des ensembles, la théorie du modèle donne à toute variable de sa théorie étudiée un domaine parmi les notions, mais ne le regarde que comme méta-objet.
On appellera théorie générique toute théorie présentée conformément à un certain format standard (décrite par une théorie du modèle plus précise), en lequel seront traduisibles les théories que nous évoquerons. Ce format clarifie notamment la gestion des variables en n'admettant comme notions que des types (en nombre fini pour chaque théorie) classifiant à la fois variables et objets : chaque objet n'appartiendra qu'à un seul type, celui des variables qui peuvent le désigner.
Voici quelques exemples de notions de diverses théories.

Théorie    Objets (notions)
Théorie générique    Eléments purs classés par types
Théorie des ensembles    Eléments, ensembles, fonctions (et autres: opérations, n-uplets...)
Théorie des modèles    Théories génériques, modèles et leurs constituants.
Théorie du modèle    Objets, symboles, notions, expressions, structures, axiomes...
Arithmétique    Nombres entiers
Algèbre linéaire    Vecteurs, scalaires...
Géométrie    Points, droites, cercles...

Les notions de théorie du modèle classifient les constituants de la théorie (types abstraits, symboles, expressions), et ceux du modèle. Les théories génériques ont 5 sortes de symboles: de variable, de structure (opérateur ou prédicat), connecteurs, et quantificateurs (∀ et ∃). Chaque théorie générique se distingue par ses listes de types abstraits, de symboles de structure (formant son langage ), et d'axiomes.
L'autre fondement possible de toute théorie générique (sans théorie du modèle) est sa traduction en théorie des ensembles. Toutes les théories et leurs modèles peuvent ainsi s'intégrer dans une théorie des ensembles munie d'un modèle fixe (aussi baptisé univers pour cette raison). Mais seuls les constituants du modèle (et le modèle lui-même) sont par là traduits en objets; ceux de la théorie générique sont traduits en constituants de la théorie des ensembles.
Décrivons les notions de théorie du modèle (la forme d'une théorie générique et de son modèle) par une telle traduction valable pour toute théorie générique: tous les objets seront traduits en éléments purs (contrairement à l'usage de la géométrie présentant les droites comme ensembles de points).
La traduction laisse les symboles de variables tels quels. Les types abstraits et les symboles de structure se traduisent tous en symboles de variables libres, qui restent libres tant que le modèle reste fixe. Leurs valeurs sont les principaux constituants du modèle, ceux qui le déterminent.
Les valeurs des types abstraits sont des ensembles d'objets, appelés types interprétés.

Les structures
Chaque symbole d'opérateur désigne une opération appelée un opérateur, dont chaque argument a pour domaine un type, et les valeurs sont d'un même type; l'arité (ou la liste des arguments présentés comme des espaces), le type abstrait de chaque argument et celui des valeurs sont fixés comme données du symbole. Lorsque l'arité est nulle c'est un symbole de constante, désignant directement un objet fixe. Un opérateur unaire, désignant une fonction, sera appelé foncteur.
A cette représentation du modèle s'ajoute de manière standard, un type spécial: celui des booléens fait des deux éléments «vrai» et «faux». Une variable de ce type (hors de la théorie) est appelé variable booléenne. Son ajout à la liste des types généralise la notion d'opérateur en para-opérateur. Un connecteur est un para-opérateur dont tous les arguments et les valeurs sont booléens. Un prédicat est un para-opérateur à au moins un argument, tous non booléens, et à valeurs booléennes. Une structure est un opérateur ou un prédicat.
Chaque théorie admet un symbole d'égalité pour chaque type (prédicat à deux arguments de ce type) abusivement tous notés =, interprétés de manière standard. Ce sont les autres structures (désignées par les autres symboles de structure, données arbitraires de chaque théorie et de son modèle) qui font jouer aux éléments de chaque type, un rôle d'objets parfois complexe.
En théorie des ensembles, les ensembles jouent leur rôle par le prédicat binaire ∈ d'appartenance : pour tout élément x et tout ensemble E, on note x ∈ E (x appartient à E, ou x est élément de E, ou E contient x), lorsque x est une valeur possible d'une variable de domaine E.
Les fonctions jouent leur rôle par le foncteur Dom (donnant leurs domaines) et l'évaluateur de fonction, opérateur binaire donnant la valeur f(x) de toute fonction f en tout élément x de Domf.
La théorie des ensembles ZFC se définit comme théorie générique avec un seule type «ensemble», les symboles ∈ et =, et des axiomes. Mais la nôtre ne sera pas générique, et inclura d'autres symboles contribuant à faire jouer leurs rôles aux ensembles, aux fonctions et à d'autres sortes d'objets.
Une théorie du modèle formalisée comme théorie générique donnerait aux types le double rôle de types abstraits et interprétés. Aussi, les mêmes méta-objets pourraient jouer les rôles des symboles de structure et des structures qu'ils désignent (via les méta-structures), sauf que la notion de structure sera étendue à d'autres opérations entre types que celles désignées par les symboles du langage (on ne peut les admettre «toutes» sans dépendre d'un univers extérieur où les trouver, hors sujet ici).

1.2.  <—
Variables, ensembles, fonctions et opérations
Sommaire
—>     1.4.
Termes, formules, connecteurs