1.4. Structures des systèmes mathématiques

Les structures interprétant le langage d'une théorie (valeurs des symboles de structure dans une interprétation ensembliste), relient les objets de différents types pour former le système étudié. Ces structures font jouer aux objets de chaque type divers rôles dans le système. Suivant ces rôles, les objets peuvent être interprétés comme des objets complexes, malgré leur nature première d'éléments purs.
Les théories génériques admettent 2 sortes de structures (et donc de symboles de structure): les opérateurs et les prédicats.

Un opérateur est une opération entre les types interprétés. Au niveau de la théorie avant interprétation, chaque symbole d'opérateur vient avec les données de son arité (ou liste des arguments présentés comme des espaces autour du symbole), le type abstrait de chaque argument (qui aura pour domaine le type interprété), et le type unique de toutes ses valeurs (résultats de l'opération).
Les symboles de constantes d'une théorie sont ses symboles d'opérateur nulaires.
Les opérateurs unaires (qui sont des fonctions) seront appelés ici des foncteurs (à ne pas confondre avec le concept de foncteur en théorie des catégories).

La liste des types est complété par le type booléen, interprété comme la paire d'éléments 1 («vrai») et 0 («faux»). Une variable de ce type (hors de la théorie) est appelé variable booléenne.
Un para-opérateur est un opérateur généralisé en autorisant le type Booléen parmi ses types d'arguments et de résultats.
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 à valeurs booléennes ayant au moins un argument mais dont aucun n'est booléen.

Structures de la théorie des ensembles

Commençons à formaliser la théorie des ensembles avec 3 notions primitives (sortes d'objets): éléments (tous les objets), ensembles et fonctions. Ce formalisme sera développé progressivement suivant les besoins, avec d'autres notions pouvant être vues comme primitives ou dérivées des premières, et d'autres symboles contribuant à donner leurs rôles aux diverses sortes d'objets. Mais ce travail de formalisation doit s'effectuer en ignorant le procédé d'interprétation ensembliste des théories évoqué ci-dessus, car ces 2 liens entre théorie générique formalisée et théorie des ensembles ne doit pas être confondus (la traduction ensembliste des théories n'est pas encore exercée sur la théorie des ensembles elle-même, cela sera discuté en 1.7).

Un moyen pour la théorie des ensembles de donner aux ensembles leur rôles, est par le prédicat binaire ∈ d'appartenance : pour tout élément x et tout ensemble E, on dit que x dans E (ou x appartient à E, ou x est élément de E, ou E contient x), et on note xE, pour signifier que x est parmi les valeurs d'une variable de domaine E.
Les fonctions f jouent leur rôle par deux opérateurs : le foncteur Dom (donnant leurs domaines) et l'évaluateur de fonction, opérateur binaire implicite dans la notation f(x) ayant pour arguments sont f et x, et donnant la valeur de toute fonction f en tout élément x de Dom f.

A propos de la théorie axiomatique des ensembles ZFC

La théorie axiomatique des ensembles de Zermelo-Fraenkel (ZF, ou ZFC avec axiome du choix) se définit comme théorie générique avec un seul type «ensemble», le symbole de structure ∈, et des axiomes.
Il suppose implicitement que tout objet est un ensemble, et donc un ensemble d'ensembles indéfiniment, construits sur l'ensemble vide.
Les spécialistes de logique mathématique l'ont choisie pour leur besoin d'une théorie puissante dans un cycle fondateur élargi, leur permettant de démontrer beaucoup d'énoncés difficiles ou leur indémontrabilité. Puis, les auteurs de cours de mathématiques de base présentent habituellement la théorie des ensembles comme une forme vulgarisée ou implicite de la théorie ZFC, admise comme référence standard, comme si cela était nécessaire ou évident (comme système axiomatique intuitivement motivé, et historiquement sélectionné pour sa cohérence et la commodité de ses conséquences).
Or pour un démarrage des mathématiques, ZF(C) n'est pas une référence idéale. Ses axiomes (description de l'univers devant présupposer le cadre de la théorie des modèles pour avoir un sens) mériteraient des justifications plus subtiles et complexes que celles habituellement admises. Les mathématiques ordinaires, utilisant beaucoup d'objets souvent vus autrement que comme ensembles, ne se formalisent que de façon inélégante sur cette base. Les rôles de tous les objets utiles pouvant de toute manière être indirectement joués par des ensembles, ils n'ont pas nécessité d'autre formalisation, mais ont laissé un décalage entre la «théorie» et la pratique des mathématiques.

Types en théorie du modèle

La théorie du modèle ignorant la diversité des modèles possibles, sa notion de type peut se formaliser sans utiliser la notion plus générale d'ensemble d'objets (dont les types interprétés sont des cas particuliers), comme une seule méta-notion jouant le double rôle des types abstraits (dans la théorie) et des types interprétés (composants du modèle) : ces rôles sont donnés par des méta-foncteurs, l'un des variables vers les types, et l'autre des objets vers les types. Une forme plus étendue de notions, les classes, sera introduite en 1.7.

Structures en théorie du modèle

De même, le rôle de «structures» (opérations entre types interprétés, avec des valeurs booléennes si un prédicat) peut être formalisée par des méta-structures (similaires à l'évaluateur de fonction).
Contrairement aux types interprétés (tous nommés par types abstraits), notre notion de structure en théorie du modèle sera plus large que celle des valeurs des symboles du langage donné. Pour cela, les structures formeront un autre méta-type, avec un méta-foncteur des symboles vers les structures. Or, cette seule formalisation laisserait indéterminée l'étendue exacte de cette notion de structure.
Essayer de concevoir cette étendue comme celle de «toutes les opérations entre les types interprétés» laisserait inconnue la source de connaissance d'une telle totalité. Cette idée de totalité sera formalisée en théorie des ensembles par l'axiome des parties (2.5.), mais sa signification dépendra encore de l'univers où il est interprété (qu'on suppose contenir toutes les opérations voulues), loin de notre préoccupation actuelle pour la théorie du modèle.
Au lieu de cela, nous fixerons en 1.5 la notion de structure comme donnée par celles définissables par des expressions.

Théorie des ensembles et fondements des mathématiques
1. Premiers fondements des mathématiques
1.1. Introduction aux fondements des mathématiques
1.2. Variables, ensembles, fonctions et opérations
1.3. Forme des théories: notions, objets, méta-objets
1.4. Structures des systèmes mathématiques
1.5. Expressions et structures définissables
1.6. Connecteurs
1.7. Classes en théorie des ensembles
1.8. Symboles liants en théorie des ensembles
1.9. Quantificateurs
1.10. Formalisation de la théorie des ensembles
1.11. Principe de génération des ensembles
 ⇨ Aspects philosophiques
Temps en théorie des modèles
Temps en théorie des ensembles
Interprétation des classes
Concepts de vérité en mathématiques
2. Théorie des ensembles (suite)
3. Théorie des modèles
Other languages:
EN : 1. First foundations of mathematics : 1.4. Structures of mathematical systems