2. Théorie des ensembles (suite)

Ayant introduit la théorie des ensembles et la théorie des modèles en première partie , on développe la théorie des ensembles en seconde partie.

2.1. Uplets, familles

Uplets

Un uplet (ou n-uplet pour tout entier n) est une interprétation d'une liste de (n) de symboles de variables. C'est donc une méta-fonction d'un méta-ensemble fini, vers l'univers. Les uplets d'un type donné (liste des variables avec leurs types) peuvent être ajoutés à toute théorie comme un nouveau type d'objets. Les variables de ce type servent à abréger des paquets de n variables de types donnés (copies de la liste donnée) x = (x0,…,xn−1). En pratique, le domaine des n-uplets considérés sera le (méta-)ensemble Vn des n chiffres de 0 à n−1. La théorie des ensembles peut représenter ses propres n-uplets comme des fonctions, représentant Vn comme ensemble d'objets tous désignés par des constantes. Un 2-uplet s'appelle un couple, un 3-uplet est un triplet, un 4-uplet est un quadruplet...
Le définisseur de n-uplets n'est pas un symbole liant mais un opérateur n-aire, présentant ses n arguments dans une parenthèse et séparés par des virgules: ( ,…, ). L'évaluateur apparaît, curryfié en fixant le méta-argument, comme une liste de n foncteurs appelés projections: pour chaque iV n, la i-ième projection πi donne la valeur πi(x) = xi de chaque uplet x=(x0,…,xn−1) en i (valeur de la i-ième variable dans x). Ils sont soumis aux axiomes suivants (dont le premier résume les autres) : pour tous x0,…, xn−1 et tout n-uplet x,

x = (x0,…,xn−1) ⇔ (π0(x)=x0 ∧ … ∧ πn−1(x)=xn−1)
xi= πi((x0,…, xn−1))    pour chaque iVn
x = (π0(x),…, πn−1(x))

Les couples suffisent à construire une représentation des uplets de toute arité n > 2, au sens où l'on peut définir des opérateurs jouant les rôles de définisseur et projections, satisfaisant les mêmes axiomes. Par exemple les triplets t=(x,y,z) peuvent se définir par t=((x,y),z)) évalué par x00(t)), y10(t)), z1(t).

Connecteur conditionnel

Le connecteur d'arité 3, «Si A alors B sinon C», sera noté ainsi (appliquant (C,B) à AV2):

(A ? B : C) ⇔ (¬CAB) ⇔ ((AB)∧(¬AC)) ⇔ (¬A ? C : B) ⇔ (C,B)(A)
⇔ ((AB)∨(¬AC)) ⇔ ((CA)⇒(AB)) ⇎ (A ? ¬B : ¬C)

Tout connecteur K d'arité n+1 équivaut à 2 connecteurs d'arité n: K(A) ⇔ (A ? K(1): K(0)). Ainsi,

¬A ⇔ (A ? 0 : 1)
(AB) ⇔ (A ? B : 1)
(AB) ⇔ (A ? 1: B)
(AB) ⇔ (A ? B : ¬B).

Familles

Une famille est une fonction vue intuitivement comme uplet généralisé: son domaine (un ensemble) est vu comme simple, fixe, et extérieur au principal système étudié, comme un ensemble de méta-objets. Une «famille de... » est une famille dont l'image est «un ensemble de... ».
Les familles utilisent le formalisme des fonctions déguisé comme celui des uplets (inapplicable du fait de la finitude des symboles). L'évaluateur (qui évalue u en i), au lieu de u(i) ou πi(u), est noté ui (tel un symbole méta-variable de variable). Une famille définie par un terme t, se note (t(i))iI au lieu de (Iit(i)) ou de (t(0),…,t(n−1)). L'argument i est appelé indice, et la famille est dite indexée par son domaine I.

Structures et symboles liants

Toute structure n-aire peut se voir comme structure unaire de domaine une classe de n-uplets (comme un symbole liant peut être vu comme une structure unaire sur une classe de fonctions ou de sous-ensembles d'un ensemble donné): les symboles liants sont la généralisation des structures quand les familles remplacent les uplets. Ainsi ∀ et ∃ généralisent les chaînes de ∧ et de ∨:

(B0∧…∧Bn−1) ⇔ (∀iVn, Bi).

La condition d'égalité des couples (x,y)=(z,t) ⇔ (x=zy=t) est semblable à celle des fonctions.

Soient R un prédicat unaire admissible sur E, et C un booléen. On a les distributivités

(C ∧ ∃xE, R(x))  ⇔  (∃xE, CR(x))
(C ∨ ∀xE, R(x))  ⇔  (∀xE, CR(x))
(C ⇒ ∀xE, R(x))  ⇔  (∀xE, CR(x))
((∃xE, R(x)) ⇒ C)  ⇔  (∀xE, R(x) ⇒ C)
(∃xE, C) ⇔ (CE≠∅) ⇒ C ⇒ (CE=∅) ⇔ (∀xE, C)

Ecriture d'ensembles en extension

Le foncteur Im définit un symbole liant :

{T(x)|xE} = {T(x)}xE = Im(ExT(x))

Cette notation ressemblant au symbole de compréhension, on peut les combiner :

{T(x)| xER(x)} = {T(x)| x∈{yE|R(y)}}

Appliquer Im aux uplets, définit les opérateurs d'écriture en extension d'ensembles (qui énumèrent leurs éléments): Im(a,b,…) = {a,b,…}. Ceux d'arité 0,1,2 ont été vus au 1.11: l'ensemble vide ∅, le singleton {a} and l'appariement {a,b}.
Ainsi l'ensemble Vn s'écrit {0,…,n−1}. Les images d'uplets sont des ensembles finis.


Théorie des ensembles et fondements des mathématiques
1. Premiers fondements des mathématiques
2. Théorie des ensembles (suite)
2.1. Uplets, familles
2.2. Opérateurs booléens sur les ensembles
2.3. Produits, graphes et composition
2.4. Quantificateurs d'unicité, graphes fonctionnels
2.5. L'ensemble des parties
2.6. Injectivité et inversion
2.7. Relations binaires, ensembles ordonnés
2.8. Bijections canoniques
2.9. Relations d'équivalence et partitions
2.10. Axiome du choix
2.11. Correspondance de Galois
3. Théorie des modèles