1. Premiers fondements des mathématiques

1.1. Introduction aux fondements des mathématiques

Mathématiques

Les mathématiques sont l'étude des systèmes d'objets élémentaires, dont la seule nature considérée est d'être exacts, sans ambiguïté (deux objets sont égaux ou différents, reliés ou non ; une opération donne un résultat exactement...). Les mathématiques dans leur ensemble peuvent être vus comme «science de tous les mondes possibles» de cette espèce (faits d'objets exacts).
Les systèmes mathématiques sont conçus comme «existant» indépendamment de notre monde habituel ou de toute sensation particulière, mais leur étude nécessite une certaine forme de représentation. Diverses méthodes peuvent être utilisées, pouvant être équivalentes (donnant les mêmes résultats) mais avec divers degrés de pertinence (efficacité) pouvant dépendre des objectifs. Les idées apparaissent habituellement comme intuitions plus ou moins visuelles exprimables par des figures ou animations, puis leurs articulations peuvent s'exprimer en mots ou formules pour être attentivement vérifiées, traitées et communiquées. Pour se libérer des limites ou biais d'une forme de représentation particulière, il suffit de développer d'autres formes de représentation, et de s'exercer à traduire les concepts d'une forme à l'autre. L'aventure mathématique est pleine de jeux de conversions entre diverses formes de représentation, qui peuvent nous initier aux articulations entre les systèmes mathématiques eux-mêmes.

Théories

Les mathématiques se divisent en diverses branches suivant le type de système considéré. Ces cadres de tout travail mathématique peuvent rester implicites (avec des limites floues), ou bien être spécifiés formellement en tant que théories. Chaque théorie est l'étude d'un système (son monde d'objets) supposé fixé, appelé son modèle. Mais chaque modèle d'une théorie peut n'être qu'une de ses interprétations possibles, parmi d'autres modèles également légitimes. Par exemple, en gros, toutes les feuilles de papier sont des systèmes de points matériels, modèles de la même théorie de la géométrie Euclidienne plane, mais indépendants les uns des autres.

Le mot «théorie» peut prendre différents sens entre les utilisations mathématiques et non mathématiques (dans le langage ordinaire et d'autres sciences). Voici la distinction suivant leur nature (sorte générale d'objets); l'autre distinction, par l'intention (réalisme contre formalisme), sera discutée plus loin.

Les théories non-mathématiques décrivent grossièrement ou qualitativement des systèmes ou aspects du monde (domaines d'observation), qui échappent à la description simple et exacte. Par exemple, les descriptions habituelles de la chimie utilisent des approximations drastiques, rassemblant à partir d'observations des effets apparemment arbitraires dont la déduction de la physique quantique est généralement hors de portée des calculs directs. L'absence de distinction claire des objets et de leurs propriétés induit des risques d'erreurs en les approchant et en essayant de déduire certaines propriétés à partir d'autres propriétés, telles que de déduire certaines propriétés globales d'un système à partir de propriétés floues probables de ses parties.

Les théories de mathématiques pures, décrivant des systèmes exacts, peuvent être protégées du risque d'être «fausses», par l'usage de méthodes rigoureuses (règles formelles) conçues pour préserver la conformité exacte des théories à leurs modèles.

Entre les deux, les théories de mathématiques appliquées, telles que les théories physiques, sont aussi des théories mathématiques, mais les systèmes mathématiques qu'elles décrivent sont conçus comme versions idéalisées (simplifiées) d'aspects de systèmes donnés du monde extérieur, négligeant d'autres aspects; suivant sa précision, cette idéalisation (réduction à des mathématiques) permet également des déductions correctes dans des marges d'erreur acceptées.

Fondements et développements

Toute théorie mathématique, décrivant son/ses modèle(s), est faite d’un contenu et est elle-même décrite par un cadre logique. Le contenu d'une théorie est fait de composants qui sont des éléments de description (concepts et informations, décrits en 1.3). Une théorie démarre par le choix d'un fondement formé d'un cadre logique et d'une version initiale du contenu (de préférence petite ou au moins simplement descriptible). Les composants de cette version initiale sont qualifiés de primitifs.
L'étude de la théorie progresse en choisissant certains de ses développements possibles : de nouveaux composants qui résultent de son contenu actuel, et peuvent lui être ajoutés pour former son contenu suivant. Ces différents contenus, ayant la même signification (décrivant essentiellement les mêmes modèles), jouent le rôle de présentations différentes de la même théorie. Les autres développements possibles (non encore choisis) pourront toujours être effectués plus tard, car la partie du fondement qui pouvait les engendrer subsiste. Dès lors la totalité des développements possibles d'une théorie, indépendante de l'ordre choisi pour les effectuer, forme déjà une sorte de «réalité» que ces développements explorent.

Pour exprimer les propriétés de ses modèles, le contenu d'une théorie comprend une liste d'énoncés qui sont des formules annoncées comme vraies dans chaque modèle où elles sont interprétées. Les énoncés primitifs sont appelés axiomes. D'autres énoncés appelés théorèmes s'ajoutent au contenu par développement, à la condition qu'ils soient prouvés (déduits) à partir des précédents: ceci garantit qu'ils soient vrais dans tous les modèles, du moment que les précédents l'étaient. Les théorèmes sont alors utilisables dans les développements suivants au même titre que les axiomes. Une théorie est cohérente (ou consistante) si ses théorèmes ne se contrediront jamais. Les théories incohérentes ne peuvent avoir aucun modèle, un même énoncé ne pouvaut être vrai et faux sur un même système. Le théorème de complétude (1.9, 4.6) montrera que l'ensemble de tous les théorèmes possibles reflète précisément la réalité plus intéressante de la diversité des modèles, qui existent pour toute théorie cohérente.
Les autres sortes de développements (définitions et constructions) ajoutant d'autres composants au-delà des énoncés seront décrits en 1.5, 4.8 et 4.9.

Il y a des hiérarchies possibles entre théories, certaines pouvant jouer un rôle fondateur pour d'autres. Notamment, les fondements de plusieurs théories peuvent avoir une partie commune formant une théorie plus simple, dont les développements sont applicables à toutes.
Un travail fondamental est de développer, à partir d'une base initiale simple, un corps de connaissances commodes pour servir de "fondement" plus complet, muni d'outils efficaces ouvrant des voies plus directes vers d'autres développements intéressants.

Platonisme vs Formalisme

Les mathématiques, ou chaque théorie, peuvent être abordées de deux manières (comme expliqué en 1.9): De nombreux philosophes des mathématiques ont des conceptions obsolètes de telles idées comme formant une multiplicité de croyances opposées (vérités candidates) sur la nature réelle des mathématiques. Mais après examen, il ne reste que ces deux approches nécessaires et complémentaires, avec diverses parts de pertinence suivant les sujets:

Par ses capacités limitées, la pensée humaine ne peut pas directement opérer d'une manière pleinement réaliste sur les systèmes infinis (ou des systèmes finis de taille illimitée), mais nécessite une sorte de logique d'extrapolation, grossièrement équivalente à des raisonnements formels développés à partir de certains fondements; ce travail de formalisation permet d'éviter d'éventuelles erreurs de l'intuition. De plus, les objets mathématiques ne peuvent pas former une totalité achevée, mais seulement un domaine toujours temporaire, en expansion, dont la forme précise est une apparence relative à un choix de formalisation.

Mais au-delà de son incommodité à exprimer les preuves, une vision purement formaliste ne serait pas non plus tenable car la clarté et l’autosuffisance de tout fondement possible (position de départ avec des règles de développement formelles) restent relatives: tout point de départ a dû être choisi plus ou moins arbitrairement, issu de et motivé par une perspective plus large sur les réalités mathématiques; il doit être défini d'une manière intuitive, supposément claire, admettant implicitement son propre fondement, car toute tentative de préciser ce dernier conduirait à une régression sans fin, dont la préexistence réaliste devrait être admise.

Le cycle des fondements

Malgré la simplicité de nature des objets mathématiques, le fondement général de toutes les mathématiques s'avère assez complexe (quoique moins qu'une théorie du tout de la physique). En effet, c'est également une étude mathématique, donc une branche des mathématiques appelée la logique mathématique. Comme toute autre branche, il est riche de définitions et théorèmes sur des systèmes d'objets. Mais comme son objet est la forme générale des théories et des systèmes décrits par celles-ci, il fournit le cadre général de toutes les branches des mathématiques... lui-même inclus. Et pour fournir ainsi le cadre ou fondement de chaque fondement considéré (à l'inverse des travaux mathématiques ordinaires avançant à partir d'un fondement admis), il ne ressemble pas à un point de départ précis, mais à une sorte de vaste cycle composé d'étapes plus ou moins difficiles. Néanmoins, ce cycle des fondements joue bien un rôle fondateur pour les mathématiques, fournissant un cadre rigoureux et de nombreuses notions utiles à diverses branches des mathématiques (outils, inspirations et réponses à diverses questions philosophiques).

(Cette situation ressemble à celle des dictionnaires définissant chaque mot par d'autres mots, ou d'une autre science des systèmes finis: l'informatique. On peut en effet simplement utiliser les ordinateurs, sachant ce qu'on fait mais non pourquoi cela fonctionne; leur fonctionnement se base sur des logiciels qui furent rédigés dans un certain langage puis compilés par d'autres logiciels, et sur le matériel et le processeur dont la conception et la fabrication furent assistées par ordinateur. Et c'est nettement mieux ainsi qu'à la naissance de cette discipline.)

Il est dominé par deux théories:

Chacune est le cadre naturel pour formaliser l'autre: toute théorie des ensembles se formalise comme théorie décrite par la théorie des modèles; celle-ci vient mieux comme développement de la théorie des ensembles (définissant théories et systèmes comme objets complexes), que directement comme théorie. Ces deux liens doivent être considérés séparément : les deux rôles de la théorie des ensembles, comme cadre et comme objet d'étude pour la théorie des modèles, doivent être distingués. Mais ces formalisations nécessiteront un long travail pour être complétées.

1.2. Variables, ensembles, fonctions et opérations

Un démarrage des mathématiques consiste à introduire quelques concepts simples du cycle fondateur, pouvant sembler auto-suffisants autant que possible (alors qu'ils ne peuvent pas l'être absolument). Une solution habituelle et naturelle est de démarrer par une théorie des ensembles non totalement formalisée comme théorie axiomatique. Ce sera fait brièvement en 1.2, expliquant intuitivement les concepts d'ensemble et de fonction. Puis 1.3 introduira les principaux aspects des fondements (théorie des modèles) permettant de formaliser la théorie des ensembles, avec ses principales subtilités (paradoxes).

Constantes

Un symbole de constante est un symbole désignant un objet précis, appelé sa valeur. Exemples: 3, Ø, ℕ. Ceux du langage courant se présentent habituellement comme noms propres et noms avec un article défini singulier («le», «la») sans complément.

Variables libres et liées

Un symbole de variable (ou une variable) est un symbole qui, au lieu d'avoir une valeur donnée a priori, vient avec le concept de valeurs possibles ou d'interprétations possibles comme prenant une valeur particulière. Chaque possibilité lui donne un rôle de constante. Ces possibilités peuvent aussi bien être infiniment nombreuses, ou une seule voire aucune.
On peut l'imaginer comme délimité par une boite dont l'intérieur a plusieurs versions en parallèle, articulant les différents points de vue à son sujet: Plus précisément par rapport à des théories données, fixer une variable signifie prendre une variable libre dans une théorie et ignorer plus longuement sa variabilité, simulant ainsi l'utilisation de l'autre théorie obtenue en acceptant ce symbole comme une constante.
Les divers «points de vue internes», correspondant à chaque valeur possible vue comme fixe, peuvent être considérés comme des «lieux» abstraits dans l'univers mathématique, tandis que la succession de points de vue sur un symbole (le qualifiant comme constante, variable libre ou variable liée), peut être vue comme une première expression de l'écoulement du temps en mathématiques: une variable est liée lorsque tous les «lieux parallèles de l'intérieur de la boite» (valeurs possibles) sont passés. Tous ces lieux et temps sont eux-mêmes des entités purement abstraites et mathématiques.

Domaines et ensembles

On appelle domaine d'une variable, sa signification vue comme liée: c'est la «connaissance» de la totalité considérée de ses valeurs possibles ou autorisées (vues en vrac: sans ordre ni égard à leur contexte) appelées les élements de ce domaine. Cette «connaissance» est une entité abstraite, capable de traiter (d'englober) des infinités d'objets, contrairement à l'esprit humain. Tout domaine d'une variable est appelé un ensemble.
Une variable admet un domaine lorsqu'elle peut être liée: lorsqu'un point de vue englobant toutes ses valeurs possibles est donné. Les variables de la théorie des ensembles n'auront pas toutes un domaine. Une variable sans domaine peut toujours être libre, ce qui n’est plus un statut intermédiaire entre fixe et liée, mais signifie qu’elle peut prendre certaines valeurs ou d’autres valeurs sans prétention d’exhaustivité.

Cantor définissait un ensemble comme «un groupement en un tout d'objets bien distincts de notre intuition ou de notre pensée». «Si la totalité des éléments d'une multiplicité peut être pensée comme «existant simultanément», de telle sorte qu'il soit possible de la concevoir comme un «seul objet» (ou un «objet achevé»), je la nomme une multiplicité consistante ou un «ensemble».» (Nous venons d'exprimer cette «multiplicité» comme celle des valeurs d'une variable).
Il décrivit le cas contraire comme celui d'une «multiplicité inconsistante» où «l'admission d'une coexistence de tous ses éléments mène à une contradiction». Mais la non-contradiction ne peut pas suffire comme définition générale des ensembles: la non-contradiction d'un énoncé n'implique pas sa véracité (l'énoncé contraire peut être vrai mais indémontrable); les faits de non-contradiction sont souvent eux-mêmes indémontrables (théorème d'incomplétude), et deux coexistences séparément consistantes pourraient se contredire (paradoxe de l'omnipotence).

On dit qu'une variable parcourt un ensemble, lorsqu'elle est liée de domaine cet ensemble. On peut introduire à volonté des variables parcourant tout ensemble donné, indépendantes entre elles et des autres variables en présence.
Le renommage systématique d'une variable liée dans tout l'intérieur de sa boite, en un autre symbole inutilisé dans le même contexte (la même boite), de même domaine, ne change pas la signification du tout. En pratique, une même lettre peut représenter plusieurs variables liées séparées (dont les boites sont séparées), qui peuvent prendre des valeurs différentes sans incohérence : il ne s'en trouve nulle part deux libres à la fois où l'on puisse en comparer les valeurs. Le langage courant le fait sans cesse, ne disposant que de fort peu de symboles de variables («il», «elle», ...).

Fonctions

Une fonction est un objet f constitué des données suivantes: Ainsi f est une entité se comportant comme variable dont la valeur est déterminée par celle d'une autre variable appelée son argument de domaine Dom f. Dès que cet argument est fixé (reçoit un nom, ici "x", et une valeur dans Dom f), f devient fixe, notée f(x). Cela revient en fait à concevoir une variable f dont les "vues possibles" comme fixe, sont traitées comme des objets x conceptuellement distincts de la valeur résultante de f. Comme nous le verrons plus tard, une telle entité (variable dépendante) f ne serait pas (traitable comme) un objet de la théorie des ensembles si son argument n'avait pas de domaine, autrement dit ne pouvait pas être lié. (Ce ne serait qu'un méta-objet, ou objet de la théorie des modèles, qu'on appellera un foncteur en 1.4)

Opérations

La notion d'opération généralise celle de fonction, par l'admission d'une liste finie d'arguments (variables de domaines respectifs donnés) au lieu d'un seul. Une opération donne donc un résultat (une valeur) quand tous ses arguments sont fixés. Le nombre n des arguments d'une opération est appelé son arité ; l'opération est dite n-aire. Elle est dite nulaire si n=0 (c'est une constante), unaire si n=1 (c'est une fonction), binaire si n=2, ternaire si n=3...
Les opérations nulaires sont inutiles car leur rôle est déjà joué par leur unique valeur; on verra en 2.1 comment construire celles d'arité > 1 au moyen des fonctions.

La valeur d'une opération binaire f en ses arguments fixés x et y (sa valeur lorsque ses arguments reçoivent les valeurs fixes de x et y), se note f(x,y). Généralement, au lieu de noms, les arguments sont figurés par des espaces autour du symbole, ici les espaces à gauche et à droite dans la parenthèse, à remplir par toute expression leur donnant des valeurs voulues.

Un urelement (élément pur) est un objet ne jouant aucun autre rôle que celui d'élément: ce n'est ni un ensemble, ni une fonction, ni une opération.

1.3. Forme des théories: notions, objets et méta-objets

La variabilité du modèle

Chaque théorie décrit son modèle comme un système fixe. Mais du point de vue plus large de la théorie des modèles, cela n'est qu'un simple «choix» d'un modèle (interprétation) possible dans une diversité (généralement infinie) d'autres modèles existants, également légitimes, de la même théorie. Or, cette fixation du modèle, comme la fixation de toute variable, n’est que l’acte élémentaire de choisir une possibilité, en ignorant le problème de savoir comment spécifier un exemple. En fait, ces «choix» et «existence» de modèles peuvent être très abstraits. En détail, la preuve du théorème de complétude «spécifiera» effectivement un modèle de toute théorie cohérente pour le cas général, mais sa construction nécessitera une infinité d'étapes, dont chacune dépend d'une connaissance infinie. Indépendamment de cette difficulté, l’attitude de fixer implicitement un modèle lorsqu’on étudie formellement une théorie mathématique, reste la manière normale de l'interpréter (sauf en un sens pour la théorie des ensembles comme expliqué plus loin).

Notions et objets

Chaque théorie a sa propre liste de notions, couramment désignées par des noms communs, et qui lui servent formellement de sortes de variables utilisables. Chaque modèle interprète chaque notion comme un ensemble qui est le domaine commun de toutes les variables de cette sorte. Par exemple, la géométrie euclidienne a les notions de «point», «ligne droite», «cercle» et plus, et est généralement exprimée en utilisant un style différent de symbole variable pour chacune. Les objets d'une théorie dans un modèle, sont toutes les valeurs possibles de ses variables de toutes sortes (éléments de toutes ses notions) dans ce modèle.

Théorie du modèle

Toute discussion sur plusieurs théories T et systèmes M modèles possibles de ces T, se place dans la théorie des modèles, avec ses notions de «théorie» et «système» qui sont les sortes respectives des variables T et M. Mais en se concentrant sur une théorie avec un modèle fixe, les variables T et M étant fixées disparaissent de la liste des variables. Leurs sortes, les notions de théorie et de modèle, disparaissent ainsi de la liste des notions. Ceci réduit le cadre, de la théorie des modèles à la théorie du modèle.
Un modèle de la théorie du modèle, est un système [T,M] combinant une théorie T et un modèle M de T.

Sur la diversité des cadres logiques

Le rôle d'un cadre logique, version précise de la théorie du modèle ou des modèles avec sa théorie des preuves, est de décrire Voici ceux que nous présenterons, grossièrement ordonnés du plus pauvre au plus expressif (bien que l'ordre dépende des manières de les relier): Nous allons d'abord décrire les deux principaux cadres logiques en parallèle. La logique du premier ordre est la version la plus courante de la théorie des modèles, décrivant les théories du premier ordre qu'on appellera également ici des théories génériques. La théorie des ensembles, qui peut englober toutes les autres théories, pourra également englober les cadres logiques et ainsi servir elle-même de cadre logique ultime, comme cela sera expliqué en 1.B.
Le qualificatif "ensembliste" visera à qualifier tout concept appartenant à, ou se rapportant à, la théorie des ensembles.
La plupart des cadres gèrent les notions comme des types (habituellement en nombre fini pour chaque théorie), classifiant à la fois variables et objets. Les notions sont appelées des types si chaque objet n'appartient qu'à un seul d'entre eux, qu'on appelle alors aussi le type des variables qui peuvent le désigner. Par exemple, un objet de la géométrie euclidienne peut être un point ou une droite, mais le même objet ne peut être à la fois un point et une droite. Mais la théorie des ensembles aura besoin d'autres notions que les types: les classes, qui seront introduites en 1.7.

Exemples de notions de diverses théories

Théorie Sortes d'objets (notions)
Théorie générique Urelements classés par types pour jouer divers roles
Théorie des ensembles  Eléments, ensembles, fonctions, opérations, relations, uplets...
Théorie des modèles Théories, systèmes et leurs composants (détaillés ci-dessous).
Théorie du modèle Objets, symboles, types ou autres notions, Booléens,
structures (opérateurs, prédicats), expressions (termes, formules)...
Arithmétique Nombres entiers
Algèbre linéaire Vecteurs, scalaires...
Géométrie Points, droites, cercles...

Méta-objets

Les notions d'une théorie du modèle T1, normalement interprétées dans [T,M], classifient les composants de T («type», «symbole», «formule»...) et ceux de M («objet», et des outils pour y interpréter les composants et expressions de T). Mais les mêmes notions (bien que d'une version différente de la théorie du modèle) pourront être interprétées dans [T1, [T,M]], en les marquant du préfixe méta-.

Par sa notion d'«objet», la théorie du modèle distingue les objets de T dans M du reste de ses propres objets dans [T,M] qui sont les méta-objets. La règle ci-dessus d'utilisation du préfixe méta admettrait tout objet comme un méta-objet ; mais on fera une exception de vocabulaire en réservant le nom de méta-objet à ceux qui ne sont pas des objets : symboles, types ou autres notions, Booléens, structures, expressions...

La théorie des ensembles ne connait que les domaines de certaines de ses variables, vus comme objets (ensembles). Mais vue par la théorie du modèle, toute variable d'une théorie a un domaine parmi les notions, qui ne sont que des méta-objets.

Composants des théories

Dans un cadre logique donné, le contenu d'une théorie consiste en 3 listes de composants de sortes suivantes, où ceux de chacune des 2 dernières sortes sont des systèmes finis utilisant ceux de la sorte précédente:

Interprétation ensembliste

Toute théorie générique peut être interprétée (insérée, traduite) en théorie des ensembles, en convertissant ses composants en composants de la théorie des ensembles. C'est l'approche habituelle des mathématiques ordinaires, voyant de nombreux systèmes comme «ensembles avec des relations ou des opérations telles que ...», avec des connexions possibles entre ces systèmes. Présentons à la fois les interprétations génériques applicables à toute théorie générique, et d'autres habituellement préférées pour des théories particulières.

Toute interprétation convertit chaque type abstrait en un symbole (nom) désignant un ensemble appelé type interprété (servant de domaine aux variables de ce type, dont l'usage reste par ailleurs intact). Ce symbole est habituellement une variable fixe dans le cas générique, mais peut être accepté comme symbole de constante de la théorie des ensembles dans des cas particuliers comme les systèmes de nombres (ℕ, ℝ...).
Dans les interprétations génériques, tous les objets (éléments des types interprétés) sont des urelements, mais d'autres sortes d'interprétations dites standard par convention pour des théories particulières peuvent faire autrement. Par exemple, les interprétations standard de la géométrie représentent les points par des urelements, mais représentent les droites par des ensembles de points.

Les interprétations génériques convertiront aussi les symboles de structure en variables fixes (tandis que celles standard peuvent les définir par le langage de la théorie des ensembles). Tout choix de valeurs fixes de tous les types et symboles de structure, définit un choix de système. Lorsque le langage est vu comme un ensemble (en particulier s'il est fini), les modèles deviennent des objets de la théorie des ensembles, dont la multiplicité vient de la variabilité des types et des symboles de structures. Ceci permet d'intégrer toutes les théories voulues dans une même théorie des ensembles, en rassemblant des représentants de tous leurs modèles considérés dans un même modèle de la théorie des ensembles. C'est pourquoi les modèles de la théorie des ensembles sont appelés des univers.

En adoptant la théorie des ensembles comme cadre conceptuel, ce concept "d'interprétation" devient synonyme de choix (désignation) d'un modèle.

1.4. Structures des systèmes mathématiques

Les structures, interprétant chaque structure de symbole d'un langage donné sur une liste de types, forment un système étudié en reliant les objets de certains types, donnant leurs rôles aux objets de chaque type en rapport avec ceux d'autres types. Suivant ces rôles, les objets peuvent être conçus comme objets complexes, bien que n'ayant autrement pas de nature 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, sont classés en opérateurs et prédicats. Elles se décrivent comme des opérations désignées par les symboles de structure dans une interprétation ensembliste. 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 les 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 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 nulaires (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 qu'on notera 1 pour «vrai» et 0 pour «faux». Une variable de ce type (hors de la théorie) est appelée 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 avec au moins un argument mais aucun argument booléen.
Comme sera formalisé en 2.6, un opérateur n-aire f est réductible au prédicat (n+1)-aire (y=f(x1,...,xn)), vrai pour une valeur unique de y pour toutes valeurs choisies de x1,...,xn.

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 admettrons 3 notions primitives : éléments (tous les objets), ensembles et fonctions. Leurs principales structures primitives sont introduites ci-dessous. La plupart des autres symboles primitifs et axiomes seront présentés en 1.7,1.8, 2.1 et 2.2, dans un cadre logique dédié, convertible en logique du premier ordre par une procédure également décrite en 1.10. D'autres composants primitifs s'ajouteront encore ensuite (2.3, 2.6, 2.7, 4.3). Des composants optionnels comme l’axiome du choix (2.12), ouvriront une diversité de théories des ensembles possibles.

Cette approche de la théorie des ensembles comme décrite par la théorie du/des modèles, relie les terminologies des deux théories, de manière différente du lien donné par interprétations des théories génériques en théorie des ensembles. Comme les notions ensemblistes (ensembles, fonctions ...) doivent garder leur nom naturel lorsqu'on les définit par cette formalisation, il deviendrait incorrect de garder cette terminologie pour les utiliser au sens du lien précédent (où les notions étaient des "ensembles" et les opérateurs étaient des "opérations"). Alors pour éviter toute confusion, utilisons ici uniquement les notions de théorie des modèles comme cadre conceptuel, en ignorant leurs interprétations ensemblistes. Nous décrirons en 1.7 et 1.B comment ces deux liens peuvent être mis ensemble, et comment les deux manières de concevoir les mêmes théories (les décrire par la théorie des modèles ou utiliser une interprétation ensembliste), peuvent être réconciliées.

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 xE, 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 fonction, 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.

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:

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.

1.5. Expressions et structures définissables

Termes et formules

Etant donnés les deux premiers niveaux d'une théorie (une liste de types et un langage), une expression (soit un terme soit une formule) est un système fini d'occurrences de symboles, où une occurrence d'un symbole dans une expression, est un lieu où il ce symbole est écrit (par exemple le terme «x+x » comporte 2 occurrences de x et une de +). Chaque expression vient dans le contexte d'une liste de variables libres disponibles donnée. Les expressions des théories du premier ordre et de la théorie des ensembles, peuvent utiliser les symboles des sortes suivantes. Toute expression définira une valeur pour chaque donnée possible de: En logique du premier ordre, appelons symboles logiques les quantificateurs et symboles de para-opérateur hors du langage (égalité, connecteurs et opérateur conditionnel): leur liste et leur signification dans chaque système sont déterminés par le cadre logique et la liste de types donnée, ce qui justifie de ne pas les présenter comme composants de théories particulières.

Esquissons une description plus précise (le cas d'expressions avec uniquement des variables libres et des symboles d'opérateur, appelées termes algébriques, sera formalisé en théorie des ensembles en 4.1 pour un seul type).

Chaque expression contient une occurrence spéciale d'un symbole appelé sa racine, chaque autre occurrence étant la racine d’une unique sous-expression (une autre expression qu’on peut appeler la sous-expression de cette occurrence). Le type d'une expression, qui sera le type de ses valeurs, est donné par le type de résultats de sa racine. Les expressions de type booléen sont des formules ; les autres, de type appartenant à la liste des types donnés, sont des termes (leurs valeurs seront des objets).
Les expressions se construisent successivement, en parallèle entre différentes listes de variables libres disponibles. Les premières et plus simples sont faites d'un seul symbole (comme racine, ayant déjà une valeur par lui-même) : les symboles de constante et de variable sont les premiers termes; les constantes booléennes 1 et 0 sont les plus simples formules.
Les autres expressions se construisent successivement comme formées des données suivantes :

Conventions d'écriture

La présentation de cette liste de sous-expressions directement attachées à la racine nécessite un choix de convention. Pour un symbole de para-opérateur autre qu'une constante : Les parenthèses peuvent aussi servir à distinguer (séparer) les sous-expressions, donc distinguer la racine de chaque expression parmi les autres occurrences de symboles. Par exemple la racine de (x+y)n est l'opérateur de puissance.

Structures variables

Seuls quelques objets sont habituellement nommés par les symboles de constantes d'un langage donné. Tout autre objet peut être nommé par un symbole de variable fixe, dont le statut dépend du choix de la théorie dans laquelle on se place: La différence disparait dans les interprétations génériques qui convertissent les constantes en variables (dont les valeurs définissent différents modèles).
Par analogie avec les constantes qui sont des structures particulières (opérateurs nulaires), le concept de variable se généralise en celui de structure variable. Mais ceux au-delà des opérations nulaires échappent à la liste ci-dessus des symboles admis dans les expressions. Cependant, certains types d'utilisation de symboles de structure variable peuvent être justifiés comme d'abréviations (descriptions indirectes) de l'utilisation d'expressions légitimes. Le cas principal de ceci est expliqué ci-dessous, formant un développement de la théorie; d’autres utilisations possibles seront introduites en 1.10 (l'interprétation d’une utilisation comme abréviation d’autres travaux revient à utiliser une version développée du cadre logique).

Structures définies par des expressions

Dans toute théorie on peut légitimement introduire un nouveau symbole, désignant soit une structure variable (opérateur ou prédicat), soit une variable booléenne (prédicat nulaire, pas une "structure") comme abréviation de, donc définie par, les données suivantes: La variabilité du symbole est l'abréviation de celle de tous ses paramètres.

En théorie des ensembles, toute fonction f est synonyme du foncteur défini par le terme «f(x)» d'argument x et de paramètre f (mais le domaine de ce foncteur est Dom f au lieu d'un type). Les termes sans argument définissent de simples objets (opérateurs nulaires); celui fait d'une variable d'un type donné, vu comme paramètre, suffit pour donner tous les objets de ce type.

Considérons maintenant la méta-notion de "structure" en théorie du modèle, et donc celles d '"opérateur" et de "prédicat", comme devant contenir toutes les structures ainsi atteignables: définies par toute expression avec toutes les valeurs possibles des paramètres. La version minimale d'une telle méta-notion peut être formalisée comme un rôle attribué aux données d'une expression avec les valeurs de ses paramètres. Comme elle fait appel à l'ensemble infini de toutes les expressions, elle échappe (est généralement inaccessible) aux capacités de la théorie étudiée (qui ne peut utiliser qu'une expression à la fois) : aucune expression ne peut suffire. De plus en interprétant cela en théorie des ensembles, encore d'autres d'opérations (indéfinissables) entre types interprétés existent généralement dans l'univers. Parmi les rares exceptions, le domaine ensembliste complet d'une structure variable dont tous les arguments parcourent des ensembles finis (comme types interprétés) avec des limites de taille données, peut être atteinte par une expression dont la taille dépend de ces limites.

Structures invariantes

Une structure invariante d'un système donné (langage interprété), est une structure définie à partir de son langage sans paramètre (donc constante). Cette distinction des structures invariantes parmi les autres structures, généralise la distinction entre les constantes et les variables, à la fois aux cas d'arité non nulle, et à ce qui peut être défini par des expressions plutôt que directement nommé dans le langage.

En effet toute structure désignée par un symbole du langage est directement définie par lui sans paramètre, et donc invariante. Comme sera détaillé en 4.8, les théories peuvent être développées par des définitions, consistant à nommer une autre structure invariante par un nouveau symbole ajouté au langage. Parmi les aspects de la signification préservée de la théorie, figurent les méta-notions de structure, structure invariante, et l'ensemble des théorèmes exprimables avec le langage précédent.

1.6. Connecteurs logiques

Nous avons défini précédemment le concept de connecteur logique. Énumérons maintenant les principaux connecteurs utiles, au-delà des deux connecteurs nullaires (constantes booléennes) 1 et 0. (A cela s'ajoutera le connecteur conditionnel en 2.1).

Tautologies

Leurs propriétés seront exprimées par des tautologies, qui sont des formules utilisant uniquement des connecteurs et des variables Booléennes (ici écrites A, B, C), et vraies pour toutes les combinaisons de valeurs possibles de ces variables. Ainsi, les tautologies donnent également des formules nécessairement vraies après remplacement de ces variables par des formules les définissant utilisant n'importe quel langage et interprétées dans tout système. De telles définitions des variables booléennes par les formules d'une théorie peuvent restreindre leurs domaines de valeurs possibles dépendant les unes des aux autres.

Les tautologies constituent les règles de l'algèbre booléenne, une théorie algébrique décrivant les opérations sur le type booléen, naturellement interprétée comme la paire d'éléments 0 et 1, mais admettant également des interprétations plus sophistiquées dépassant le cadre de ce chapitre.

Le connecteur binaire d'égalité entre booléens est noté ⇔ et appelé équivalence : AB se lit «A équivaut à B».

Negation

Le seul connecteur unaire utile est la negation ¬, qui échange les booléens (¬A se lit «non A»):
¬1
¬0
¬(¬A)
⇔ 0
⇔ 1
A
Il est souvent noté en barrant le symbole principal de son argument, formant avec lui un autre symbole de même format:
xy
xE
(AB)
⇔ ¬(x=y)
⇔ ¬(xE)
⇔ (A ⇔ ¬B)
(x est différent de y)
(x n'appartient pas à E)
(Non-équivalence)

Conjonctions, disjonctions

La conjonction ∧ signifie «et», donnant vrai uniquement si ses deux arguments sont vrais;
La disjonction ∨ signifie «ou», donnant vrai sauf si ses deux arguments sont faux.
Chacun est:
Idempotent
(AA) ⇔ A
(AA) ⇔ A
Commutatif
(BA) ⇔ (AB)
(BA) ⇔ (AB)
Associatif
((AB)∧C) ⇔ (A∧(BC))
((AB)∨C) ⇔ (A∨(BC))
Distributif sur l'autre
(A ∧ (BC)) ⇔ ((AB) ∨ (AC))
(A ∨ (BC)) ⇔ ((AB) ∧ (AC))

Cette ressemblance (symétrie) de leurs propriétés vient du fait qu'ils sont échangés par négation:

(AB) ⇎ (¬A ∧ ¬B)
(AB) ⇎ (¬A ∨ ¬B)

L'inéquivalence ⇎ est aussi appelée «ou exclusif» car (AB) ⇔ ((AB) ∧ ¬(AB)).

Les chaines de conjonctions comme (ABC) abrègent toute formule avec plus de parenthèses comme ((AB) ∧ C), équivalentes entre elles par associativité; de même pour les chaines de disjonctions (ABC).

Affirmer (déclarer vraie) une conjonction de formules revient à affirmer successivement toutes ces formules.

Implication

Le connecteur binaire d'implication ⇒ se definit par (AB) ⇔ ((¬A) ∨ B). Il peut se lire «A implique B», «A est une condition suffisante à B», ou «B est une condition nécessaire à A». Etant vrai sauf quand A est vrai et B est faux, il exprime la vérité de B quand A est vrai, mais il ne donne plus d'information sur B quand A est faux (étant alors vrai).
De plus,
(AB) ⇎
(AB) ⇔
(A ∧ ¬B)
B ⇒ ¬A)
La formule (¬B ⇒ ¬A) est appelée la contraposée de (AB).
L'équivalence peut aussi se redéfinir par
(AB) ⇔ ((AB) ∧ (BA)).
Ainsi dans une théorie donnée, une preuve de AB peut se former d'une preuve de la première implication (AB), puis une preuve de la deuxième (BA) appelée la réciproque de (AB).

La formule (A ∧ (AB)) sera abrégée en AB, qui se lit «A donc B». Elle est équivalente à (AB), mais sert à indiquer qu'elle est déduite des vérités de A et de (AB).

Les négations transforment les formules d'associativité et de distributivité des conjonctions et disjonctions en diverses tautologies avec des implications:

(A ⇒ (BC)) ⇔ ((AB) ⇒ C)
(A ⇒ (BC)) ⇔ ((AB) ∨ C)

(A ⇒ (BC)) ⇔ ((AB) ∧ (AC))
((AB) ⇒ C) ⇔ ((AC) ∧ (BC))
((AB) ⇒ C) ⇔ ((AC) ∧ (BC))
(A ∧ (BC)) ⇔ ((AB) ⇒ (AC))
Enfin on a
(AB) ⇒ ((AC) ⇒ (BC))
(AB) ⇒ ((AC) ⇒ (BC)).

Chaines d'implications et d'équivalences

Par une autre sorte d'abréviation, toute chaine de formules reliées par des ⇔ et/ou ⇒, abrégera la conjonction de toutes ces implications ou équivalences entre formules voisines:

(ABC) ⇔ ((AB) ∧ (BC)) ⇒ (AC)
(ABC) ⇔ ((AB) ∧ (BC)) ⇒ (AC)
0 ⇒ AA ⇒ 1
A) ⇔ (A ⇒ 0) ⇔ (A ⇔ 0)
(A ∧ 1) ⇔ A ⇔ (A ∨ 0) ⇔ (1 ⇒ A) ⇔ (A ⇔ 1)
(AB) ⇒ A ⇒ (AB)

1.7. Classes en théorie des ensembles

Pour toute théorie, une classe est un prédicat unaire A vu comme ensemble des objets où A est vrai, à savoir «la classe des x tels que A(x)».
Notamment en théorie des ensembles, tout ensemble E est synonyme de la classe des x tels que xE (définie par la formule xE, d'argument x et de paramètre E). Mais cela utilise deux interprétations différentes de la notion d'ensemble, qui doivent être distinguées comme suit.

Univers standard et méta-ensembles

Interpréter (insérer) la théorie des ensembles dans elle-même, nécessite d’articuler deux interprétations (modèles) de la théorie des ensembles, qui seront distingués en donnant le préfixe méta à l'interprétation dans le rôle de cadre. Outre les interprétations génériques, la théorie des ensembles a un type standard d'interprétation dans elle-même où chaque ensemble est interprété par la classe (méta-ensemble) de ses éléments (l'objet et le méta-objet synonymes sont alors égaux), et chaque fonction est interprétée par sa méta-fonction synonyme. Ainsi, tout ensemble sera une classe, toute classe étant un méta-ensemble d'objets. Mais certains méta-ensembles d'objets ne sont pas des classes (n'étant définissables par aucune formule avec paramètres); et certaines classes ne sont pas des ensembles, par exemple la classe des ensembles (voir le paradoxe de Russell en 1.8), ou l'univers (classe de tous les objets, définie par 1).

Classes d'admissibilité

La théorie des ensembles accepte tous les objets comme «éléments» pouvant appartenir à des ensembles et être opérés par des fonctions (pour éviter les divisions sans fin entre ensembles d'éléments, ensembles d'ensembles, de fonctions, ensembles mixtes...). Cela serait formalisable en gardant 3 types (éléments, ensembles et fonctions) où chaque ensemble aurait une copie comme élément, identifiée par un foncteur des ensembles vers les éléments, et de même pour les fonctions. Mais au-delà de ces types, notre théorie des ensembles aura de toute façon besoin d'autres notions comme domaines de ses structures, qui ne peuvent être commodément formalisées que comme classes. Ainsi les notions d'ensemble et de fonction seront des classes désignées par des symboles de prédicats:

Set = «est un ensemble»
Fnc = «est une fonction»

En logique du premier ordre, toute expression est assurée de prendre une valeur définie, pour chaque donnée d'un modèle et de valeurs de ses variables libres dedans (en raison de sa correction syntaxique implicite dans le concept d '«expression»). Mais en théorie des ensembles, cela peut encore dépendre des valeurs des variables libres.
Ainsi une expression A (et toute structure qu'elle définit) sera dite admissible si elle a effectivement une valeur pour les valeurs données de ses variables libres (vues comme arguments et paramètres de toute structure qu'elle définit). Cette condition est elle-même un prédicat partout admissible, exprimé par une formule dA avec les mêmes variables libres. En choisissant une d'elles comme argument, la classe qu'elle définit est le méta-domaine, appelé classe d'admissibilité, de la structure unaire définie par A.
Les expressions ne doivent être employées que là où elles sont admissibles, ce qui se fera assez naturellement. La condition d'admissibilité de (xE) est Set(E). Celle de l'évaluateur de fonction f(x), est (Fnc(f) ∧ x ∈ Dom f).
Mais l'admissibilité de cette dernière formule nécessite une justification, donnée plus bas.

Admissibilité étendue

Une théorie aux structures partiellement admissibles, comme la théorie des ensembles, peut être formalisée (traduite) en théorie avec un seul type et des structures partout admissibles, gardant intactes les expressions et leurs valeurs partout où elles sont admissibles : les modèles se traduisent dans un sens en donnant des valeurs arbitraires aux structures non admissibles (par exemple une valeur constante), et en sens inverse en ignorant ces valeurs. Ainsi, une expression comportant une sous-expression non admissible peut être déclarée admissible si sa valeur finale ne dépend pas de ces valeurs ajoutées.
En particulier, pour toutes formules A et B on considèrera les formules AB et AB comme admissibles si A est faux, de valeurs respectives 0 et 1, même si B n'est pas admissible. Donnons leur ainsi la même condition d'admissibilité (dA ∧ (AdB)) (rompant, pour «et», la symétrie entre A et B qu'il est inutile de rétablir). Cette formule est rendue admissible par la même règle dès lors que dA et dB étaient admissibles. Ainsi les deux formules

A ∧ (BC)
(AB) ∧ C

ont la même condition d'admissibilité (dA ∧ (A ⇒ (dB ∧ (BdC)))).

Les classes seront définies par des prédicats unaires partout admissibles, facilement exprimables par la règle ci-dessus comme suit.
Tout prédicat A peut être étendu au-delà de son domaine d'admissibilité, sous la forme dAA (donnant 0) ou dAA (donnant 1).
Pour toute classe A et tout prédicat unaire B admissible sur tout A, la classe définie par AB est appelée la sous-classe de A définie par B.

1.8. Symboles liants en théorie des ensembles

Syntaxe des symboles liants

Cette dernière sorte de symbole peut former une expression en prenant un symbole de variable, disons ici x, et une expression F pouvant utiliser x comme variable libre (en plus des variables libres disponibles à l’extérieur), pour donner une valeur dépendant de la structure unaire définie par F d'argument x. Ainsi, il sépare la sous-expression «intérieure» F ayant x parmi ses variables libres, de l'«extérieur» où x est liée. Mais dans la plupart des cas (la plupart des théories...), les symboles liants ne peuvent pas conserver la donnée complète de cette structure unaire, trop complexe pour être enregistrée comme objet, comme expliqué ci-dessous.

Nous présenterons d’abord les deux principaux symboles liants en théorie des ensembles: le symbole de compréhension et le définisseur de fonctions. Puis, 1.9 présentera les deux principaux quantificateurs. Enfin 1.10 et 1.11 donnera des axiomes complétant cette formalisation des notions d’ensemble et de fonction en théorie des ensembles.

La syntaxe diffère entre la logique du premier ordre et la théorie des ensembles, qui gèrent le domaine des variables différemment. En logique du premier ordre, les domaines sont des types, données implicites des quantificateurs. Mais les domaines des symboles liants en théorie des ensembles sont des ensembles qui, comme objets, sont désignés par un argument supplémentaire du symbole (un espace pour un terme n'utilisant pas la variable à lier).

Symbole de compréhension

Pour tout prédicat unaire A admissible dans un ensemble E, la sous-classe de E définie par A est un ensemble: c'est le domaine d'une variable x introduite comme parcourant E, donc liable, dont on sélectionne les valeurs satisfaisant A(x). C'est donc un sous-ensemble ou une partie de E, noté {xE | A(x)} (ensemble des x dans E tels que A(x)): pour tout y,

y ∈ {xE|A(x)} ⇔ (yEA(y))

Cette combinaison de caractères { ∈  |  } forme la notation d'un symbole liant appelé symbole de compréhension : {xE | A(x)} lie x de domaine E sur la formule A.

Paradoxe de Russell

Si l'univers (classe de tous les éléments) était un ensemble alors en l'utilisant, le symbole de compréhension pourrait convertir en ensembles toutes les classes, dont la classe de tous les ensembles. Mais c'est impossible, comme on peut montrer à l'aide du symbole de compréhension lui-même :

Théorème. Pour tout ensemble E il existe un ensemble F tel que FE. Ainsi aucun ensemble E ne peut contenir tous les ensembles.

Preuve. F={xE | Set(x) ∧ xx} ⇒ (FF ⇔ (FEFF)) ⇒ (FFFE). ∎

Cela nous obligera à préserver les distinctions entre ensembles et classes.

Définitions des fonctions par des termes

Le définisseur de fonction (  ∋   ↦  ) lie une variable sur un terme, suivant la syntaxe (Ext(x)) où Admissible si t(x) est admissible pour tout x dans E, il prend alors le foncteur défini par t et restreint son domaine (classe d'admissibilité) à E, pour donner une fonction de domaine E.
Il convertit donc les foncteurs en fonctions, à l'inverse du rôle de l'évaluateur de fonction (avec le foncteur Dom) qui convertissait (interprétait) les fonctions en leur rôle (signification) comme foncteurs dont les classes d'admissibilité étaient des ensembles.
La notation abrégée xt(x) peut être utilisée lorsque E est déterminé par le contexte, ou dans une méta-description pour désigner un foncteur en spécifiant l'argument x du terme qui le définit.

Relations

Une relation est un objet de la théorie des ensembles semblable à une opération mais à valeurs booléennes: il joue un rôle de prédicat dont les classes d'admissibilité (domaines des arguments) sont des ensembles (les prédicats peuvent ainsi se décrire comme relations entre types interprétés).

Les relations unaires (fonctions à valeurs booléennes), seront représentées par des sous-ensembles S de leur domaine E, en utilisant le symbole de compréhension comme définisseur, et ∈ comme évaluateur interprétant S comme prédicat x ↦ (xS). Ce rôle de S diffère encore de la relation unaire voulue, ignorant son domaine E, mais étant admissible dans tout l'univers, valant 0 hors de E. Cette absence d'opérateur Dom n'a pas d'importance, E étant généralement connu par le contexte (comme variable disponible).

Comme le définisseur de fonction (resp. le symbole de compréhension) enregistre toute la structure définie par l'expression donnée sur l'ensemble donné, il suffit à définir tout autre symbole liant ensembliste de même domaine sur la même expression, comme composé d'une structure unaire appliquée à son résultat (qui est une fonction, resp. un ensemble).

1.9. Axiomes et preuves

Enoncés

Une expression est close, si sa liste de variables libres est vide (toutes ses variables sont liées), de sorte que sa valeur ne dépend que du système où elle est interprétée.
En logique du premier ordre, un énoncé est une formule close. Il aura donc une valeur booléenne (vrai ou faux) dépendant uniquement du choix d'un système interprétant son langage.
La liste des axiomes d'une théorie est un ensemble d'énoncés, présentés comme tous vrais dans certains systèmes donnés (modèles de la théorie comme discuté plus bas).

Démontrabilité

Une preuve ou démonstration d'un énoncé A dans une théorie T, est un modèle fini d'une théorie de la démonstration, présentant A en "conclusion" et utilisant une liste finie d'axiomes parmi ceux de T.
Comme expliqué plus loin (et précisément étudié par les spécialistes), le concept de preuve peut être entièrement formalisé (une théorie de la démonstration peut être écrite en détails), ce qui peut prendre la forme d'un algorithme de vérification de preuves (n'utilisant qu'une quantité de ressources liée à la taille d'une preuve donnée). Mais la plupart des travaux mathématiques ne sont que partiellement formalisés: on utilise des preuves semi-formelles, juste assez rigoureuses pour donner l’impression qu’une formalisation complète est possible sans l'avoir en fait rédigée; une vision intuitive d'un problème peut sembler plus claire qu'un raisonnement formel. De même, ce travail présentera des preuves naturellement sans formalisation complète explicite : utilisant parfois des articulations en langage courant, elles seront principalement écrites sous forme d’une succession d’énoncés, chacun visiblement vrai à l'aide des précédents, de prémisses, d'axiomes, de théorèmes connus, et de règles de preuve, notamment celles des quantificateurs (1.10). Mais sans détailler une théorie de la démonstration, voyons-en quelques propriétés générales.

On dit que A est démontrable (ou ) dans T, ou un théorème de T, et on note TA s'il existe une preuve de A dans T. C’est la condition d’arrêt d’un algorithme de recherche de preuve, opéré par un "ordinateur" abstrait aux temps et ressources disponibles illimités (infinis), essayant chaque morceau de preuve possible jusqu’à éventuellement trouver une preuve valide de l'énoncé donné.

En pratique, seuls sont qualifiés de théorèmes les énoncés connus comme tels, c'est-à-dire dont on connait une preuve. Mais des synonymes de "théorème" sont traditionnellement utilisés pour les qualifier suivant leur importance: un théorème est plus important qu'une proposition. L'un ou l'autre peuvent se déduire d'un lemme autrement moins important, et implique facilement un corolaire aussi moins important.

Toute bonne théorie de la démonstration doit bien entendu être correcte, à savoir qu'elle ne peut "prouver" que des énoncés toujours vrais: la démontrabilité implique la vérité dans chaque modèle (où tous les axiomes sont vrais).

Validité logique

Pour un langage donné L, un énoncé A est dit logiquement valide, s'il est démontrable avec L sans utiliser d'axiome. On pourrait noter cela ⊢ A mais par mesure d'exactitude il faut l'écrire LA (signifiant que A est théorème de la théorie faite de L sans axiome, donc de toute autre théorie contenant L), Alors, A est vrai dans tous les systèmes interprétant L de par le caractère correct du cadre logique. Les plus simples énoncés logiquement valides sont les tautologies (dont les variables Booléennes sont remplacées par des énoncés); d'autres seront donnés en 1.10.

Une preuve de A utilisant certains axiomes peut être vue comme une preuve de (conjonction de ces axiomes ⇒ A) sans axiome, rendant cette implication logiquement valide.

Réfutabilité et cohérence

Une réfutation de A dans T, est une preuve de ¬A. S'il en existe (T ⊢ ¬A), l'énoncé A est dit réfutable (dans T).
Un énoncé est dit décidable (dans T) s'il est démontrable ou réfutable.
Une théorie T is est dite contradictoire ou inconsistante si T ⊢ 0, sinon est est dite cohérente.
Si un énoncé est à la fois démontrable et réfutable dans T alors tous le sont, car cela signifie que la théorie est contradictoire, indépendamment de l'énoncé choisi :

(A ∧ ¬A) ⇔ 0
((TA) ∧ (TB)) ⇔ (TAB)
((TA) ∧ (T ⊢ ¬A)) ⇔ (T ⊢ 0).

Dans une théorie contradictoire, tout énoncé est démontrable. Son cadre étant correct, une telle théorie n'a aucun modèle.
Une réfutation de A dans T peut être aussi vue comme une contradiction de la théorie TA obtenue en ajoutant A aux axiomes de T.

Théories réalistes vs axiomatiques en mathématiques et autres sciences

Après la distinction de nature (mathématique ou non), les théories peuvent également différer selon l'intention de leur usage, entre réalisme et formalisme :

Une théorie axiomatique est une théorie donnée avec une liste d'axiomes visant à définir sa diversité de modèles, comme classe de tous les systèmes, interprétant le langage donné, où tous les axiomes sont vrais (rejetant ceux où un axiome est faux). Cela rend automatique la véracité des axiomes dans chaque modèle. Les théories non-réalistes en dehors des mathématiques (non qualifiées d'axiomatiques par manque de précision mathématique) seraient des œuvres de fiction décrivant des systèmes imaginaires ou futurs possibles.

Une théorie réaliste est une théorie visant à décrire un système fixe ou une classe de systèmes, vus comme donnés par une réalité indépendante. Ses axiomes sont des énoncés qui, pour certaines raisons, sont considérés connus comme vrais sur ces systèmes. Une telle théorie est "vraie" si tous ses axiomes y sont effectivement vrais. Ces systèmes sont ainsi des modèles, qualifiés de standard par contraste avec les autres modèles non voulus de cette théorie prise axiomatiquement.
Cette véracité sera généralement assurée pour les théories réalistes des mathématiques pures : arithmétique et théorie des ensembles (bien que la signification réaliste de la théorie des ensembles ne soit pas toujours claire suivant les axiomes considérés). Ces théories s'avèreront admettre également des modèles non standard, donnant une différence effective entre leurs significations réaliste et axiomatique.

Hors des mathématiques pures, la véracité des théories réalistes peut être douteuse (discutable): les énoncés non mathématiques sur des systèmes non mathématiques peuvent être ambigus (mal définis), tandis que la vérité des théories des mathématiques appliquées peut être approximative, ou encore spéculative comme les systèmes "réels" voulus peuvent être inconnus (contingents parmi d'autres systèmes possibles). Une telle théorie est dite falsifiable si en principe, le cas de sa fausseté peut être découvert en comparant ses prédictions (théorèmes) avec les observations.
Par exemple, la biologie est relative à un grand nombre de choix aléatoires discrètement accumulées par la nature sur Terre pendant des milliards d'années. Elle contient de nombreux "axiomes", falsifiables et qui nécessitent de nombreux tests empiriques.

La géométrie euclidienne fut d'abord conçue comme théorie réaliste de mathématiques appliquées (pour son rôle de première théorie physique), puis fut comprise comme une théorie axiomatique de mathématiques pures parmi diverses autres géométries mathématiquement tout aussi légitimes; tandis que l'espace physique réel est plus précisément décrit par la géométrie non-euclidienne de la Relativité Générale.

1.10. Quantificateurs

Un quantificateur est un symbole liant exercé sur un prédicat unaire (une formule) et à valeurs booléennes.
En théorie des ensembles, la syntaxe complète d'un quantificateur Q liant une variable x de domaine E sur un prédicat unaire A, est

QxE, A(x)

A(x) abrège la formule définissant A, dont les variables libres sont x et d'éventuels paramètres.
Une notation plus condensée met le domaine en indice (QEx, A(x)), ou l'élimine (Qx,A(x)) quand il peut être sous-entendu (sans importance, ou fixé par le contexte, notamment un type dans une théorie générique).
Les deux principaux quantificateurs (par lesquels d'autres seront définis ensuite) sont: Le quantificateur universel de la théorie des ensembles peut être vu comme défini par le symbole de compréhension :

(∀xE, A(x)) ⇔ {xE | A(x)} = E.

Celui de la logique du premier ordre peut se définir dans un cadre ensembliste en regardant A comme une fonction, et ses valeurs booléennes comme des objets:

(∀x, A(x)) ⇔ A = (x ↦ 1)

La formule (∀x,1) est toujours vraie.
∃ peut se définir à partir de ∀ avec le même domaine: (∃x, A(x)) ⇎ (∀x, ¬A(x)).
Donc (∃x, A(x)) ⇔ A ≠ (x ↦ 0).
Avec des classes,
(∃C x, A(x))
(∀C x, A(x))
x, (C(x)
⇔ (∃x, C(x) ∧ A(x)) ⇔ ∃CA x, 1
⇔ (∀x, C(x) ⇒ A(x))
⇔ (∃C y, x=y))

Inclusion entre classes

Une classe A est dite incluse dans une classe B si ∀x, A(x) ⇒ B(x). Alors A est une sous-classe de B car ∀x, A(x) ⇔ (B(x) ∧ A(x)). Réciproquement, toute sous-classe de B est incluse dans B.
L'inclusion de A dans B entraîne pour tout prédicat C (en cas d'admissibilité):

(∀B x, C(x)) ⇒ (∀A x, C(x))
(∃A x, C(x)) ⇒ (∃B x, C(x))
(∃C x, A(x)) ⇒ (∃C x, B(x))
(∀C x, A(x)) ⇒ (∀C x, B(x))

Règles de preuves pour les quantificateurs sur un prédicat unaire

Tout comme les expressions furent décrites en permettant de prendre des expressions déjà faites pour en former de nouvelles, on peut formaliser le concept de preuve en utilisant des preuves déjà connues pour en former de nouvelles. Voici quelques "règles" intuitivement introduites, toujours sans prétendre formaliser entièrement les preuves.

Introduction existentielle. Si on a des termes t, t′,… et une preuve de (A(t) ∨ A(t′) ∨ …), alors x,A(x).

Elimination existentielle. Si x, A(x), alors on peut introduire une nouvelle variable libre z avec l'hypothèse A(z) (les conséquences seront justes, sans restreindre la généralité).

Ces règles traduisent le sens de ∃ : le passage de t, … à ∃ puis de ∃ à z, revient à abréger par z un des termes t, … (sans savoir lequel). Elles donnent le même sens à ∃C qu'à ses 2 formules équivalentes ci-dessus, court-circuitant (rendant implicite) la règle d'admissibilité étendue de (CA) en se concentrant sur le cas où C(x) est vrai et donc A(x) est admissible.
La validité logique dépend du langage parce que, avec un seul type

(L ⊢ ∃x, 1) ⇔ (un symbole de constante existe dans L)

(Avec plus de types, la condition est plus compliquée.)

Alors que ∃ apparaissait comme désignation d'objet, ∀ se présente comme une règle de déduction: ∀C x, A(x) signifie que sa négation ∃C x, ¬A(x) entraine une contradiction.

Introduction universelle. Si de la seule hypothèse C(x) sur une nouvelle variable libre x on a pu déduire A(x), alors C x, A(x).

Elimination universelle. Si C x, A(x) et t est un terme satisfaisant C(t), alors A(t).

Introduire puis éliminer ∀ revient à remplaçer x par t dans la démonstration initiale.

On peut ainsi faire des déductions par ces règles, reflétant les formules

((∀C x, A(x)) ∧ (∀C x, A(x) ⇒ B(x))) ⇒ (∀C x, B(x))
((∃C x, A(x)) ∧ (∀C x, A(x) ⇒ B(x))) ⇒ (∃C x, B(x))
(∀C x, A(x)) ∧ (∃C x, B(x))) ⇒ (∃C x, A(x) ∧ B(x))
(∃A x, ∀B y, R(x,y)) ⇒ (∀By, ∃A x, R(x,y))

Complétude de la logique du premier ordre

Au-delà de la qualité indispensable de correction de la partie théorie de la démonstration d'un cadre logique, plus remarquable est sa qualité réciproque de complétude: pour toute théorie axiomatique qu'il décrit, tout énoncé vrai dans tous les modèles est démontrable. Autrement dit, tout énoncé non démontable est faux quelque part et tout énoncé irréfutable est vrai quelque part. Ainsi, toute théorie cohérente a des modèles existants, mais souvent une diversité de ceux-ci, car tout énoncé indécidable est vrai dans certains et faux dans d'autres. Ajouter des énoncés indécidables aux axiomes conduit à différentes théories cohérentes pouvant être «en désaccord» sans conflit, descriptions correctes de systèmes différents qui «existent» également.

La logique du premier ordre a été trouvée complète, ce qu'exprime le théorème de complétude, qui était à l’origine la thèse de Gödel: à partir d’un concept de «démonstration» convenablement formalisé, la classe résultante de théorèmes (potentiels) de toute théorie du premier ordre se trouve être celle "parfaite", coïncidant à celle des énoncés universellement vrais (vrais dans tous les modèles). A cette qualité de la logique du premier ordre s'ajoute sa capacité à exprimer toutes les mathématiques : tout cadre logique plus puissant peut de toute façon être développé depuis la théorie des ensembles (ou plus directement ses théories peuvent être interprétées en théorie des ensembles) elle-même traduisible en une théorie du premier ordre. De là son importance centrale dans les fondements des mathématiques: sa complétude résout le gros des divergences a priori entre platonisme et formalisme pour les théories axiomatiques du premier ordre, tout en donnant un sens clair et naturel aux concepts a priori intuitifs de «démonstration», «théorème» et «cohérence».

Une telle théorie de la démonstration pour la logique du premier ordre est essentiellement unique: l'équivalence entre deux versions (correctes et complètes) concernant l'existence d'une preuve dans toute théorie T, apparaît concrètement par la possibilité de traduire toute "preuve" pour l'une en une "preuve" pour l'autre. Parmi les formalisations possibles des preuves, se trouvent des formules V(p,s) de l'arithmétique du premier ordre (la théorie du premier ordre décrivant le système ℕ des entiers naturels à quatre symboles 0, 1, +, ⋅ avec axiomes énumérés en 4.3 et 4.4), signifiant que le nombre p code une preuve valide d'un énoncé codé par le nombre s, dépendant des symboles de prédicats unaires t,l,a qui codent les classes de composants de T (ses types, ses symboles et ses axiomes; les axiomes d’induction de l’arithmétique doivent admettre l’utilisation des symboles t,l,a si ces symboles ne sont pas définissables, alors qu'ils le sont généralement comme on ne considère que des théories définissables). La formule de prouvabilité qui en résulte (∃p, V(p,s)) est indépendante de la manière correcte et complète choisie pour définir V, en ce sens que toutes ces formules de prouvabilité sont prouvablement équivalentes les unes aux autres en arithmétique du premier ordre. Plus formellement, pour deux telles formules arithmétiques V, V' codant la vérification de preuve dans la même théorie,

(Arithmétique + symboles et axiomes pour t,l,a) ⊢ ∀s, (∃p, V(p,s)) ⇔ (∃p, V'(p,s))

Cependant, pour achever de définir la prouvabilité, une fois écrite sous forme d'une formule de ce type, il reste encore à interpréter le ∃p de manière réaliste, dans le modèle standard de l'arithmétique ℕ, décrit intuitivement comme le système de seulement tous les entiers naturels effectivement finis, comme cela sera clarifié dans la partie 4. Cette utilisation du ℕ standard peut se comprendre intuitivement comme utilisation de l'infini actuel, nécessaire faute de limites prédictibles aux tailles de preuves nécessaires (minimales) pour des énoncés donnés. En effet, comme on expliquera en 1.A, les théorèmes d'incomplétude affaibliront cette définition de deux façons: établissant l'imprévisibilité de la taille des preuves nécessaires, et l'indécidabilité irréductible de certains prédicats de démontrabilité dans toute formalisation algorithmique de l'arithmétique (tandis que le point de vue réaliste les voit tous bien définis).

La preuve du théorème de complétude, qui nécessite l'axiome de l'infini (l'existence de ℕ) consistera à construire un modèle de toute théorie axiomatique cohérente du premier ordre, comme suit (détails en 4.6). L'ensemble (infini) de toutes les termes clos dont les symboles d'opération dérivent de la théorie (ceux de son langage plus d'autres issus de ses axiomes existentiels) devient un modèle en définissant progressivement chaque symbole de prédicat sur chaque combinaison de valeurs de ses arguments, par une règle conçue pour maintenir la cohérence. Cette construction est non algorithmique: elle est composée d'une infinité d'étapes, chacune utilisant une connaissance infinie (à savoir si le prédicat donné sur des arguments donnés, vu comme un axiome supplémentaire candidat, préserve la cohérence avec ceux précédemment acceptés). En fait, la plupart des théories fondatrices, telles que les théories des ensembles, n’ont aucun modèle définissable par un algorithme.

1.11. Quantificateurs universels du second ordre

La logique du premier ordre autorisera l'utilisation de symboles de structures variables comme abréviations d'expressions fixes définissant ces structures, mais ainsi ne peut les lier que sur certains domaines restreints respectivement déterminés par ces expressions (voir 1.B).
Appelons quantificateur du second ordre, un quantificateur liant un symbole de structure variable sur l'ensemble de toutes les structures de son type de symbole. Cela peut être conçu soit comme l'ensemble de toutes les expressions définissables (avec toutes les expressions de définition possibles, dont les variables libres peuvent inclure toute liste de paramètres au-delà des arguments donnés), soit comme leur ensemble complet (de toutes les opérations de ce type existant dans l'univers, reliant les types interprétés donnés). Utiliser des quantificateurs du second ordre signifie travailler dans un cadre logique élargi, notamment une version de la logique de second ordre (décrite dans la partie 5), suivant les détails.
Comme on fera pour les axiomes de l’égalité puis pour la théorie des ensembles (en 2.1 et 2.2), une théorie peut d’abord être exprimée en logique du second ordre pour des raisons intuitives, avant d’interpréter cela formellement comme un outil commode de niveau méta, pour abréger une formalisation du premier ordre, comme suit. (Les règles de preuve ci-dessous visent seulement à être correctes, la logique du second ordre n'admettant aucune théorie de la démonstration correcte et complète).
Soit T une théorie du premier ordre, T' son extension par un symbole de structure s (sans axiome supplémentaire) et F un énoncé de T' (en logique du premier ordre) également noté F(s) lorsque vu comme une formule de T utilisant le symbole de structure variable s en logique du second ordre.

Introduction universelle du second ordre. Si T'F alors T implique l'énoncé du second ordre (∀s, F(s)).

Ceci est valable pour tout modèle et le domaine ensembliste complet de s, indépendamment de l'univers dans lequel les modèles et les structures s sont recherchés.

Élimination universelle du second ordre. Une fois accepté un énoncé de second ordre (∀s, F(s)) dans une théorie T, il se manifeste en logique du premier ordre sous la forme d'un schéma d'énoncés (axiomes ou théorèmes), c'est-à-dire une liste infinie d'énoncés de la forme (∀parameters, F(s)) pour chaque remplacement possible de s par une expression définissante avec des paramètres.

Appliquer l’élimination universelle du second ordre après l’introduction universelle du second ordre signifie déduire de T un schéma de théorèmes, chacun déductible en logique du premier ordre en remplaçant s par sa définition respective dans la preuve originale.

Un nouveau symbole liant B utilisable en logique du premier ordre, peut être défini via la logique du second ordre, par une expression abrégée ici par F(A) car utilisant le symbole variable A de la structure unaire dont l'argument sera lié par B:

A, (Bx, A(x)) = F(A)

Par élimination universelle du second ordre, cela donne un schéma de définitions en logique du premier ordre: pour chaque expression définissant A, il définit (Bx, A(x)) comme un symbole de structure, par l'expression F(A) dont les variables libres disponibles sont les paramètres de F plus ceux de A.

Axiomes de l'égalité

En logique du premier ordre avec des types et un langage donnés, certains énoncés utilisant = sont valides (toujours vrais) pour le domaine d'interprétations conservant = en tant que prédicat = de la théorie des ensembles, mais non plus pour le domaine plus large d'interprétations l'interprétant comme tout autre prédicat. Une liste possible d'axiomes de l'égalité est une liste de certains de ces énoncés qui suffisent à impliquer tous les autres dans ce contexte. Une de ces listes comprend les 2 axiomes suivants par type, le dernier étant à entendre comme un schéma d'axiomes par élimination universelle du second ordre du prédicat unaire variable A:
  1. x, x = x (réflexivité)
  2. A,∀x,∀y, (x = yA(y)) ⇒ A(x).
Les variables x et y peuvent également servir parmi les paramètres de la définition de A. Ceci peut être compris en réordonnant les quantificateurs en (∀x, ∀y, ∀A), ou comme déduit de cas utilisant uniquement d'autres variables libres a, b, adaptant un énoncé logiquement valide de 1.10 :

a, ∀b, (∀x, ∀y, R(a, b, x,y)) ⇒ R(a, b, a,b).

Diverses définitions de A donnent divers énoncés (en supposant la réflexivité):

Enoncé
3. ∀x,∀y, x = yy = x
4. ∀x, ∀y, ∀z, (x = yy = z) ⇒ x = z
5. ∀f, ∀x, ∀y, x = yf(x) = f(y)
6. ∀A, ∀x, ∀y, x = y ⇒ (A(x) ⇔ A(y))
7. ∀x, ∀y, ∀z, (x = yz = y) ⇒ z = x
Nom
Symétrie
Transitivité
A(u) utilisé
y = u
u = z
f(u) = f(y)
¬A(u)
z = u

5. est un schéma d'énoncés avec f parcourant les foncteurs entre deux types quelconques.
6. peut aussi se déduire par symétrie.
La formule (x = yy = z) sera abrégée en x = y = z.
Remarque. (1.∧7.) ⇒ 3., puis 3. ⇒ (4. ⇔ 7) donc (1.∧7.) ⇔ (1.∧3.∧4.).

Une autre liste possible d'axiomes de l'égalité consiste en les énoncés 1. à 5. où f et A parcourent les seuls symboles du langage, pris chacun une fois par argument: le schéma complet de 2. est impliqué par déductions successives pour chaque occurrence de symbole dans A. Ceci sera plus précisément justifié en 2.11 (relations d’équivalence).
L'introduction d'une variable x définie par un terme t en écrivant (x = t ⇒ ...), autrement dit en posant l'axiome x = t, peut être considérée comme justifiée par les règles ainsi:

t = t ∴ ∃x, (x = t ∴ ...).


Other languages:
EN : 1. First foundations of mathematics