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 (Qx ∈ E, ℛ (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))=(x→ vrai) ⇎
(∃x,
non
ℛ (x)) ⇔ (x→
non
ℛ (x)) ≠ (x→ faux)
En théorie des ensembles, (∀x ∈ E, ℛ (x)) ⇔ {x
∈ E| ℛ (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,
(∃Cx, ℛ (x))
⇔ (∃x,
C(x) et
ℛ (x)) ⇔ ∃Cet
ℛ ,vrai
(∀Cx, ℛ (x))
⇔ (∀x,
C(x) ⇒ ℛ (x))
∀x,(C(x)
⇔ (∃Cy,
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(x) etA(x));
réciproquement, toute sous-classe ( BetA)
de B satisfait ( BetA) ⇒
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 (Cet ℛ ) 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:
(∃x ∈ E,
ℛ (x))
→(∃x, x
∈ Eet ℛ (x))
(∀x ∈ E,
ℛ (x))
→(∀x,
x ∈ E ⇒ ℛ (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 F ∉ E.
Preuve. F={x ∈ E|Ens(x) etx ∉ x} ⇒ (F
∈ F ⇔ (F ∈ EetF
∉ F)) ⇒ (F ∉ FetF
∉ E). ◻