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^,).

Quantification universelle

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

Exemple

La phrase notée symboliquement :

\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 « $\forall$ » a été utilisée pour la première fois^, par Gerhard Gentzen en 1933 (publié en 1934). 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 « $\exists$ » pour le quantificateur existentiel qu'il tient de Russell (qui lui-même l'a emprunté à Peano).

Quantification existentielle

Article détaillé : Quantification existentielle.

La quantification existentielle (« il existe un ... » au sens « il existe au moins un ... ») se note avec le signe $\exists$ (le symétrique axial d'un E, c'est-à-dire, la lettre Ə majuscule). 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 ${\displaystyle \exists$ (le quantificateur existentiel suivi d'un point d'exclamation), plus précisément,

\exists !x\,P(x)

signifie

{\text{il existe un unique }}x{\text{ tel que }}P(x)

, ou encore

{\text{il existe un et un seul }}x{\text{ 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 $\exists$ a tout d'abord été employée par Giuseppe Peano en 1897 dans le volume II de son Formulaire de mathématiques avec une syntaxe différente, le signe étant directement associé au prédicat ( $\exists \ P$ pour notre $\exists x\ P(x)$ ). Bertrand Russell l'utilise le premier de la façon actuelle, comme lieur de variable.

Ordre des quantificateurs

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.

Quantificateurs en théorie des jeux

Quantificateur ⅁

Le signe majuscule G culbuté sans empattement ou signe majuscule G réfléchi sans empattement ⅁, est un quantificateur utilisé en théorie des jeux^,^,.

Il a la forme d’un G majuscule réfléchi, notamment dans les polices TeX de l’American Mathematical Society, mais a normalement la forme d’un G majuscule culbuté^,, notamment dans les polices STIX (en).

Il est particulièrement utilisé dans le contexte de jeu infini ou de jeu à information parfaite.

Par exemple :

\Game (G,\sigma )

représente un jeu G avec une stratégie $\sigma$ ;

\Game _{\omega }

représente un jeu infini ;

\Game (T,\phi )

représente un jeu avec des règles $T$ et un objectif $\phi$ .

Déduction naturelle

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

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

Exemples

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 ~{\text{chat dans ce groupe,}}{\text{la couleur du chat est noire}}

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

{\displaystyle \exists ~\left({\text{resp.}}\,\exists

Représentation des quantificateurs en Unicode, HTML et LaTeX

	Symbole	Unicode	HTML	LaTeX
pour tout	∀	U+2200	∀	\forall
il existe	∃	U+2203	∃	\exists

Bibliographie

Voir la bibliographie de Logique mathématique.

(en) Barbara Beeton, Addendum to L2/98-405: Request for assignment of codes to mathematical and technical symbols, 22 janvier 1999 (lire en ligne)
(en) Barbara Beeton, Request for assignment of codes to mathematical and technical symbols that do not appear in Unicode 2.0 or ISO/IEC 10646 (revised), 1^er juin 1999 (lire en ligne)
(en) Janós Flesch et Arkadi Predtetchinski, « Parameterized games of perfect information », Annals of Operations Research, vol. 287,‎ 2020, p. 683-699 (DOI 10.1007/s10479-018-3087-5, lire en ligne)
(en) Ph. G. Kolaitis, « Game quantification », dans J. Barwise, S. Feferman, Model-theoretic logics, Association of Symbol Logic / Cambridge University Press, 2017, 2^e éd. (ISBN 9781107168251)
(en) Yiannis N. Moschovakis, Descriptive set theory, Amsterdam, Noord-Holland, 1980 (ISBN 0-444-85305-7, lire en ligne)
(en) Scott Pakin, The Comprehensive LATEX Symbol List, 5 mai 2021 (lire en ligne)
(en) Ken Whistler, Asmus Freytag et AMS (STIX), Encoding Additional Mathematical Symbols in Unicode (revised) (n^o L2/00-119), 19 avril 2000 (lire en ligne)

Références

Cet article est partiellement ou en totalité issu de l'article intitulé « ⅁ » (voir la liste des auteurs).

↑ Informations lexicographiques et étymologiques de « quanteur » dans le Trésor de la langue française informatisé, sur le site du Centre national de ressources textuelles et lexicales.
↑ 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).
1 2 (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) ∃.
↑ (en) Yiannis Moschovakis, chap. 6D « The game quantifier ⅁ », dans Descriptive set theory, vol. 155, Providence, American Mathematical Society, coll. « Mathematical Surveys and Monographs », 8 avril 2009, 2^e éd. (ISBN 978-0-8218-4813-5, lire en ligne [PDF]), p. 244-254.
↑ (en) DYLAN BELLIER, MASSIMO BENERECETTI, DARIO DELLA MONICA et al., « Good-for-Game QPTL: An Alternating Hodges Semantics », ACM Transactions on Computational Logic, vol. 24, n^o 1,‎ janvier 2023, p. 4.1 Quantification Game for Sentences (DOI 10.1145/3565365, lire en ligne, consulté le 23 janvier 2026).
1 2 (en) Erich Grädel, « Automatic Structures: Twenty Years Later », dans Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS ’20), July 8–11, 2020, Saarbrücken, Germany., New York, ACM, 8 juillet 2020 (lire en ligne [PDF]), p. 8 - Model checking games.
↑
« 6X12 should be a turned sans serif G ( $\Game$ ), not a backwards one. »

Beeton 1999a, p. 12
↑ Par exemple dans Moschovakis 1980.
1 2 (en) « \Game | LaTeX Symbol | LatexAI », sur latexai.app (consulté le 28 juin 2025)
↑ (de) Gerhard Gentzen, Untersuchungen über das Logische Schliessen, p. 22.
↑ « Unicode Character 'FOR ALL' (U+2200) ».
1 2 Cf. Table de symboles mathématiques (Chevrons et angles).
↑ « Unicode Character 'THERE EXISTS' (U+2203) ».
1 2 Cf. Croisements et symboles en traits droits.

Voir aussi

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] Informations lexicographiques et étymologiques de « quanteur » dans le Trésor de la langue française informatisé, sur le site du Centre national de ressources textuelles et lexicales.

[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] 1 2 (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) ∃.

[Moschovakis-6D-8] (en) Yiannis Moschovakis, chap. 6D « The game quantifier ⅁ », dans Descriptive set theory, vol. 155, Providence, American Mathematical Society, coll. « Mathematical Surveys and Monographs », 8 avril 2009, 2^e éd. (ISBN 978-0-8218-4813-5, lire en ligne [PDF]), p. 244-254.

[Bellier-9] (en) DYLAN BELLIER, MASSIMO BENERECETTI, DARIO DELLA MONICA et al., « Good-for-Game QPTL: An Alternating Hodges Semantics », ACM Transactions on Computational Logic, vol. 24, n^o 1,‎ janvier 2023, p. 4.1 Quantification Game for Sentences (DOI 10.1145/3565365, lire en ligne, consulté le 23 janvier 2026).

[Grädel-10] 1 2 (en) Erich Grädel, « Automatic Structures: Twenty Years Later », dans Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS ’20), July 8–11, 2020, Saarbrücken, Germany., New York, ACM, 8 juillet 2020 (lire en ligne [PDF]), p. 8 - Model checking games.

[11] 
« 6X12 should be a turned sans serif G ( $\Game$ ), not a backwards one. »

Beeton 1999a, p. 12

[12] Par exemple dans Moschovakis 1980.

[:0-13] 1 2 (en) « \Game | LaTeX Symbol | LatexAI », sur latexai.app (consulté le 28 juin 2025)

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

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

[pour-tout-16] 1 2 Cf. Table de symboles mathématiques (Chevrons et angles).

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

[il-existe-18] 1 2 Cf. Croisements et symboles en traits droits.