Prédicats et quantificateurs

Les prédicats

Les énoncés mathématiques intéressants sont le plus souvent des énoncés à propos d'objets mathématiques variables. Par exemple l'énoncé « L'entier $n$ est pair» dépend de la variable $n$. Un tel énoncé est appelé prédicat. Les prédicats peuvent porter sur plusieurs variables, par exemple « la fonction $f$ admet une dérivée au point $x_0$ » porte sur $f$ et $x_0$. Chaque variable fait référence à une type d'objet mathématique bien déterminé : un entier, une fonction réelle à variable réelle, un nombre réel, etc...

Un prédicat ne constitue pas a priori un énoncé autonome, mais peut le devenir si le contexte de l'énoncé ou de la démonstration fixe un valeur pour toutes les variables. On peut aussi spécialiser le prédicat en indiquant explicitement des valeurs pour certaines de ses variables. Lorsque toutes les variables ont ainsi fixées, on obtient un énoncé. Ainsi si $P$ est un prédicat portant sur une variable $x$ de type $X$ et si $x_0$ est un objet de type $X$ fixé alors $P x_0$ (noté aussi $P(x_0)$) est un énoncé.

En Lean, pour exprimer que $P$ est un prédicat portant sur une variable de type $X$, on écrit P : X → Prop, suggérant ainsi que $P$ est une fonction allant de $X$ dans les énoncés. Si $P$ porte sur plusieurs variables, par exemple une variable de type $X$ et une variable de type $Y$, on écrit P : X → Y → Prop, etc... L'interprétation de cette notation est que, pour chaque valeur de type $X$ on obtient une fonction allant de $Y$ dans les énoncés. La spécialisation de P à x₀ est notée P x₀.

Le quantificateur universel

Étant donné un prédicat $P$ portant sur des objets de type $X$, on peut former l'énoncé « pour tout $x$ de type $X$, $P x$ est vrai ». Il est noté $∀ x ∈ X, P x$. On peut voir cet énoncé comme une grande conjonction, portant sur autant d'énoncés qu'il y a d'objets de type $X$ (donc parfois une infinité d'énoncés).

Il est crucial de comprendre que, dans la formule $∀ x ∈ X, P x$, la variable $x$ est liée. Cela signifie qu'elle est enfermée à l'intérieur de la formule, et n'interagit pas avec le monde extérieur, le contexte. En particulier, on peut renommer cette variable. L'énoncé $∀ y ∈ X, P y$ est le même énoncé que $∀ x ∈ X, P x$. Pour la même raison, si $P$ et $Q$ sont deux prédicats portant sur des objets de type $X$, et si on suppose les énoncés $∀ x ∈ X, P x$ et $∀ x ∈ X, Q x$, se demander si la lettre $x$ désigne le même objet dans les deux hypothèses n'a aucun sens.

Dans Lean, on note ∀ x : X, P x (noter le : qui remplace le $∈$). Sur papier comme dans Lean, on peut omettre de préciser le type de l'objet $x$ lorsqu'il n'y a aucune ambigüité sur le type d'objet sur lequel porte le prédicat $P$. On écrit alors $∀ x, P x$. Par exemple, si on sait que $f$ est une fonction d'une variable réelle, l'énoncé $∀ x, f(x) = 0$ est sans ambigüité : il signifie $∀ x ∈ ℝ, f(x) = 0$.

Utilisation d'un énoncé quantifié universellement

Pour utiliser un énoncé de la forme $∀ x, P x$, on construit un objet $x_0$ en utilisant les données du contexte de la démonstration et on spécialise l'énoncé en $x_0$. On dit aussi qu'on a appliqué l'hypothèse à $x_0$. On obtient ainsi l'énoncé $P x_0$. L'objet $x_0$ peut-être directement un élément du contexte ou bien le résultat d'une opération. Par exemple, si $P$ est un prédicat portant sur les entiers naturels, et si $n$ et $n'$ sont deux entiers fixés par le contexte, on peut spécialiser $P$ à $n$ ou bien $n'$ ou bien $n+n'$ par exemple. Dans le cas où $x_0$ est directement une variable fixée par le contexte, il est important de noter que, dans la formule $∀ x, P x$, la variable $x$ est liée par le quantificateur tandis que dans la formule $P x_0$, la variable $x_0$ est libre. Cette dernière formule ne constitue un énoncé autonome que parce que $x_0$ est fixée par le contexte.

Cette distinction est parfois difficile à saisir parce que rien n'interdit au contexte de fixer un objet nommé $x$ et une hypothèse affirmant $∀ x, P x$, en utilisant le même symbole $x$. On peut alors spécialiser l'hypothèse au $x$ fixé, ce qui donne l'impression que le quantificateur a simplement disparu de l'hypothèse. Mais il ne faut pas oublier qu'il est loisible de renommer la variable liée de l'hypothèse pour faire disparaître cette illusion.

Dans Lean, si le contexte contient x₀ : X et h : ∀ x, P x, on peut spécialiser l'hypothèse par la commande specialize h x₀, qui transforme h en P x₀. On peut aussi se référer directement à l'énoncé spécialisé en écrivant h x₀, sans modifier le contexte. On remarquera que cette notation suggère que l'hypothèse $h$ est une fonction qui transforme $x$ en démonstration de $P x$.

example (P : ℕ → Prop) (h : ∀ n, P n) : P 0 :=

  exact h 0,

P : ℕ → Prop,
h : ∀ (n : ℕ), P n
⊢ P 0

no goals

Démonstration d'un énoncé quantifié universellement

Pour démontrer un énoncé de la forme $∀ x ∈ X, P x$, on considère un objet $x$ de type $X$ quelconque, et on démontre $P x$. Il est important de noter que $x$ est fixé durant toute la démonstration. Comme rien de spécifique concernant $x$ n'est supposé, la démonstration assure bien que $P x$ est valide pour tout $x$. La démonstration de $∀ x ∈ X, P x$ pourra donc commencer par la phrase « Soit $x$ dans $X$ » ou « Fixons $x$ dans $X$ ». Selon la nature de $X$, d'autres formulations sont possibles, comme « Soit $x$ un nombre réel » ou « Soit $f$ une fonction de $ℝ$ dans $ℝ$ ».

Il est crucial de ne plus modifier, ou sembler modifier un objet $x$ ainsi fixé. En particulier, on évitera de réutiliser la lettre $x$ comme variable liée, par exemple dans autre un énoncé quantifié. Même si une telle utilisation n'est pas une faute logique en elle-même, elle induit un grand risque de confusion, chez le lecteur comme chez l'auteur.

example : ∀ x : ℝ, x^2 = (-x)^2 :=

  intro x,

⊢ ∀ (x : ℝ), x ^ 2 = -x ^ 2

x : ℝ
⊢ x ^ 2 = -x ^ 2

  compute,

x : ℝ
⊢ x ^ 2 = -x ^ 2

no goals

Revenons maintenant sur la question des variables liées. Dans Lean, on peut utiliser la commande rename_var pour renommer une variable liée. Lean n'en a jamais besoin, cette commande ne sert qu'à éclaircir les choses pour les humains, comme dans l'exemple suivant (nous verrons des exemples plus convainquant dans les démonstrations d'analyse).

example (P Q : ℤ → Prop) (hP : ∀ n, P n) (hPQ : ∀ n, P (n-1) → Q n): ∀ n, Q n :=

  intro n,

P Q : ℤ → Prop,
hP : ∀ (n : ℤ), P n,
hPQ : ∀ (n : ℤ), P (n - 1) → Q n
⊢ ∀ (n : ℤ), Q n

P Q : ℤ → Prop,
hP : ∀ (n : ℤ), P n,
hPQ : ∀ (n : ℤ), P (n - 1) → Q n,
n : ℤ
⊢ Q n

  apply hPQ,

P Q : ℤ → Prop,
hP : ∀ (n : ℤ), P n,
hPQ : ∀ (n : ℤ), P (n - 1) → Q n,
n : ℤ
⊢ Q n

P Q : ℤ → Prop,
hP : ∀ (n : ℤ), P n,
hPQ : ∀ (n : ℤ), P (n - 1) → Q n,
n : ℤ
⊢ P (n - 1)

  rename_var n m at hP,

P Q : ℤ → Prop,
hP : ∀ (n : ℤ), P n,
hPQ : ∀ (n : ℤ), P (n - 1) → Q n,
n : ℤ
⊢ P (n - 1)

P Q : ℤ → Prop,
hPQ : ∀ (n : ℤ), P (n - 1) → Q n,
n : ℤ,
hP : ∀ (m : ℤ), P m
⊢ P (n - 1)

  exact hP (n-1),

P Q : ℤ → Prop,
hPQ : ∀ (n : ℤ), P (n - 1) → Q n,
n : ℤ,
hP : ∀ (m : ℤ), P m
⊢ P (n - 1)

no goals

La quantification universelle implicite

Bien des affirmations mathématiques sont en fait implicitement des énoncés quantifiés universellement. Par exemple l'affirmation : « Soit $f$ une fonction réelle d'une variable réelle. Si $f$ est dérivable alors elle est continue » est quantifiée universellement. On peut la réécrire « Pour toute fonction $f$ réelle d'une variable réelle, si $f$ est dérivable alors elle est continue ». De façon plus cachée, on peut écrire « Les médiatrices d'un triangle sont concourantes » plutôt que « Pour tout triangle ABC, les médiatrices de ABC sont concourantes ». Comme le montre ce dernier exemple, ce mode d'expression est souvent très commode par sa concision. Le prix à payer pour cette concision est une augmentation de la quantité d'information implicite.

Au niveau de la démonstration, l'avantage de la quantification universelle implicite est qu'il devient inutile d'introduire les objets mathématiques quantifiés.

Ce raccourci est aussi disponible dans Lean, et il a en fait été abondamment utilisé dans tous les exemples présentés jusque ici. Tous les objets mentionnés dans le contexte, à gauche du : introduisant l'énoncé à démontrer, sont quantifiés universellement.

La quantification universelle bornée

Il est parfois commode de restreindre immédiatement la portée d'un quantificateur universel en imposant une condition sur l'objet lié. Ainsi on écrira souvent $∀ ε > 0, P ε$. Il s'agit d'une abréviation qui remplace la forme explicite $∀ ε ∈ ℝ, ε > 0 ⇒ P ε$. Il s'agit d'une abréviation utile mais il faudra y prêter une attention particulière lors de la négation d'énoncés dans le chapitre suivant. De façon plus terre à terre, il faut prendre garde à ne pas écrire de chimère mêlant l'abréviation et sa définition, comme $∀ ε > 0 ⇒ P ε$ qui ne veut rien dire du tout.

Lean comprend cette abréviation, on peut écrire ∀ ε > 0, P ε. Par contre il a tendance à ne pas l'utiliser dans l'affichage du contexte et du but, préférant afficher ∀ ε : ℝ, ε > 0 → P ε.

Exercices

Les fichier Lean correspondant à cette première partie de chapitre sont ici.

Le quantificateur existentiel

Étant donné un prédicat $P$ portant sur des objets de type $X$, on peut former l'énoncé « il existe $x$ de type $X$ tel que $P x$ est vrai ». Il est noté $∃ x ∈ X, P x$. On peut voir cet énoncé comme une grande disjonction, portant sur autant d'énoncés qu'il y a d'objets de type $X$ (donc parfois une infinité d'énoncés).

Il est crucial de comprendre que, dans la formule $∃ x ∈ X, P x$, la variable $x$ est liée. Cela signifie qu'elle est enfermée à l'intérieur de la formule, et n'interagit pas avec le monde extérieur, le contexte. En particulier, on peut renommer cette variable. L'énoncé $∃ y ∈ X, P y$ est le même énoncé que $∃ x ∈ X, P x$. Pour la même raison, si $P$ et $Q$ sont deux prédicats portant sur des objets de type $X$, et si on suppose les énoncés $∃ x ∈ X, P x$ et $∃ x ∈ X, Q x$, il n'y a aucune raison a priori qu'il existe un $x$ vérifiant à la fois $P x$ et $Q x$. Par exemple, les deux énoncés $∃ n ∈ ℕ, n ≥ 10$ et $∃ n ∈ ℕ, n ≤ 3$ sont vrais, mais il n'existe aucun entier naturel qui soit supérieur à $10$ et inférieur à $3$. De même, si le contexte comporte un objet nommé $x$ et une hypothèse assurant $∃ x ∈ X, P x$, il n'y a aucune raison que l'objet $x$ du contexte vérifie $P x$.

Dans Lean, on écrit ∃ x : X, P x (noter le : qui remplace le $∈$). Sur papier comme dans Lean, on peut omettre de préciser le type de l'objet $x$ lorsqu'il n'y a aucune ambigüité sur le type d'objet sur lequel porte le prédicat $P$. On écrit alors $∃ x, P x$. Par exemple, si on sait que $f$ est une fonction d'une variable réelle, l'énoncé $∃ x, f(x) = 0$ est sans ambigüité : il signifie $∃ x ∈ ℝ, f(x) = 0$.

Utilisation d'un énoncé quantifié existentiellement

Pour utiliser un énoncé de la forme $∃ x, P x$, on fixe un objet $x_0$ vérifiant $P x_0$. On dit parfois que $x_0$ est un témoin de l'hypothèse $∃ x, P x$. Le nom de cet objet est laissé au choix de l'auteur de la démonstration, sous la seule contrainte de ne pas réutiliser un nom désignant déjà un objet fixé par le contexte. Le contexte s'enrichit alors d'un nouvel objet $x_0$ et d'une hypothèse affirmant $P x_0$ (on note que la variable $x_0$ est libre dans la formule $P x_0$, qui ne constitue un énoncé que parce que $x_0$ est fixé par le contexte). Ce nouvel objet reste fixé durant toute la suite de la démonstration (ou sous-démonstration en cas d'embranchement). Il est important de bien comprendre cela car, en général, de nombreux $x$ conviennent comme témoins d'existence, et le fait de changer de témoin en cours de route peut complètement invalider une démonstration.

D'un point de vue stratégique, on peut retenir qu'il n'y a aucun inconvénient à fixer un témoin d'existence. Mieux, on peut retenir qu'une hypothèse d'existence est inutilisable sans fixer un témoin (les utilisations qui semblent s'en passer ne sont que des raccourcis de langage). Au contraire, le fait de « faire disparaître un $∀$ » en le spécialisant est une opération a priori risquée.

Pour la rédaction, on pourra écrira par exemple : « On sait qu'il existe $x$ vérifiant $P x$, fixons un tel élément $x_0$ ». On rencontre souvent une forme plus fluide qui omet la deuxième partie de la phrase, le nom choisi étant alors systématiquement celui apparaissant de façon liée dans l'hypothèse. Ce raccourci commode présente l'inconvénient de donner l'illusion qu'on a simplement retiré de le quantificateur dans l'hypothèse. Et bien sûr il est très dangereux lorsque plusieurs hypothèses sont des énoncés quantifiés existentiellement sur le même type d'objet mathématique, comme dans l'exemple portant sur les entiers naturels dans le paragraphe précédent.

On notera aussi qu'il y a une ressemblance trompeuse entre la démonstration d'un énoncé quantifié universellement $∀ x, Px$ et l'utilisation d'un énoncé quantifié existentiellement $∃ x, Px$. Dans les deux cas on commence par enrichir le contexte d'un nouvel objet $x$, qui sera fixé dans la suite. Mais dans le premier cas il faut ensuite démontrer $Px$, tandis que dans le second on peut utiliser $Px$. Afin d'éviter de confondre ces deux mécanismes, le plus simple est de bien réserver le verbe « Soit » au premier cas et « Fixons » au second (malheureusement on rencontre les deux verbes utilisés dans les deux cas).

Dans Lean, si le contexte contient h : ∃ x, P x, on peut fixer un témoin x₀ et une hypothèse hx₀ affirmant P x₀ par la commande cases h with x₀ hx₀. Hélas Lean n'émet aucune protestation si le nom x₀ est déjà utilisé, il créé simplement un nouvel objet portant ce nom, et toute mention ultérieure de x₀ se réfère au dernier objet créé sous ce nom. Le même problème se pose pour la commande intro.

example (Q : Prop) (P : ℕ → Prop) (hPQ : ∀ n, P n → Q) :
  (∃ n, P n) → Q :=

  intro hP,

Q : Prop,
P : ℕ → Prop,
hPQ : ∀ (n : ℕ), P n → Q
⊢ (∃ (n : ℕ), P n) → Q

Q : Prop,
P : ℕ → Prop,
hPQ : ∀ (n : ℕ), P n → Q,
hP : ∃ (n : ℕ), P n
⊢ Q

  cases hP with n₀ hn₀,

Q : Prop,
P : ℕ → Prop,
hPQ : ∀ (n : ℕ), P n → Q,
hP : ∃ (n : ℕ), P n
⊢ Q

Q : Prop,
P : ℕ → Prop,
hPQ : ∀ (n : ℕ), P n → Q,
n₀ : ℕ,
hn₀ : P n₀
⊢ Q

  specialize hPQ n₀,

Q : Prop,
P : ℕ → Prop,
hPQ : ∀ (n : ℕ), P n → Q,
n₀ : ℕ,
hn₀ : P n₀
⊢ Q

Q : Prop,
P : ℕ → Prop,
n₀ : ℕ,
hn₀ : P n₀,
hPQ : P n₀ → Q
⊢ Q

  exact hPQ hn₀,

Q : Prop,
P : ℕ → Prop,
n₀ : ℕ,
hn₀ : P n₀,
hPQ : P n₀ → Q
⊢ Q

no goals

Démonstration d'un énoncé quantifié existentiellement

Pour démontrer (directement) un énoncé de la forme $∃ x, P x$, on fournit un témoin $x_0$ produit directement ou indirectement à partir du contexte, puis on montre que $P x_0$ est vrai. On écrira par exemple « Montrons que $x_0$ convient », suivi d'une démonstration de $P x_0$. Par exemple, si le contexte mentionne deux entiers $n$ et $n'$ et que $P$ est un prédicat sur les entiers, on pourra écrire « Montrons que $n$ convient » ou « Montrons que $n+n'+3$ convient ».

Dans Lean, la commande pour affirmer que x₀ convient est use x₀.

example : ∃ k : ℕ, 8 = 2*k :=

  use 4,

⊢ ∃ (k : ℕ), 8 = 2 * k

⊢ 8 = 2 * 4

  compute,

⊢ 8 = 2 * 4

no goals

La quantification existentielle implicite

Les quantificateurs existentiels implicites sont plus rares que leurs homologues universels, mais on les rencontre malgré tout. Ainsi l'énoncé « Les médiatrices d'un triangle sont concourantes » cache, en plus d'une quantification universelle sur les triangles, l'énoncé $∃ O, O ∈ Δ_1 ∩ Δ_2 ∩ Δ_3$ où les $Δ_i$ sont les médiatrices du triangle.

La quantification existentielle bornée

Il est parfois commode de condenser une quantification existentielle et une affirmation portant sur l'objet quantifié. Par exemple, dans un cours sur les limites de fonctions d'une variable réelle, $∃ δ > 0, P δ$ est l'abréviation de $∃ δ ∈ ℝ, δ > 0 ∧ P δ$. Il s'agit d'une abréviation utile mais il faudra y prêter une attention particulière lors de la négation d'énoncés dans le chapitre suivant. De façon plus terre à terre, il faut prendre garde à ne pas écrire de chimère mêlant l'abréviation et sa définition, comme $∃ δ > 0 \text{ et } P ε$ qui ne veut rien dire du tout.

Lean n'a aucun problème pour lire une telle forme abrégée mais il a tendance à l'afficher sous la forme ∃ δ : ℝ, ∃ H : δ > 0, P δ, ce qui est pour le moins déroutant (cela se lit : « il existe un nombre réel $δ$ et il existe une démonstration $H$ de la stricte positivité de $δ$, tels que $P δ$ »). On peut utiliser la commande de réécriture rw exists_prop pour convertir cet énoncé en ∃ δ : ℝ, δ > 0 ∧ P δ. Mais on peut aussi travailler directement avec cette formulation regrettable. S'il s'agit du but à démontrer, on utilisera deux fois use pour proposer successivement une valeur de δ et une démonstration de positivité. S'il s'agit d'une hypothèse h, on pourra en extraire l'information à l'aide de deux cases successifs, ou bien par rcases h with ⟨δ, δ_pos, hP⟩.

Priorité, associativité et commutativité des symboles logiques

Dans ce cours et le précédent, nous avons introduit plusieurs connecteurs logiques et quantificateurs qui peuvent être combinés pour former des énoncés plus intéressants. Comme dans le cas des opérations arithmétiques, il est important de garder en tête les règles de priorité et d'associativité. Ainsi on sait que $4 + 5×3$ doit être lu comme $4 + (5×3)$ et nos comme $(4 + 5)×3$ car la multiplication est prioritaire sur l'addition. De plus on sait que $4 - 5 - 3$ doit être lu comme $(4 - 5) - 3$ et non comme $4 - (5 - 3)$. Cela est important car, comme la division mais contrairement à l'addition et à la multiplication, la soustraction n'est pas associative. L'exponentiation n'est pas non plus associative, mais suit la convention opposée à celle de la soustraction : $4^{5^6}$ signifie $4^{(5^6)}$ et non pas $(4^5)^6$.

L'ordre de priorité des opérateurs logiques rencontrés pour l'instant est $∧$, $∨$, $⇔$, $⇒$. De plus les trois premiers sont associatifs, tandis que $⇒$ ne l'est pas. Un énoncé de la forme $P ⇒ Q ⇒ R$ doit être lu $P ⇒ (Q ⇒ R)$, de sorte qu'il est équivalent à $P ∧ Q ⇒ R$. Les opérateurs $∧$, $∨$ et $⇔$ sont commutatifs (on obtient des énoncés équivalent en permutant les deux opérandes), mais $⇒$ ne l'est pas en général.

Par exemple l'énoncé $P ⇒ Q ∨ R ∧ S$ se lit $P ⇒ (Q ∨ (R ∧ S))$. En pratique, on rencontre assez peu d'énoncé de ce type, et on ajoute fréquemment des parenthèses, mêmes lorsqu'elles sont théoriquement inutiles. Cependant Lean a tendance à retirer les parenthèses inutiles lors de l'affichage du contexte et du but, il est donc utile de connaître l'ordre de priorité, ou au moins être conscient que ces règles peuvent expliquer un affichage qui semble bizarre.

Les quantificateurs quant à eux lient une variable à un énoncé le plus grand possible. Ainsi $∃ n, P n ⇒ Q$ signifie $∃ n, (P n ⇒ Q)$ et non $(∃ n, P n) ⇒ Q$. De même $∃ x, ∀ y, P y → Q x$ est à lire comme $∃ x, (∀ y, (P y → Q x))$ et non pas $∃ x, ((∀ y, P y) → Q x)$. On commence à voir dans cet exemple l'intérêt de conventions supprimant un maximum de parenthèse. Contrairement à l'exemple artificiel du paragraphe précédent, ce genre d'empilement de quantificateurs est très courant en analyse.

On peut permuter deux quantificateurs existentiels pourvu que le type d'objet sur lequel a lieu la deuxième quantification ne dépende pas du premier objet quantifié. Ainsi, si $P$ est un prédicat portant sur deux entiers naturels, les énoncés $∀ n, ∀ m, P(n, m)$ et $∀ m, ∀ n, P(n, m)$ sont équivalents. Par contre on ne peut évidemment par réorganiser $∀ n, ∀ x ∈ ℝ^n, ||x|| = 0 ⇒ x = 0$ car la formule obtenue n'aurait plus aucun sens.

De même on peut permuter deux quantificateurs existentiels pourvu que le type d'objet sur lequel porte la deuxième quantification ne dépende pas du premier objet quantifié.

Dans les deux cas, on peut retenir en première approximation que l'on peut permuter les quantificateurs quand ils sont de même nature. Le plus souvent, les exceptions amènent à des énoncés visiblement dépourvu de sens. Au contraire il ne faut surtout pas permuter un quantificateur universel et un quantificateur existentiel. En général l'énoncé obtenu a bien un sens, mais il n'est pas du tout équivalent à l'énoncé de départ. Par exemple, l'énoncé $∀ x ∈ ℝ, ∃ n ∈ ℕ, x < n$ est vrai, c'est la propriété d'Archimède des nombres réels. Mais l'énoncé $∃ n ∈ ℕ, ∀ x ∈ ℝ, x < n$ est évidemment faux : nul entier n'est supérieur à tous les nombres réels !

Utilisation d'un $∀ x, ∃ y$ et axiome du choix

L'enchaînement de quantificateurs $∀ x, ∃ y, P\, x\, y$ est particulièrement fréquent. Les explications des sections précédentes permettent d'utiliser un tel énoncé en le spécialisant à un $x_0$, puis en fixant un $y_0$ vérifiant $P\, x_0\, y_0$. Pour obtenir une rédaction fluide, il vaut mieux faire les deux opérations en une seule phrase, par exemple : « l'hypothèse $H$ appliquée à $x_0$ fournit $y_0$ tel que $P\, x_0\, y_0$ ». Cela évite en particulier de d'écrire l'énoncé intermédiaire $∃ y, P\, x_0\, y$.

Il faut bien comprendre que, en général, il n'y a aucune raison qu'il existe un $y_0$ convenant simultanément pour tous les $x_0$. Donc on ne peut pas commencer par fixer $y_0$ avant de spécialiser l'énoncé à $x_0$. On insiste parfois sur ce fait en écrivant que « $y_0$ dépend de $x_0$ ». Cette formulation est commode mais un peu piégeuse car elle suggère que $y_0$ est uniquement déterminé par $x_0$, ce qui n'est pas le cas en général.

Dans certaines situations, on veut faire cette double opération de spécialisation et extraction de témoin non pour un unique $x_0$ mais pour une famille infinie. Par exemple si $x$ et $y$ sont réels, on peut vouloir spécialiser à tous les termes d'une suite $(x_n)$, pour obtenir une suite $(y_n)$ telle que $∀ n, P\, x_n\, y_n$. Les définitions et règles introduites jusqu'ici ne permettent pas d'obtenir cela en consommant une quantité finie d'encre. On rajoute donc une nouvelle règle appelée axiome du choix. Elle stipule que, pour types d'objets $X$ et $Y$, si $∀ x, ∃ y, P\, x\, y$ alors il existe une fonction $f : X → Y$ telle que, $∀ x, P\, x\, f(x)$.

Dans les cours élémentaires, cette règle n'est presque jamais invoquée explicitement. Un camouflage fréquent consiste à écrire « d'après l'hypothèse $H$, il existe $y(x)$ tel que $P\, x\, y(x)$ » plutôt que « l'hypothèse $H$ et l'axiome du choix fournissent une fonction $f$ telle que $P\, x\, f(x)$ ».

L'axiome du choix est une règle purement mathématique. Elle n'a aucun contenu algorithmique car elle affirme qu'on peut choisir parmi les $y$ convenant pour chaque $x$. Or, si $X$ est infini, il y a un nombre infini de tels choix à faire, en un temps fini. On ne peut donc pas écrire un programme se basant sur cette règle pour calculer quelque chose. Bien sûr cette impossibilité de calculer n'empêche pas l'ordinateur de raisonner en utilisant cette règle. Dans Lean, étant donnée une hypothèse h : ∀ x, ∃ y, P x y, la commande choose f hf using h rajoute au contexte une fonction f : X → Y et l'hypothèse hf : ∀ x, P x (f x).

Le cours continue avec le chapitre 4 qui aborde les négations d'énoncés, le raisonnement par l'absurde et la contraposition.