1.9. 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: Leur interprétation peut se définir dans un cadre ensembliste regardant A comme une fonction, et ses valeurs booléennes comme des objets:

(∀x, A(x)) ⇔ A = (x ↦ 1)
(∃x, A(x)) ⇔ A ≠ (x ↦ 0)
(∀x, A(x)) ⇎ (∃x, ¬A(x))

En théorie des ensembles, (∀xE, A(x)) ⇔ {xE | A(x)} = E. La formule (∀x,1) est toujours vraie.
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

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.

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))

Statut des quantificateurs ouverts en théorie des ensembles

La théorie des ensembles se traduit en théorie générique en convertissant en classes les domaines des quantificateurs:

(∃xE, A(x)) → (∃x, xEA(x))
(∀xE, A(x)) → (∀x, xEA(x))

La théorie des ensembles n'admet que des quantificateurs sur des ensembles, dits quantificateurs bornés, dans ses formules (dites formules bornées pour insister sur ce fait), qui définissent les prédicats et peuvent s'utiliser dans des termes. Mais sa forme traduite en théorie générique autorise des quantificateurs sur des classes (ou sur l'univers), dits quantificateurs ouverts.
Les formules avec quantificateurs ouverts en théorie des ensembles seront appelées des énoncés. Leur usage sera essentiellement restreint aux déclarations de véracité des énoncés clos admissibles. Ce seront d'abord les axiomes, puis les théorèmes qui s'en déduisent.
Les quantificateurs ouverts dans les énoncés seront le plus souvent exprimés comme articulations verbables (utilisant naturellemement les règles de preuves ci-dessus) entre leurs sous-formules bornées seules notées en symboles.

Le symbole de compréhension K = {xE|A(x)} fut défini par un énoncé (∀x, xK ⇔ (xEA(x))) mais 1.11 le redéfinira sans quantificateur ouvert (sauf sur ses paramètres).

Théorie des ensembles et fondements des mathématiques
1. Premiers fondements des mathématiques
1.1. Introduction au fondement des mathématiques
1.2. Variables, ensembles, fonctions et opérations
1.3. Forme des théories
1.4. Structures 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
Sens des quantificateurs ouverts
Interprétation des classes
Concepts de vérité en mathématiques
2. Set theory (continued) 3. Model theory

Other languages:
EN : 1. First foundations of mathematics : 1.9. Quantifiers