1.7. Quantificateurs

On appelle quantificateur tout symbole liant exercé sur une formule et à valeurs booléennes.
Un quantificateur Q de domaine un ensemble E sur une formule ℛ s'écrira (Q xE, ℛ (x)). Avec un domaine sous-entendu (fixé), on l'écrira Qx, ℛ (x).
Les deux principaux quantificateurs ∃ et ∀ (par lesquels on en définira ensuite d'autres) sont:
- Le quantificateur existentiel ∃, qui se lit «Il existe x (dans...) tel que... »
- Le quantificateur universel ∀, qui se lit «Pour tout (ou: quel que soit) x (dans...),... »).
Notant (x→ ℛ (x)) la méta-fonction de même domaine définie par ℛ , on méta-définit ∀ et ∃ par
(∀x, ℛ (x))  ⇔  (x→ ℛ (x))=(xvrai)  ⇎  (∃x, non
ℛ (x)) ⇔  (x non
ℛ (x)) ≠ (xfaux)
En théorie des ensembles, (∀xE, ℛ (x)) ⇔ {xE| ℛ (x)}=E.
La formule (∀x,vrai) est toujours vraie.
En théorie générique on mettra le domaine en indice: Qix, ℛ (x) où i est le type de x; avec des classes,

(∃C x, ℛ (x))
 ⇔ (∃x, C(x)  et  ℛ (x)) ⇔ ∃C et  ℛ ,vrai


(∀C x, ℛ (x))
 ⇔ (∀x, C(x)  ⇒  ℛ (x))


x,(C(x)
 ⇔ (∃C y, x=y))

Inclusion entre classes
La classe A est dite incluse dans B si ∀x, A(x) ⇒  B(x). C'est la condition pour que A soit une sous-classe de B, car alors ∀x,(A(x) ⇔ ( B(xet A(x)); réciproquement, toute sous-classe ( B et A) de B satisfait ( B et A) ⇒  B. L'inclusion de A dans B entraîne pour tout prédicat C (en cas de validité):

(∃Ax, C(x))
 ⇒ (∃ Bx, C(x))


(∀ Bx, C(x))
 ⇒ (∀Ax, C(x))


(∀Cx, A(x))
 ⇒ (∀Cx, B(x))


(∃Cx, A(x))
 ⇒ (∃Cx, B(x))

Règles de preuves des quantificateurs sur un prédicat unaire ℛ

Règle d'introduction de ∃. Si on trouve un terme t et une preuve de ℛ (t), alors ∃x, ℛ (x).

Règle d'élimination de ∃. Si ∃x, ℛ (x), alors on peut introduire une nouvelle variable libre z avec l'hypothèse ℛ (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 t par z. Elles donnent le même sens aux 3 formules équivalentes de définition de ∃C, court-circuitant la règle de validité étendue de (C et  ℛ ) car n'invoquant que le cas où C(x) est vrai et donc ℛ (x) est valide.
Alors que ∃ s'exprimait comme désignation d'un objet, ∀ se présente comme règle de déduction.

Règle d'introduction de ∀. Si de la seule hypothèse C(x) sur une nouvelle variable libre x on a pu déduire ℛ (x), alors ∀Cx, ℛ (x).

Règle d'élimination de ∀. Si ∀Cx, ℛ (x) et t est un terme satisfaisant C(t) alors ℛ (t) est vrai.
L'usage successif de ces règles revient à réécrire la démonstration initiale en remplaçant x par t.

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, ℛ (x))
→(∃x, xE et  ℛ (x))


(∀xE, ℛ (x))
→(∀x, xE ⇒  ℛ (x))
La théorie des ensembles n'admet dans ses formules, dites formules ensemblistes (qui définissent les prédicats et multiclasses, et composent certains termes) que des quantificateurs sur des ensembles, dits quantificateurs bornés. Mais sa forme traduite en théorie générique autorise des quantificateurs sur des classes (ou sur l'univers), dits quantificateurs ouverts, plus généraux. Les formules avec quantificateurs ouverts seront appelées des énoncés. En théorie des ensembles, on réservera l'usage des énoncés clos et valides à la déclaration de leur véracité: ce seront d'abord les axiomes, puis les théorèmes (déduits des axiomes) nommés différemment suivant leur importance: un théorème est plus important qu'une proposition; un lemme sert à démontrer un théorème; un corollaire en est une conséquence.
Sauf exception de commodité, les quantificateurs ouverts seront exprimés verbalement plutôt que symboliquement dans les énoncés, encadrant des formules ensemblistes seules notées en symboles. Les règles de preuves des quantificateurs traduiront les énoncés en manipulations de formules.
Le symbole de compréhension fut défini par un énoncé. On va l'utiliser pour montrer que la classe de tous les ensembles n'est pas un ensemble, rendant nécessaires toutes ces distinctions entre classes et ensembles, et entre quantificateurs ouverts et quantificateurs bornés:

Proposition (paradoxe de Russell). Pour tout ensemble E il existe un ensemble F tel que FE.
Preuve. F={xE|Ens(xet xx} ⇒ (FF ⇔ (FE  et FF)) ⇒ (FF et FE). ◻

1.6.  <—
Variables liées en théorie des ensembles

Sommaire
>     1.8.
Premiers axiomes de théorie des ensembles