Quantificateurs

1.10. Quantificateurs

Un quantificateur est un symbole liant exercé sur un prédicat unaire (une formule) et à valeurs booléennes.

Quantificateurs bornés; quantificateurs ouverts

Un quantificateur Q est dit borné lorsqu'il suit le fornat d'usage ensembliste des symboles liants (1.8) : son domaine est un ensemble donné en argument. Pour les quantificateurs ce format se note (Q ∈ , ) rempli comme (Qx∈E, A(x)) pour prendre en entrée un prédicat unaire A, en liant une variable x de domaine E sur une quelconque formule ici abrégée en A(x) pour signifier qu'elle définit A d'argument x avec d'éventuels paramètres.
Primitivement en logique du premier ordre, les domaines des quantificateurs sont des types (le même type que la variable liée, formellement pas un argument). Tout domaine E (type, classe ou ensemble) peut être marqué en indice (Q_Ex, A(x)), ou supprimé (Qx,A(x)) quand il est sans importance, ou sous-entendu comme fixé par le contexte.
Lorsque la théorie des ensembles est formalisée en logique du premier ordre, les quantificateurs de la logique du premier ordre, parcourant l'univers, et leurs variantes parcourant des classes (définis à partir d'eux ci-dessous), sont appelés des quantificateurs ouverts par opposition au cas restreint des quantificateurs bornés (comme les ensembles sont des cas particuliers de classes). Dans ce contexte, une formule est dite bornée si tous ses quantificateurs sont bornés. Cette condition sera requise pour certaines utilisations (1.A, 1.C, 2.1, 2.2).

Les deux principaux quantificateurs

Les deux principaux quantificateurs (par lesquels d'autres seront définis en 2.6) sont:

Le quantificateur universel ∀ signifie «pour tout» ou «quel que soit»: (∀x∈E, A(x)) se lit «pour tout x dans E, A(x) ».
Le quantificateur existentiel ∃ signifie «il existe» : (∃x∈E, A(x)) se lit «il existe x dans E tel que A(x)».

Le quantificateur universel borné est définissable par le symbole de compréhension :

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

Les quantificateurs de tout domaine peuvent se définir dans des interprétations ensemblistes en 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))

La formule (∀x,1) est toujours vraie. Les quantificateurs sur les classes peuvent se définir par

(∀_C x, A(x)) ⇔ (∀x, C(x) ⇒ A(x))
(∃_C x, A(x)) ⇔ (∃x, C(x) ∧ A(x)) ⇔ ∃_C∧A x, 1

Inversement, toute classe est définissable à partir d'un quantificateur sur elle: ∀x, (C(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))
(∃_Cx, A(x)) ⇒ (∃_Cx, B(x))
(∀_Cx, A(x)) ⇒ (∀_Cx, B(x))

Règles de preuves pour les quantificateurs sur un prédicat unaire

Tout comme les expressions furent décrites en permettant de prendre des expressions déjà faites pour en former de nouvelles, on peut formaliser le concept de preuve en utilisant des preuves déjà connues pour en former de nouvelles. Voici quelques règles intuitivement introduites, sans prétention de formalisation complète.

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 mais ils pourront être rassemblés en un seul par l'opérateur conditionnel). 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 (C ∧ A) 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: ∀_Cx, A(x) signifie que sa négation ∃_Cx, ¬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 ∀_Cx, A(x).

Elimination universelle. Si ∀_Cx, 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.

Formules logiquement valides

Ces règles permettent d'établir les formules logiquement valides suivantes

((∀_Cx, A(x)) ∧ (∀_Cx, A(x) ⇒ B(x))) ⇒ (∀_Cx, B(x))
((∃_Cx, A(x)) ∧ (∀_Cx, A(x) ⇒ B(x))) ⇒ (∃_Cx, B(x))
((∀_Cx, A(x)) ∧ (∃_Cx, B(x))) ⇒ (∃_Cx, A(x) ∧ B(x))
(∀_Cx, A(x)∨B(x)) ⇒ ((∀_Cx, A(x)) ∨ (∃_Cx, B(x)))
(∀_A x, ∀_B y, R(x,y)) ⇔ (∀_B y, ∀_A x, R(x,y))
(∃_A x, ∃_B y, R(x,y)) ⇔ (∃_B y, ∃_A x, R(x,y))
(∃_A x, ∀_B y, R(x,y)) ⇒ (∀_B y, ∃_A x, R(x,y))
∀x, (∀y, R(x,y)) ⇒ R(x,x) ⇒ (∃y, R(x,y))

On utilisera les abréviations suivantes, et de même pour les quantificateurs bornés:

(∀_C x,y, ) pour (∀_C x, ∀_C y, ) et ainsi de suite avec plus de variables de même domaine.
(∃_C x,y, ) pour (∃_C x, ∃_C y, ) (même remarque).
(∀_Cx≠y, ) pour (∀_Cx,y, x≠y ⇒ )
(∃_Cx≠y, ) pour (∃_Cx,y, x≠y ∧ )
(∃_Cx, A(x) ∴ B(x)) pour (∃_Cx, A(x)) ∧ (∀_Cx, A(x) ⇒ B(x)), alors qu'elle implique mais n'est pas toujours équivalente à (∃_Cx, A(x) ∧ B(x)).

La validité logique dépend du langage parce que, avec un seul type

(L ⊢ ∃x, 1) ⇔ (un symbole de constante existe dans L)

(Avec plus de types, la condition est plus compliquée ; mais comme la plupart des théories utiles exigent que tous les types soient non vides, la dépendance au langage peut être ignorée en pratique)

Complétude de la logique du premier ordre

La logique du premier ordre a été trouvée complète, ce qu'exprime le théorème de complétude, qui était à l’origine la thèse de Gödel: à partir d’un concept de «démonstration» convenablement formalisé, la classe résultante de théorèmes (potentiels) de toute théorie du premier ordre se trouve être celle "parfaite", équivalente à la véracité universelle (classe des énoncé vrais dans tous les modèles M):

∀A, (T ⊢ A) ⇔ (∀M, (M⊨T)⇒(M⊨A))

Une telle théorie de la démonstration pour la logique du premier ordre est essentiellement unique: l'équivalence entre deux versions (correctes et complètes) concernant l'existence d'une preuve d'un énoncé dans une théorie, apparaît concrètement par la possibilité de traduire toute "preuve" pour l'une en une "preuve" pour l'autre.

Cette qualité de la logique du premier ordre confirme son importance centrale dans les fondements des mathématiques, après sa capacité à exprimer toutes les mathématiques : tout cadre logique peut de toute façon être développé en théorie des ensembles (ou plus directement ses théories peuvent être interprétées en théorie des ensembles) elle-même exprimable comme théorie du premier ordre.

La preuve du théorème de complétude, qui nécessite l'axiome de l'infini (l'existence de ℕ) consistera à construire un modèle de toute théorie axiomatique cohérente du premier ordre, comme suit (détails en 4.7). L'ensemble (infini) de toutes les termes clos dont les symboles d'opérateur dérivent de la théorie (ceux de son langage plus d'autres issus de ses axiomes existentiels) devient un modèle en définissant progressivement chaque symbole de prédicat sur chaque combinaison de valeurs de ses arguments, par une règle conçue pour maintenir la cohérence.

Cette construction est non algorithmique: elle nécessite une infinité d'étapes, dont chacune dépend d'une connaissance infinie (à savoir si le prédicat donné sur des arguments donnés, vu comme un axiome supplémentaire candidat, préserve la cohérence avec ceux précédemment acceptés). En fait, la plupart des théories fondatrices, telles que les théories des ensembles, n’ont aucun modèle définissable par un algorithme.

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 1.7. Classes en théorie des ensembles 1.8. Symboles liants	1.9. Axiomes et preuves ⇦ 1.10. Quantificateurs ⇨1.11. Quantificateurs du 2e ordre
	Aspects philosophiques 1.A. Temps en théorie des modèles 1.B. Indéfinissabilité de la vérité 1.C. Théorèmes d'incomplétude 1.D. Le cadre ensembliste unifié
2. Théorie des ensembles - 3. Algèbre

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