1.4. Structures des systèmes mathématiques
Les structures, désignées dans chaque interprétation par les symboles de structure
formant un langage donné, forment un système décrit en reliant les objets des différents types,
donnant leurs rôles aux objets de chaque type en rapport avec ceux d'autres types.
Suivant les détails, les rôles ainsi donnés aux objets de certains types peuvent être compris
comme ceux d'objets complexes, bien que tout cela puisse fonctionner avec de simples objets
comme des urelements.
Structures du premier ordre
Les sortes de structures (et donc aussi les sortes de symboles de structure) autorisées
dans les théories du premier ordre, ainsi appelées structures du premier ordre,
se divisent en opérateurs et prédicats comme décrit plus bas.
Des structures plus puissantes nommées structures du second ordre
seront introduites en 5.1, venant d'outils ensemblistes ou comme paquets
d'un type supplémentaire avec des structures du premier ordre.
Un opérateur est une opération entre des types
interprétés. Au niveau de la théorie avant interprétation, chaque
symbole d'opérateur vient avec son type de symbole formé de
- sa liste d'arguments (symboles de variables figurés comme des espaces
autour du symbole d'opérateur au lieu de noms);
- pour chaque argument, son type (abstrait), dont la valeur comme
ensemble sera le domaine de cet argument dans toute interprétation;
- son type de résultats: le type qui contiendra tous les
résultats de l'opération désignée par ce symbole, dans toute interprétation avec
des valeurs données de ses arguments.
Dans une théorie avec un seul type, cette donnée est réduite à l'arité.
Les symboles de constantes d'une théorie sont ses symboles
d'opérateur nullaires (sans argument).
Les opérateurs unaires (qui sont des fonctions) seront appelés ici
des foncteurs (*).
La liste des types est complété par le type booléen, interprété comme la
paire d'éléments (l'ensemble de deux éléments) qu'on notera 1 pour «vrai» et 0 pour «faux».
Une variable de ce type (hors de la théorie) est appelée une variable
booléenne.
Un para-opérateur est un opérateur au sens généralisé 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
avec au moins un argument mais aucun argument booléen.
Structures de la théorie des ensembles
Formaliser la théorie des ensembles, c'est la décrire comme une théorie avec ses
notions, ses structures et ses axiomes. Nous le ferons dans un cadre logique dédié,
distinct mais convertible en logique du premier ordre par une procédure décrite
en 2.1.
Ceci relie les terminologies de la théorie des ensembles et de la théorie
du modèle, de manière différente de lorsqu'une théorie est interprétée en
théorie des ensembles. Pour garder les noms naturels des notions
ensemblistes (ensembles, fonctions ...) lorsqu'on les définit par cette
formalisation, il deviendrait incorrect de les utiliser encore au sens du lien
précédent (où les notions étaient des "ensembles" et les opérateurs étaient
des "opérations"). Pour éviter toute confusion, utilisons ici uniquement les notions de théorie
des modèles comme notre cadre conceptuel, ignorant leurs interprétations
ensemblistes. Les manières de rassembler ces deux liens, et de réconcilier les
deux conceptions des mêmes théories (descriptions par la théorie des modèles
et interprétations ensemblistes), seront décrites en 1.7 et 1.D.
Admettons 3 notions primitives : éléments (tous les objets),
ensembles et fonctions. Voici leurs principales structures primitives.
Un aspect du rôle des ensembles, est donné par le prédicat binaire ∈
d'appartenance : pour tout élément x et tout ensemble
E, on dit que x est dans E (ou x appartient à
E, ou x est élément de E, ou E contient
x), et on note x ∈ E, pour signifier que
x est une valeur possible des variables de domaine E.
Les fonctions f jouent leur rôle par deux opérateurs : le
foncteur Dom (donnant leurs domaines) et l'évaluateur de fonctions,
opérateur binaire implicite dans la notation f(x), d'arguments
f et x, et donnant la valeur de toute fonction f
en tout élément x de Dom f.
D'autres symboles primitifs seront présentés en 1.7 et 1.8, puis la plupart des autres
symboles primitifs et axiomes seront introduit en 1.A, 2.1, 2.2 et 2.7.
A propos de la théorie axiomatique des ensembles ZFC
La théorie des ensembles de Zermelo-Fraenkel (ZF, ou ZFC avec axiome du
choix) est une 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.
Comme théorie des ensembles assez simplement
exprimable mais très puissante pour un cycle fondateur élargi, elle peut en
effet être un bon choix pour les spécialistes de logique mathématique pour
prouver commodément divers théorèmes
fondationnels difficiles, tels que la non-démontrabilité de certains énoncés,
tout en leur donnant une portée sans doute parmi les meilleures concevables.
Mais malgré l’habitude des auteurs de cours de mathématiques de
base de concevoir leur présentation de la théorie des ensembles comme
une version vulgarisée ou implicite de ZF(C), ce n’est en fait pas une
référence idéale pour un démarrage des mathématiques pour débutants:
- Elle ne peut pas être autonome car elle doit admettre le cadre de la
théorie des modèles pour avoir un sens.
-
Ses axiomes, généralement juste admis (soit comme intuitifs, évidents,
nécessaires ou simplement choisis historiquement pour leur cohérence et la
commodité de leurs conséquences), mériteraient en fait des justifications plus
subtiles et complexes, qui ne peuvent trouver leur place à un point de départ des mathématiques.
- Les mathématiques ordinaires, utilisant beaucoup d'objets habituellement
vus autrement que comme ensembles, ne se développent que de façon
inélégante à partir de 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. La complexité et la bizarrerie
de ces développements nécessaires ne gênent pas les spécialistes
simplement parce que, une fois connus possibles, ils peuvent tout
simplement être tenus pour acquis.
Formalisation des types et structures comme objets de la théorie
du modèle
Pour formaliser la théorie du modèle en utilisant le préfixe
méta-, les méta-notions de "types" et de "structures" reçoivent leurs
rôles par des méta-structures comme suit.
La théorie du modèle supposant une modèle fixe, il lui suffit d’un méta-type
de "types" pour jouer les deux rôles de types abstraits (dans la théorie)
et de types interprétés (composants du modèle), respectivement donnés
par deux méta-foncteurs: l'un des variables vers les types, et l'autre
des objets vers les types. En effet, la notion plus générale d'«ensemble
d'objets» n'est pas utilisée et peut être ignorée.
Mais la méta-notion de structure devra rester distincte du langage, car d'autres
structures que celles nommées dans le langage seront employées (1.5). Les
structures recevront leurs rôles d'opérations, par des méta-structures similaires
à l'évaluateur de fonctions (voir 3.1-3.2 pour une approche), tandis que le
langage (ensembles des symboles de structure) y sera interprété par un
méta-foncteur des symboles de structure vers les structures.
Or, cette seule formalisation laisserait indéterminée l'étendue 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'ensemble des parties (2.5),
mais sa signification dépendra encore de l'univers où il est interprété,
loin de notre préoccupation actuelle pour la théorie du modèle.
Other languages:
EN : 1. First foundations of
mathematics : 1.4. Structures of mathematical
systems