On appelle classe tout prédicat unaire vu comme ensemble des
objets où il est vrai. Les classes invariantes sont des cas très
généraux de notions. Elles remplaceront les types en théorie des
ensembles. En effet on a besoin de rassembler tous ses objets dans le
type «élément» pouvant appartenir à des ensembles (pour éviter de
rediviser à l'infini : ensembles d'éléments, d'ensembles, de fonctions,
ensembles mixtes...). Dès lors les notions d'ensemble et de fonction
seront des classes désignées par les symboles: Ens =
«est un ensemble», Fon = «est une fonction».
(Une autre méthode serait de conserver 3 types où chaque ensemble
figurerait en double, comme ensemble et comme élément, identifiés par
un foncteur convertissant l'ensemble en élément; et de même pour les
fonctions. Mais cette idée qui pourrait servir à d'autres théories ne
suffira pas en théorie des ensembles qui aura de toute façon besoin des
classes comme notions)
La théorie des ensembles dans le cycle fondateur
La théorie du modèle n'est que partiellement formalisable comme
théorie: son exigence que chaque expression et chaque preuve soient de
taille finie, n'est formulable que dans sa forme traduite en théorie
des ensembles. Cette forme désignant les constituants de son modèle M1=[T,M]
par des variables libres, leur variabilité fait de ceci l'expression
ensembliste de la théorie des modèles (grand tour des fondements des
mathématiques).
Dans ce cadre, le composant M de M1
constitue un modèle de la traduction ensembliste de T (les
constituants ensemblistes de T se traduisent en termes
désignant leur image dans le système-objet T).
Or en tant que théorie T nous allons formaliser une théorie des
ensembles, interprétant ses concepts dans M. C'est pourquoi on
marquera du préfixe méta- leur précédente
interprétation dans l'univers extérieur (cadre des notions de théorie
du modèle et même de leur méta-interprétation déjà évoquée).
La traduction des objets, notions et structures ensemblistes en leur
équivalent méta-ensembliste, les préservera en grande partie, mais
n'est pas réversible. Contrairement à la méthode standard traduisant
tout objet en élément pur, les ensembles seront généralement traduits
en méta-ensembles des mêmes éléments, et de même pour les fonctions.
Ainsi tout ensemble E sera une classe (celle des x tels
que x ∈ E, d'argument x et de paramètre E)
mais on verra que l'univers, classe (vrai) de tous les objets, n'est
pas un ensemble. Toute classe est un méta-ensemble d'objets, mais
certains méta-ensembles d'objets, indéfinissables, ne sont pas des
classes.
Classes de validité
Etant donnés un modèle et des valeurs des variables libres, une
expression sera dite valide
si elle a effectivement une valeur (une formule non valide n'est ni
vraie ni fausse). La validité des expressions des théories génériques
est garantie par la correction syntaxique, intégrée au concept
d'expression. Mais en théorie des ensembles la validité d'une structure
(expression) peut dépendre des valeurs de ses arguments (variables
libres). La condition de validité est un prédicat, exprimé par une
formule de mêmes variables libres, toujours valide. S'il est unaire, il
définit une classe qui est le domaine du foncteur (ou prédicat unaire)
considéré.
Généralement, le lieu de vérité d'un prédicat n-aire ℛ partout
valide est une classe n-aire (classe de systèmes de
valeurs de n variables - on y reviendra avec les n-uplets),
ou multiclasse pour ne pas préciser n. C'est le domaine
d'un système de n variables uniquement soumises à l'hypothèse ℛ
.
Toute structure (définie par une expression) a pour domaine une
multiclasse appelée sa multiclasse de validité, définie par la
formule de sa condition de validité, de mêmes arguments et paramètres.
Celle de l'évaluateur de fonction f(x), est (Fon f
et x ∈ Domf). On doit
prendre soin de n'employer des expressions que dans leur multiclasse de
validité, ce qui se fera assez naturellement.
Une théorie aux structures partiellement valides se traduit en théorie
générique à un seul type (aux structures partout valides), gardant
intactes les expressions et leurs valeurs lorsqu'elles sont valides :
les modèles se traduisent en ajoutant arbitrairement des valeurs aux
structures hors de leur multiclasse de validité (par exemple une valeur
constante), et en sens inverse en ignorant ces valeurs.
Validité étendue
Pour tous prédicats A et B de conditions de validité VA
et VB, les formules «AetB» et «A ⇒ B»
auront la même condition de validité (VAet (A ⇒ VB))
(rompant, pour «et», la symétrie entre A et B qu'il est
inutile de rétablir).
On les regardera donc valides même si A est faux et B
non valide, alors de valeurs respectives faux et vrai, résultats
indépendants d'une valeur arbitrairement ajoutée à B.
Ceci rend valides «VAetA»
et «VA ⇒ A» (étendant A
respectivement par faux et par vrai hors de son domaine de validité),
et les conditions de validité elles-mêmes. Les formules «Aet (BetC)»
et «(AetB) etC» ont la même condition de
validité (VAet (A ⇒ (VBet (B ⇒ VC)))).
Si (AetB) est
toujours valide (A est toujours valide et B valide sur
toute la (multi)classe A), la (multi)classe qu'il définit est
appelée la sous-classe de A définie par B.