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 est un système fini d'occurrences de symboles, qui définira une valeur pour chaque donnée possible d'un modèle (système interprétant les types et les symboles de structure donnés, ignorant les axiomes), et d'une interprétation des variables libres utilisées (leurs valeurs dans le modèle).
Toute expression est un terme ou une formule: les valeurs des termes seront des objets, tandis que les formules auront des valeurs booléennes.
Une expression est close, si elle ne comporte aucune variable libre (toutes ses variables sont liées), de sorte que sa valeur ne dépend que du modèle. Les axiomes d'une théorie sont choisis parmi ses formules closes.

Esquissons la description générale des expressions (qui sera formalisée dans la partie 3).

Une occurrence d'un symbole dans une expression, est un lieu où il est écrit, par exemple le terme «x+x» comporte 2 occurrences de x et une de +.
Les symboles utilisables dans les expressions sont Les expressions se construisent successivement. Les premières et plus simples sont faites d'un seul symbole 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 : Le symbole principal détermine le type des valeurs (et donc décide si c'est un terme ou une formule), et le format de la liste (le nombre d'entrées et leurs types). Pour les symboles de para-opérateurs, ce format est donné par la liste des arguments.
La liste était vide pour les constantes, qui (comme racines) forment des expression seules. Les autres para-opérateurs et symboles liants demandent une liste non vide, nécessitant un choix conventionnel de présentation: Les parenthèses peuvent aussi servir, pour chaque expression ou sous-expression, à distinguer son symbole principal en séparant les sous-expressions, comme dans (x+y)n.

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 autre symbole hors du langage: un symbole de variable fixe. On peut l'interpréter différemment suivant la théorie dans laquelle on se place: Généralisant cela du cas de simples objets (identifiés à toutes les opérations nulaires pouvant exister entre types interprétés) aux autres structures (d'arité non nulle), on obtient le concept de symbole de structure variable, mais cela échappe à la liste ci-dessus des symboles admis dans les expressions. Ainsi, le statut des expressions utilisant un tel symbole est à choisir entre: Comme une théorie du premier ordre ne peut pas gérer tout le domaine d'une structure variable d'arité non nulle (sauf si tous ses arguments parcourent des ensembles finis), elle ne peut pas exprimer toutes les propriétés de ce domaine. Certaines propriétés peuvent encore se trouver comme suit: si une formule avec un symbole de structure variable (non défini) est formellement prouvée, alors elle est vraie pour toutes les structures qu'elle pourrait signifier, peu importe si ces structures peuvent être «trouvées» ou non. Cette notion de vérité universelle prouvable sera utilisée comme une règle de preuve pour les variables ordinaires (principe d'introduction universelle, 1.9) et dans l'expression du principe de génération des ensembles (1.11).

Structures définies par des expressions

Toute théorie peut produire des structures (opérateurs ou prédicats, au-delà de celles directement nommées dans son langage), données comme opérations entre types interprétés, définies par les données suivantes:
Ainsi les opérateurs nullaires (simples objets) sont «définis» par le terme fait d'un symbole de variable vu comme paramètre. Dans une formalisation de la 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.

On peut accepter comme légitime à l'intérieur de la théorie, de nommer une telle structure par un symbole de structure variable, conçu comme abréviation de l'expression avec ses paramètres. Comme la variabilité du symbole abrège celle des paramètres, cette structure variable peut être liée dans la théorie comme parcourant toutes les structures définies par une même expression avec toutes les valeurs possibles des paramètres : ceci abrège le fait de lier les paramètres.

Nous fixerons désormais pour la théorie du modèle, la notion de structure, et donc celles d'opérateur et de prédicat, comme ensemble de toutes les structures ainsi atteignables, définies par toute expression avec toutes valeurs possibles des paramètres. Comme cela fait appel à l'ensemble infini de toutes les expressions, cela échappe aux capacités de la théorie étudiée (qui ne peut utiliser qu'une expression à la fois) et est accessible uniquement par le cadre de la théorie du modèle avec sa méta-notion d'expression. Cependant cette généralité ne prétend pas épuiser l'ensemble des opérations (entre types interprétés) pouvant exister dans l'univers d'un cadre ensembliste, comme il peut y avoir des structures indéfinissables.

Structures invariantes

Une structure invariante pour une théorie, est une structure définie sans paramètre (donc constante). Toute structure désignée par un symbole du langage d'une théorie, est directement définie par lui sans paramètre, donc invariante pour cette théorie. 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 est exprimable indirectement par la théorie plutôt que directement nommé dans son langage.
Toute structure invariante absente du langage peut être désignée par un nouveau symbole et ajoutée au langage, préservant la signification profonde de la théorie (méta-notions de structure, structure invariante, prouvabilité...). De telles règles de développement des théories seront détaillées en partie 3.

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 logiques
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.5. Expressions and definable structures