2.4. Quantificateurs d'unicité et opérateur conditionnel

Quantificateurs d'unicité

Pour tous ensembles F ⊂ E, tout prédicat unaire A admissible sur E, et tout x ∈ E,

x ∈ F ⇔ {x} ⊂ F ⇔ (∃y∈E, x=y ∧ y∈F) ⇔ (∀y∈E, x=y ⇒ y∈F)
x ∈ F ⇒ ((∀y∈F, A(y)) ⇒ A(x) ⇒ ∃y∈F, A(y))
F ⊂ {x} ⇔ (∀y∈F, x=y) ⇒ ((∃y∈F, A(y)) ⇒ A(x) ⇒ (∀y∈F, A(y)))
F={x} ⇔ (x∈F ∧ ∀y∈F, x=y) ⇔ (∀y∈E, y∈F ⇔ x=y)

Voici 3 nouveaux quantificateurs: ∃≥2 (pluralité), ! (unicité), et ∃! («il existe un unique... »), qui appliqués à A dans E ne dépendent que de F={x ∈ E, ℛ (x)} (comme ∃ et contrairement à ∀) :

(∃x∈E, A(x)) ⇔ (F ≠ ∅) ⇔ (∃x∈F, 1) ⇔ (∃x∈E, {x} ⊂ F)
(∃≥2x∈E, A(x)) ⇔ (∃≥2: F) ⇔ (∃x,y∈F, x ≠ y) ⇔ (∃x≠y∈E, A(x) ∧ A(y))
(!x∈E, A(x)) ⇔ (!:F) ⇔ ¬(∃≥2: F) ⇔ (∀x,y∈F, x=y) ⇔ ∀x∈F, F ⊂ {x}
(∃!x∈E, A(x)) ⇔ (∃!:F) ⇔ (∃x∈F, F⊂{x}) ⇔ (∃x∈E, F={x})
F ⊂ {x} ⇒ (∀y∈F, F⊂{y}) ⇔ (!:F)
(∃!:F) ⇔ (F≠∅ ∧ !: F)
F≠∅ ⇒ ((∀y∈F, B(y)) ⇒ (∃y∈F, B(y)))
( !: F) ⇒ ((∃y∈F, B(y)) ⇒ (∀y∈F, B(y)))
F={x} ⇒ ((∃y∈F, B(y)) ⇔ B(x) ⇔ ∀y∈F, B(y))

Axiome de l'élément singulier

Introduisons un nouveau symbole primitif ℩ pour servir d'inverse du foncteur singleton { } : admissible uniquement sur la classe des singletons d℩E ⇔ (Set(E) ∧ ∃!:E), il donne leur élément unique, suivant l'axiome de l'élément singulier pouvant s'écrire de manière équivalente

∀x, ℩{x} = x
∀SetE, ∃!:E ⇒ ℩E ∈ E

(il fut d'abord introduit par Peano, puis son utilisation a été étendue au-delà de notre usage, comme "opérateur de description définie" de Russell, puis comme opérateur ϵ de Hilbert).
Alors pour chaque prédicat unaire A et chaque singleton E, A(℩E) ⇔ (∃x∈E, A(x)) ⇔ (∀x∈E, A(x)).

Connecteur conditionnel

Suivant les conventions de l'informatique, notons le connecteur ternaire «Si A alors B sinon C», par

(A ? B : C) ⇔ (¬C⇒A⇒B) ⇔ ((A⇒B)∧(¬A⇒C)) ⇔ (¬A ? C : B)
⇔ ((A∧B)∨(¬A∧C)) ⇔((C⇒A)⇒(A∧B)) ⇎ (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)
(A⇒B) ⇔ (A ? B : 1)
(A∧B) ⇔ (A ? B : 0)
(A∨B) ⇔ (A ? 1: B)
(A ⇔ B) ⇔ (A ? B : ¬B).

Opérateur conditionnel

Comme le connecteur conditionnel, il choisit entre deux objets x,y suivant le booléen B:

(B ? x : y) = ℩{z∈{x,y}| B ? z=x : z=y = ℩{z∈{x,y}| z=x ⇔ B}}

de sorte que pour tout prédicat unaire A,

A(B ? x : y) ⇔ (B ? A(x) : A(y)).

Tous les para-opérateurs autres que les connecteurs mais avec au moins un argument booléen, s'expriment naturellement comme composés de l'opérateur conditionnel et d'opérateurs, ou du connecteur conditionnel et de prédicats, ce qui explique l'inutilité de leur présence explicite dans le langage d'une théorie.

Les relations comme opérations

Les booléens B sont convertis en et depuis les objets b∈V2 = {0,1}, par b = (B ? 1 : 0) et B ⇔ b = 1.
Puis, de la notion d'opération n-aire avec ses symboles définisseur et évaluateur notés comme en 2.3, la notion de relation n-aire est constructible comme comme la classe des opérations n-aires à valeurs dans V2 (servant de type booléen), comme suit. Avec n=2 (les autres cas sont similaires), une telle opération binaire r de domaines E et F reçoit ce rôle de relation binaire, étant définie à partir de tout prédicat binaire R, et évaluée en retour comme R, par les formules

r = (E×F ∋ (x,y) ↦ (R(x,y) ? 1 : 0))
∀x∈E, ∀y∈F, R(x,y) ⇔ r(x, y) = 1

Définition des définisseurs d'uplets

Le définisseur de couple se définit comme une vue curryfiée de l'opérateur conditionnel:

(x,y) = (V2 ∋ a ↦ (a = 1 ? y : x))

Confondant les booléens avec des objets, (B ? x : y) = πB(y,x).
D'autres uplets peuvent être ainsi définis de diverses manières, telles que

(x,y,z) = (V3 ∋ a ↦ (a = 2 ? z : (a = 1 ? y : x)))

Étant donné la notion de couples, les rôles des notions d'uplets de toute arité supérieure n > 2 peuvent également être joués par d'autres classes, avec d'autres définitions de leurs définisseurs et projections, satisfaisant les mêmes axiomes. Par exemple les triplets t = (x,y,z) peuvent être définis par t = ((x,y),z)) et évalués par

x = π0(π0(t))
y = π1(π0(t))
z = π1(t)

Théorie des ensembles et fondements des mathématiques
1. Premiers fondements des mathématiques
2. Théorie des ensembles
2.1. Premiers axiomes de théorie des ensembles
2.2. Principe de génération des ensembles
2.3. Curryfication et uplets ⇦
2.4. Quantificateurs d'unicité
⇨ 2.5. Familles, opérateurs booléens sur les ensembles
2.6. Graphes
2.7. Produits et ensembles des parties		 2.8. Injections, bijections
2.9. Propriétés des relations binaires
2.10. Axiome du choix
Temps en théorie des ensembles
Interprétation des classes
Concepts de vérité en mathématiques
3. Algebra - 4. Arithmetic - 5. Second-order foundations
Other languages:
EN : 2.4. Uniqueness quantifiers