Quantification (logique)

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

Exemple

La phrase notée symboliquement :

${\displaystyle \forall x\,P(x)}$

se lit :

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

et signifie :

« tout objet du domaine considéré possède la propriété ${\displaystyle P}$ ».

La notation « ${\displaystyle \forall }$ » 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 « ${\displaystyle \exists }$ » pour le quantificateur existentiel qu'il tient de Russell (qui lui-même l'a emprunté à Peano)^[6].

La quantification existentielle (« il existe un ... » au sens « il existe au moins un ... ») se note avec le signe ${\displaystyle \exists }$ (le symétrique axial d'un E, c'est-à-dire, la lettre Ə majuscule). Plus précisément,

${\displaystyle \exists x\,P(x)}$

signifie

${\displaystyle {\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é ${\displaystyle 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,

${\displaystyle \exists !x\,P(x)}$

signifie

${\displaystyle {\text{il existe un unique }}x{\text{ tel que }}P(x)}$, ou encore ${\displaystyle {\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é ${\displaystyle 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

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

La notation ${\displaystyle \exists }$ 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 (${\displaystyle \exists \ P}$ pour notre ${\displaystyle \exists x\ P(x)}$). Bertrand Russell l'utilise le premier de la façon actuelle, comme lieur de variable^[3].

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.

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

Davantage d’informations , ...

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

Fermer

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 :

${\displaystyle \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$ !\right)~{\text{chat dans ce groupe, la couleur du chat est blanche}}}

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)