Quantification (logique)

En mathématiques, les expressions « pour tout » (ou « quel que soit ») et « il existe », utilisées pour formuler des propositions mathématiques dans le calcul des prédicats, sont appelées des quantifications. Les symboles qui les représentent en langage formel sont appelés des quantificateurs (ou autrefois des quanteurs^[1]^,^[2]).

Symboles mathématiques des deux quantificateurs logiques les plus courants.

Quantification universelle modifier

La quantification universelle (« pour tout ... » ou « quel que soit ... ») se dénote par le symbole ∀ (un A à l'envers).

Exemple :

\forall x\,P(x)

se lit

{\text{Pour tout}}\,x\,P(x)

et signifie

« tout objet du domaine considéré possède la propriété P ».

La notation « ∀ » a été utilisée pour la première fois^[3]^,^[4] par Gerhard Gentzen en 1933 (publié en 1934^[5]). Le mot allemand alle signifiant « tout », il propose un « symbole (Zeichen) valant pour tout (für alle) ». Gentzen indique qu'il a choisi comme « symbole pour tout » (All-Zeichen) le A renversé par analogie avec le symbole « ∃ » pour le quantificateur existentiel qu'il tient de Russell (qui lui-même l'a emprunté à Peano)^[6].

Quantification existentielle modifier

Article détaillé : Quantification existentielle.

La quantification existentielle (« il existe un ... » au sens « il existe au moins un ... ») se note avec le signe ∃ (un E retourné). Plus précisément,

\exists x\,P(x)

signifie

{\text{il existe au moins un}}\,x\,{\text{tel que}}\,P(x).

(un objet au moins du domaine considéré possède la propriété P)

Pour exprimer l'unicité en plus de l'existence, le signe utilisé est ∃! (le quantificateur existentiel suivi d'un point d'exclamation), plus précisément,

\exists !x\,P(x)

signifie

il existe un unique x tel que P(x), ou encore il existe un et un seul x tel que P(x) (un objet exactement du domaine considéré possède la propriété P).

Ce dernier quantificateur se définit en calcul des prédicats égalitaire à partir des deux quantificateurs précédents (et de l'égalité), par exemple par

\exists !x\,P(x)\equiv \exists x[P(x)\,{\text{et}}\,\forall y(P(y)\Longrightarrow y=x)]

La notation ∃ a tout d'abord été employée par Giuseppe Peano en 1897 dans le volume II de son Formulaire de mathématiques^[7] avec une syntaxe différente, le signe étant directement associé au prédicat (∃ P pour notre ∃x P(x)). Bertrand Russell l'utilise le premier de la façon actuelle, comme un opérateur de liaison^[3].

Négation des quantificateurs modifier

La négation de $\exists x\,P(x)$ est :

\neg \exists x\,P(x)

, soit :

\forall x\,\neg P(x)

.

La négation de $\forall x\,P(x)$ est :

\neg \forall x\,P(x)

, soit :

\exists x\,\neg P(x)

en logique classique, mais pas en logique intuitionniste.

Ordre des quantificateurs modifier

Pour une formule mise en forme prénexe, l'ordre des quantificateurs entre chaque bloc de quantificateurs identiques (donc bloc de quantificateurs existentiels ou bloc de quantificateur universels) est indifférent, la formule restant la même. Par contre, l'alternance des blocs de quantificateurs existentiels ou universels donne des formules bien distinctes dont la complexité logique s'observe notamment dans la hiérarchie arithmétique.

Déduction naturelle modifier

En déduction naturelle, Gerhard Gentzen présente les deux quantificateurs de la manière suivante^[8]:

	Règles d'introduction	Règles d'élimination
pour tout	${\frac {F}{\forall xF}}$ .	${\frac {\forall xF}{F}}$
il existe	${\frac {F}{\exists xF}}$	${\frac {\exists xF\quad {\begin{array}{c}[F]\\\vdots \\q\end{array}}}{q}}$

Exemples modifier

Si l'on prend un groupe de chats noirs, on peut dire que quel que soit le chat que l'on choisit dans ce groupe, il sera noir. ( $\forall chat\mathrm {\textvisiblespace} dans\mathrm {\textvisiblespace} ce\mathrm {\textvisiblespace} groupe,la\mathrm {\textvisiblespace} couleur\mathrm {\textvisiblespace} du\mathrm {\textvisiblespace} chat\mathrm {\textvisiblespace} est\mathrm {\textvisiblespace} noire$ )

Si, dans un groupe de chats noirs, il y a quelques chats blancs (ou un seul), on peut dire qu'il existe un (ou un unique) chat de couleur blanche dans ce groupe.

( $\exists (!)chat\mathrm {\textvisiblespace} dans\mathrm {\textvisiblespace} ce\mathrm {\textvisiblespace} groupe,la\mathrm {\textvisiblespace} couleur\mathrm {\textvisiblespace} du\mathrm {\textvisiblespace} chat\mathrm {\textvisiblespace} est\mathrm {\textvisiblespace} blanche$ )

Représentation des quantificateurs en Unicode, HTML et LaTeX modifier

	Symbole	Unicode	HTML	LaTeX
pour tout	∀	U+2200^[9]	∀^[10]	\forall^[10]
il existe	∃	U+2203^[11]	∃^[12]	\exists^[12]

Bibliographie modifier

L'exposé des règles régissant les quantificateurs usuels il existe et quel que soit se trouve dans tous les manuels de calcul des prédicats dont une bibliographie peut être trouvée sur logique mathématique.

Pour une généalisation de ces quantificateurs on peut se tourner vers :

(en) Generalized Quantifiers and Computation: 9th European Summer School in Logic, Language, and Information ESSLLI’97Workshop Aix-en-Provence, France, August 11–22, 1997 Revised Lectures, 145 pages, (ISBN 9783540669937)

Références modifier

↑ quanteur dans le dictionnaire du CNTRL.
↑ Maurice Pouzet, « Modèle universel d'une théorie n-complète », Comptes-rendus de l'Académie des Sciences, a, t. 274,‎ 1972, p. 433 (lire en ligne)
↑ ^{a et b} (en) Jeff Miller, Earliest Uses of Symbols of Set Theory and Logic, septembre 2010 (Premiers usages des symboles logiques dans la théorie des ensembles).
↑ Jacques Herbrand utilise, en 1930, la notation $(x)\,P(x)$ dans sa thèse Recherches sur la théorie de la démonstration : Thèses présentées à la faculté des sciences de Paris, Paris, 1930, 128 p. (lire en ligne), p. 28-29.
↑ « Untersuchungen über das logische Schließen. I », Mathematische Zeitschrift, vol. 39 (2),‎ 1934, p. 176-210 (lire en ligne).
↑ (en) Stephen Webb, « Clash of Symbols », SpringerLink,‎ 2018 (DOI 10.1007/978-3-319-71350-2, lire en ligne, consulté le 2 mars 2024)
↑ G. Peano, Formulaire de mathématiques, Tome II, Logique mathématique (1897) ∃.
↑ (de) Gerhard Gentzen, Untersuchungen über das Logische Schliessen, p. 22
↑ « Unicode Character 'FOR ALL' (U+2200) ».
↑ ^{a et b} Cf. Table de symboles mathématiques (Chevrons et angles).
↑ « Unicode Character 'THERE EXISTS' (U+2203) ».
↑ ^{a et b} Cf. Table de symboles mathématiques (Autres symboles en traits droits).

Voir aussi modifier

Théorie de la description définie de Bertrand Russell
Théorie des mondes possibles
Notation (mathématiques)
La lettre λ du Lambda-calcul qui elle aussi lie des variables.

Portail des mathématiques

[1] quanteur dans le dictionnaire du CNTRL.

[2] Maurice Pouzet, « Modèle universel d'une théorie n-complète », Comptes-rendus de l'Académie des Sciences, a, t. 274,‎ 1972, p. 433 (lire en ligne)

[Gentzen-1933-3] {a et b} (en) Jeff Miller, Earliest Uses of Symbols of Set Theory and Logic, septembre 2010 (Premiers usages des symboles logiques dans la théorie des ensembles).

[4] Jacques Herbrand utilise, en 1930, la notation $(x)\,P(x)$ dans sa thèse Recherches sur la théorie de la démonstration : Thèses présentées à la faculté des sciences de Paris, Paris, 1930, 128 p. (lire en ligne), p. 28-29.

[5] « Untersuchungen über das logische Schließen. I », Mathematische Zeitschrift, vol. 39 (2),‎ 1934, p. 176-210 (lire en ligne).

[6] (en) Stephen Webb, « Clash of Symbols », SpringerLink,‎ 2018 (DOI 10.1007/978-3-319-71350-2, lire en ligne, consulté le 2 mars 2024)

[Peano-1897-7] G. Peano, Formulaire de mathématiques, Tome II, Logique mathématique (1897) ∃.

[8] (de) Gerhard Gentzen, Untersuchungen über das Logische Schliessen, p. 22

[9] « Unicode Character 'FOR ALL' (U+2200) ».

[pour-tout-10] {a et b} Cf. Table de symboles mathématiques (Chevrons et angles).

[11] « Unicode Character 'THERE EXISTS' (U+2203) ».

[il-existe-12] {a et b} Cf. Table de symboles mathématiques (Autres symboles en traits droits).

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]