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: Le quantificateur universel de la théorie des ensembles peut être vu comme défini par le symbole de compréhension :

(∀xE, A(x)) ⇔ {xE | A(x)} = E.

Celui de la logique du premier ordre peut se définir dans un cadre ensembliste en regardant A comme une fonction, et ses valeurs booléennes comme des objets:

(∀x, A(x)) ⇔ A = (x ↦ 1)

La formule (∀x,1) est toujours vraie.
∃ peut se définir à partir de ∀ avec le même domaine: (∃x, A(x)) ⇎ (∀x, ¬A(x)).
Donc (∃x, A(x)) ⇔ A ≠ (x ↦ 0).
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))
Un cadre logique élargi acceptant les symboles de structure variables (comme la logique du second ordre, voir 3.6)

Axiomes de l'égalité

Pour tous objets x,y (pouvant abréger des termes), tout foncteur T et tout prédicat unaire A,
x = y
x = y
x = x
T(x) = T(y)
(A(x) ⇔ A(y))
Cette dernière formule peut aussi s'écrire (A(x) ∧ x = y) ⇒ A(y), puisque la réciproque A(y) ⇒ A(x) peut se déduire soit par sa contraposée (replaçant A par ¬A) ou par la symétrie de l'égalité (x = yy = x) obtenue en prenant pour A(z) la formule (z = x).
Cela donne aussi pour tous x, y, z, (x = yy = z) ⇒ x = z. La formule (x = yy = z) sera abrégée en x = y = z.
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