Processing math: 100%

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 x0 » porte sur f et x0. 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 x0 est un objet de type X fixé alors Px0 (noté aussi P(x0)) 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, Px est vrai ». Il est noté xX,Px. 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 xX,Px, 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é yX,Py est le même énoncé que xX,Px. 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 xX,Px et xX,Qx, 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,Px. 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,Px, on construit un objet x0 en utilisant les données du contexte de la démonstration et on spécialise l'énoncé en x0. On dit aussi qu'on a appliqué l'hypothèse à x0. On obtient ainsi l'énoncé Px0. L'objet x0 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ù x0 est directement une variable fixée par le contexte, il est important de noter que, dans la formule x,Px, la variable x est liée par le quantificateur tandis que dans la formule Px0, la variable x0 est libre. Cette dernière formule ne constitue un énoncé autonome que parce que x0 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,Px, 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 Px.

Exemple

Soit P un prédicat portant sur les entiers naturels. Si P est vrai pour tout entier n alors P0 est vrai.

example (P :   Prop) (h :  n, P n) : P 0 :=
Démonstration
Il suffit d'appliquer l'hypothèse à n = 0.
  exact h 0,
P :   Prop,
h :  (n : ), P n
 P 0
no goals
QED.
P :   Prop,
h :  (n : ), P n
 P 0

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

Pour démontrer un énoncé de la forme xX,Px, on considère un objet x de type X quelconque, et on démontre Px. 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 Px est valide pour tout x. La démonstration de xX,Px 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.

Exemple

La fonction xx2 est paire.

example :  x : , x^2 = (-x)^2 :=
Démonstration
Soit x un nombre réel.
  intro x,
  (x : ), x ^ 2 = -x ^ 2
x : 
 x ^ 2 = -x ^ 2
Un calcul montre que x2=(x)2.
  compute,
x : 
 x ^ 2 = -x ^ 2
no goals
QED.
  (x : ), x ^ 2 = -x ^ 2

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

Exemple

Soit P et Q deux prédicats portant un entier relatif. On suppose que, n,Pn et n,Pn1Qn. Alors Qn est vrai pour tout n.

example (P Q :   Prop) (hP :  n, P n) (hPQ :  n, P (n-1)  Q n):  n, Q n :=
Démonstration
Soit n un entier relatif. On doit montrer Qn.
  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
Vu l'hypothèse liant P à Q, il suffit de montrer Pn1.
  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)
Ici la variable liée dans l'hypothèse n,Pn nous embrouille un peu mais on peut la renommer en m.
  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)
Maintenant on voit plus clairement qu'il faut appliquer cette hypothèse à n1.
  exact hP (n-1),
P Q :   Prop,
hPQ :  (n : ), P (n - 1)  Q n,
n : ,
hP :  (m : ), P m
 P (n - 1)
no goals
QED.
P Q :   Prop,
hP :  (n : ), P n,
hPQ :  (n : ), P (n - 1)  Q n
  (n : ), Q n

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 ε,ε>0Pε. 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 ε>0Pε 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 Px est vrai ». Il est noté xX,Px. 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 xX,Px, 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é yX,Py est le même énoncé que xX,Px. 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 xX,Px et xX,Qx, il n'y a aucune raison a priori qu'il existe un x vérifiant à la fois Px et Qx. Par exemple, les deux énoncés n,n10 et n,n3 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 xX,Px, il n'y a aucune raison que l'objet x du contexte vérifie Px.

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,Px. 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,Px, on fixe un objet x0 vérifiant Px0. On dit parfois que x0 est un témoin de l'hypothèse x,Px. 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 x0 et d'une hypothèse affirmant Px0 (on note que la variable x0 est libre dans la formule Px0, qui ne constitue un énoncé que parce que x0 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 Px, fixons un tel élément x0 ». 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.

Exemple

Soit Q un énoncé, et P un prédicat portant sur un entier naturel. On suppose que, pour tout entier n, Pn implique Q. S'il existe n tel que Pn alors Q est vrai.

example (Q : Prop) (P :   Prop) (hPQ :  n, P n  Q) :
  ( n, P n)  Q :=
Démonstration
Supposons qu'il existe un entier vérifiant P.
  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
Soit n0 un tel entier.
  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
L'hypothèse faisant intervenir P et Q, appliquée à n0, garantit que Pn0 implique 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
On peut donc en déduire Q.
  exact hPQ hn₀,
Q : Prop,
P :   Prop,
n₀ : ,
hn₀ : P n₀,
hPQ : P n₀  Q
 Q
no goals
QED.
Q : Prop,
P :   Prop,
hPQ :  (n : ), P n  Q
 ( (n : ), P n)  Q

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

Pour démontrer (directement) un énoncé de la forme x,Px, on fournit un témoin x0 produit directement ou indirectement à partir du contexte, puis on montre que Px0 est vrai. On écrira par exemple « Montrons que x0 convient », suivi d'une démonstration de Px0. 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₀.

Exemple

Montrons que l'entier 8 est un multiple de 2.

example :  k : , 8 = 2*k :=
Démonstration
Montrons que 4 convient.
  use 4,
  (k : ), 8 = 2 * k
 8 = 2 * 4
Il s'agit de montrer que 8 = 2*4, ce qui découle de la définition de la multiplication des entiers
  compute,
 8 = 2 * 4
no goals
QED.
  (k : ), 8 = 2 * k

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 δ,δ>0Pδ. 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 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 453 doit être lu comme (45)3 et non comme 4(53). 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 : 456 signifie 4(56) et non pas (45)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 PQR doit être lu P(QR), de sorte qu'il est équivalent à PQR. 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é PQRS se lit P(Q(RS)). 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,PnQ signifie n,(PnQ) et non (n,Pn)Q. De même x,y,PyQx est à lire comme x,(y,(PyQx)) et non pas x,((y,Py)Qx). 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,xn,||x||=0x=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,Pxy est particulièrement fréquent. Les explications des sections précédentes permettent d'utiliser un tel énoncé en le spécialisant à un x0, puis en fixant un y0 vérifiant Px0y0. 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 à x0 fournit y0 tel que Px0y0 ». Cela évite en particulier de d'écrire l'énoncé intermédiaire y,Px0y.

Il faut bien comprendre que, en général, il n'y a aucune raison qu'il existe un y0 convenant simultanément pour tous les x0. Donc on ne peut pas commencer par fixer y0 avant de spécialiser l'énoncé à x0. On insiste parfois sur ce fait en écrivant que « y0 dépend de x0 ». Cette formulation est commode mais un peu piégeuse car elle suggère que y0 est uniquement déterminé par x0, 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 x0 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 (xn), pour obtenir une suite (yn) telle que n,Pxnyn. 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,Pxy alors il existe une fonction f:XY telle que, x,Pxf(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 Pxy(x) » plutôt que « l'hypothèse H et l'axiome du choix fournissent une fonction f telle que Pxf(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.