Accueil

Logique intuitionniste et maths constructives.

Tout au long de notre développement de la logique classique, on a construit les règles du raisonnement valide d'une façon qui collait avec "le bon sens". Mais comme on l'a vu, ces règles ne sont pas sans poser quelques problèmes et paradoxes.

Fig.1 - Développement d'une logique qui fasse le café (vue d'artiste).

Un de ces problèmes provient non pas de la logique elle-même, mais des mathématiques qu'on peut faire avec. Pour les intuitionnistes, némésis du projet de Hilbert, un énoncé mathématique affimant l'existence d'un certain objet ne devrait pas être considéré comme prouvé si la preuve n'indique pas comment construire cet objet. Ce qui les fâche, donc, c'est le raisonnement par l'absurde: une façon de prouver qu'un objet existe, en logique classique, est de supposer qu'il n'existe pas, et d'aboutir à une contradiction. Alors, puisqu'il ne peut pas ne pas exister, c'est donc qu'il existe ! Mais on n'est pas plus avancé s'il s'agit de le trouver. La logique intuitionniste ne pas permet pas cette facilité. Cela peut sembler un peu gratuit, comme de se lancer dans le saut à la perche sans perche, mais avec l'importance croissante de l'informatique, les preuves qui fournissent un algorithme pour construire les objets mathématiques ont le vent en poupe.

Logique intuitionniste et maths constructives

Pour mener à bien l'éradication des preuves non constructives, il faut commencer par en identifier les sources. Qu'est-ce qui fait marcher le raisonnement par l'absurde ? Qu'est-ce qu'on utilise quand on affirme que, si "non p" mène à une contradiction, et est donc fausse, alors "p" doit être vraie ? La version formelle de ce raisonnement s'appelle la "loi du tiers exclus", qui, en hiéroglyphes logiques, s'écrit $P \vee \neg P$. Et d'où vient cette loi ? Parmi nos axiomes logiques, il se trouve que le coupable est la règle d'élimination des doubles négations (notée $\neg E$), qui affirme que de "non non P", il est licite de déduire "P".


Pour une proposition $P$ donnée, on cherche à obtenir $\vdash P \vee \neg P$. On utilise les notations et axiomes logiques présentés ici. $$\begin{align} &(i)\ (P, \neg ( P \vee \neg P)) \vdash \neg ( P \vee \neg P) \text{ par (As)}\\ &(ii)\ (P, \neg(P \vee \neg P)) \vdash P,\text{ par (As)}\\ &(iii)\ (P, \neg ( P \vee \neg P)) \vdash ( P \vee \neg P),\text{ par ($\vee I$) et (ii)}\\ &(iv)\ ( \neg(P \vee \neg P)) \vdash \neg P,\text{ par ($\neg$ I) sur (i) et (iii)}\\ &(v)\ (\neg P, \neg ( P \vee \neg P)) \vdash \neg ( P \vee \neg P) \text{ par (As)}\\ & (vi)\ (\neg P, \neg ( P \vee \neg P)) \vdash \neg P \text{ par (As)}\\ &(vii)\ (\neg P, \neg ( P \vee \neg P)) \vdash P \vee \neg P \text{ par ($\vee$I) sur (vi)}\\ &(viii)\ (\neg ( P \vee \neg P)) \vdash \neg \neg P \text{ par ($\neg$ I) sur (v) et (vii)}\\ &(ix)\ \vdash \neg\neg ( P \vee \neg P) \text{ par ($\neg$ I) sur (iv) et (viii)}\\ \end{align}$$ et c'est là qu'on a besoin de l'élimination des doubles négations pour conclure que $$ \vdash P \vee \neg P.$$


Puisque cet axiome est à la source de tous les maux des intuitionnistes, la solution est donc...de s'en débarrasser. Les axiomes de la logique intuitionniste sont ceux de la logique classique, moins l'élimination des doubles négations et tout ce qui en résulte, notamment la loi du tiers exclus et le problématique Ex Falso Quodlibet (qui affirme que d'une proposition fausse, on peut déduire tout autre proposition). On appelle "mathématiques constructives" les mathématiques basées sur cette logique, et, selon Brouwer, ce sont les seules mathématiques qui garantissent qu'on ne raconte pas n'importe quoi.

La question devient alors "Qu'a-t-on vraiment sacrifié ?". Autrement dit, quelles parties des mathématiques dépendent de ces axiomes, et parmi celles-ci, lesquelles peuvent-être "constructivisées" ?

A première vue, tout cela peut sembler déraisonnable. La loi du tiers exclus dit qu'"une proposition est soit vraie, soit fausse". Les intuitionnistes essaient-ils donc de faire de la logique avec des propositions qui sont vraies et fausses à la fois ?

En fait, non. Notons $\perp$ une proposition fausse quelconque, et remarquons que $\neg P$ est une abbréviation de $P\Rightarrow \perp$. Alors on peut montrer, en restant intuitionnistes, qu'il n'y a pas de proposition $P$ telle qu'on ait à la fois $P$ et $\neg P$. En effet, on aurait alors à la fois $P$ et $P \Rightarrow \perp$, autrement dit, par modus ponens (noté ($\Rightarrow$E)), on aboutit à $\perp$: contradiction. Donc il n'y a pas de telle proposition.

...me direz-vous, c'est un raisonnement par l'absurde ! On n'y a pas droit !

Et c'est là l'un des points vraiment subtils des mathématiques constructives: il faut faire une distinction entre les raisonnements par contradiction et les raisonnements par négation. En mathématiques "habituelles", on appelle généralement "raisonnement par l'absurde" tout raisonnement qui commence par "Supposons P", et aboutit à une contradiction ($\perp$). Mais il y a en fait deux types de preuve de ce type:

  1. La preuve par négation: Pour prouver $\neg P$, on suppose $P$ et on démontre une contradiction. Ainsi, on utilise simplement la reformulation de $\neg P$ en $P \Rightarrow \perp$: cela ne contredit pas les préceptes intuitionnistes. Par exemple, la démonstration classique de l'irrationalité de $\sqrt 2$ est une preuve par négation, et ce théorème est donc tout à fait acceptable pour l'intuitionnisme. Il en est de même du théorème de Russel qui affirme qu'il n'existe pas d'ensemble de tous les ensembles.

  2. La preuve par contradiction: Pour prouver $P$, on suppose $\neg P$ et on démontre une contradiction. C'est ce raisonnement qui est rejeté par l'intuitionnisme. Ce qui est caché dessous, c'est que, par définition, il nous permet d'aboutir à $\neg \neg P$, mais sans élimination des doubles négations, on ne peut pas aller plus loin.

On veut donc identifier et exterminer les parties des mathématiques qui dépendent du second type de preuve. C'est d'autant plus difficile que l'élimination des double négations est extrêmement naturelle, et que dans le langage "de tous les jours", on le fait automatiquement, car les doubles négations sont franchement disgracieuses. Il va donc falloir faire preuve de vigilance. De manière générale, la méthode constructiviste généralise l'approche classique, puisque tout théorème prouvé constructivement est, a fortiori, prouvé "classiquement".

Certains théorèmes sont classiquement démontrés par contradiction, mais on peut trouver une autre preuve qui, elle, soit constructive (et donc valide suivant la logique intuitionniste). Par exemple:

Il existe deux irrationnels $a$ et $b$ tels que $a^b$ est rationnel.


Preuve "classique": Par la règle du tiers exclus, soit $\sqrt {2}^{\sqrt 2}$ est rationnel, soit il ne l'est pas. S'il l'est, on prend $a=b=\sqrt 2$; sinon, on prend $a = \sqrt{2}^{\sqrt 2}$ et $b \sqrt {2}$.

Preuve constructive: Montrons d'abord que $\log_2 (9)$ est irrationnel. On peut procéder par négation: supposons que $\log_2(9) = \frac pq$, pour deux entiers non nuls $p$ et $q$. Alors, par définition du logarithme de base 2, $2^{\log_2(9)} = 2^{\frac pq}$, c'est-à-dire $9 = 2^{\frac pq}$, ou encore $9^q = 2^p$. C'est une contradiction, car $9^q$ est un entier impair et $2^p$ un entier pair. Donc $\log_2 (9)$ est irrationnel et on peut poser $a=\sqrt2$, $b= \log_2 (9)$ et alors

$$a^b = (\sqrt 2)^{\log_2(9)} = \sqrt{2^{\log_2(9)}} = \sqrt{9} = 3$$

Certains cas particuliers du tiers exclus peuvent aussi être récupérés (tout ce qui est interdit, c'est la loi "générale" du tiers exclus). Ainsi, on peut montrer:

Tout entier $n$ est soit nul, soit non nul.



On va montrer, par récurrence, que pour tout entier $n$, soit $n=0$, soit $n\neq 0$

  • Initialisation: Pour $n=0$, on est dans le premier cas.
  • Hérédité: Supposons que $(n=0)$ ou $(n \neq 0)$ et montrons-le pour $n+1$. Dans les deux cas, $n+1$ est le successeur de $n$, et, d'après le troisième axiome de l'arithmétique, 0 n'est le successeur d'aucun entier. Donc $n+1 \neq 0$.


Dans le même ordre d'idées, on récupère, par récurrence, les propriétés de type "tiers exclus" suivantes:

  • Un entier est soit pair, soit impair.
  • Deux entiers quelconques sont soit égaux, soit différents. En fait, c'est aussi vrai pour les rationnels.
  • Pour deux entiers $a$ et $b$, soit $a$ divise $b$, soit $a$ ne divise pas $b$.
  • Pour deux rationnels $p$ et $q$ quelconques, soit $p< q$, soit $p = q$, soit $p> q$.

Cependant, tous les théorèmes ne peuvent être "récupérés" de cette façon. Notamment, les propositions qui sont, en fait, équivalentes au tiers exclus ne peuvent pas être prouvées de façon constructive. Par exemple:

La règle du tiers exclus est équivalent au fait que tout sous-ensemble d'un ensembles fini est fini.



Supposons que la règle du tiers exclus soit vraie. Alors, si $A= \{a_1, \dots, a_n\}$ est un ensemble fini, et $B\subset A$ un sous ensemble, on considère $a_1$: par tiers exclus, soit $a_1 \notin B$ auquel cas on passe au suivant, soit $a_1\notin B$, et on le note $b_1$, puis on passe au suivant. On regarde ainsi à tour de rôle chaque élément de $A$, et lorsqu'on arrrive à $a_n$, on s'arrête: on a alors $B=\{b_1,\dots,b_k\}$, donc $B$ est en bijection avec $\{1,2\dots,k\}$; autrement dit il est fini.
Réciproquement, supposons que tout sous -ensemble d'un ensemble fini soit fini. Soit $P$ une proposition quelconque, il s'agit de montrer qu'on a soit $P$, soit $\neg P$. Considérons pour cela l'ensemble fini $A= \{0\}$, et le sous-ensemble $B=\{x \in A \text{ tel que } P\}$. C'est une formulation un peu bizarre puisque $x$ n'a rien à voir avec $P$, mais c'est parfaitement licite en théorie des ensembles. Mais alors par hypothèse, $B$ est un ensemble fini: il a donc un certain nombre d'éléments, disons $m$. Si $m=0$, $B$ est vide et donc 0 ne vérifie pas $P$: donc $P$ est fausse. Si $m >0$, alors 0 vérifie $P$, autrement dit $P$ est vraie. Ainsi, on a bien le tiers exclus pour $P$.


A ce stade, la méthode constructive semble cher payée: elle nous coûte une proposition tout de même fondamentale. Doit-on donc admettre que certains ensembles finis ont des sous-ensembles infinis ? Cela peut sembler étrange, mais après tout, ce n'est pas comme si on pouvait vérifier tous les ensembles finis, un par un, pour s'en assurer.

Les choses empirent quand on s'approche des réels et de l'analyse. Ainsi, on ne peut pas montrer constructivement que, pour tous réels $x$ et $y$, soit $x< y$, soit $x=y$, soit $x> y$. Le théorème des valeurs intermédiaires, prouvé par exemple par dichotomie, repose lui aussi sur le tiers exclus, et ne peut être récupéré en analyse constructive.

Avec un peu d'astuce, on peut en effet relier le signe d'un réel bien choisi avec l'affirmation qu'une certaine proposition est soit vraie, soit fausse. Considérons par exemple une propriété P des entiers, dont on ignore si $\forall n P(n)$ ou si $\exists n \neq P(n)$ (autrement dit, on n'a de preuve constructive pour aucune de ces deux propositions) et posons

$$ x = \sum_{n=0}^{\infty} \frac{(-1)^n}{2^n} x_n,\ \text{ où } x_n= \begin{cases} 1 \text{ si P(n) est fausse,}\\ 0 \text{ si P(n) est vraie} \end{cases} $$

Ce $x$ vaut 0 si et seulement si $\forall\,n\, P(n)$ de pi, il est strictement positif si, et seulement si, $P(n)$ est fausse pour un entier pair, et négatif si et seulement si P(n) est fausse pour un entier impair. Donc, si on avait une manière constructive de déterminer le signe de $x$, ce serait aussi une méthode constructive de décider $P$.

Ceci peut sembler assez dramatique: sans notion d'ordre, il va être difficile de faire de l'analyse ! Mais on peut en fait prouver constructivement des théorèmes proches. On peut notamment montrer que

  • Pour tous réels $x$ et $y$, si $x\nless y$ et $x \ngtr y$ alors $x=y$
  • Pour tous réels $x$, $y$ et pour tout entier $n$, soit $x< y+ \frac 1n$, soit $x > y - \frac 1n$

L'analyse constructive n'en est pas moins une contrée étrange. Ainsi, on ne peut pas construire de fonction discontinue. Par exemple, l'un des exemple les plus simples de fonctions discontinues:

$$ f(x) = \begin{cases} 0 \text{ si } x<0\\ 1 \text{ sinon} \end{cases} $$

ne peut pas être défini en mathématiques constructives, puisqu'on ne peut pas décider, pour tout réel $x$, s'il est plus grand ou plus petit que 0. Cela ne signifie pas que le théorème "Toutes les fonctions sont continues" est démontrable en mathématiques constructives; simplement, on ne peut pas construire de contre-exemple.

D'autres théorèmes qui prennent l'eau incluent:

  • Si $x\neq 0$ alors $\frac 1x$ existe MAIS on peut montrer que si $x<0$ ou $x>0$ alors $\frac 1x$ existe
  • Le théorème des valeurs intermédaires MAIS on peut le montrer pour les fonctions dérivables dont la dérivée est minorée par un nombre positif ET on peut aussi en montrer une version "approchée" (voir plus bas)

Analyse constructive


Comment, alors, faire de l'analyse de façon constructive ? Un peu comme en mathématiques "classiques", on va partir des entiers et des rationnels pour construire les réels. On utilise pour construire les entiers l'l'arithmétique de Heyting, qui est une version constructive de celle de Peano.

Cependant, la construction des réels via les suites de Cauchy, présentée ici, n'est pas constructive: la connaissance des éléments de la suite ne nous dit pas grand chose sur le réel qu'on cherche. Encore plus problématique: si on essaie d'appliquer la méthode des suites de Cauchy et des coupures de Dedekind constructivement, on n'obtient pas les mêmes nombres réels. Mieux vaut donc repartir des rationnels.

On va cependant garder l'idée des suites de rationnels. On va définir un réel $x$ comme une suite de rationnels $(x_n)_n$ régulière, c'est à dire, telle que $ |x_n - x_p| < \frac 1n + \frac 1p.$ Deux suites régulières $(x_n)$ et $(y_n)$ définissent le même réel si, pour tout $n$, $ |x_n - y_n| < \frac 2n$. Remarquons qu'on peut alors inclure les rationnels dans les réels en prenant des suites constantes. On peut alors redéfinir des propriétés basiques des réels:

  • Un réel positif ou nul est défini par une suite régulière $(x_n)_n$ telle que, pour tout $n$, $x_n \geq -\frac 1n$. Un réel strictement positif est donné par une suite régulière $(x_n)_n$ et un entier $n$ tels que $x_n > \frac 1n$.
  • Un réel est nul si, pour tout $n$, $|x_n| \leq \frac 1n$.
  • Un réel non nul est donné par une suite régulière $(x_n)_n$ et un entier $n$ tels que $|x_n| > \frac 1n$.
  • Avec la notion de signe, on récupère celle de valeur absolue d'un réel, d'ordre, de maximum et de minimum

Par exemple, le réel $e$ est alors défini par la suite $x_n= \sum_{k=0}^n \frac1{k!}$


Le côté constructif apparaît dans le fait que, pour montrer qu'un réel est non nul, il faut fournir un entier $n$ tel que $|x_n| > \frac 1n$. Si on montre simplement que $\forall n,\ |x_n| \leq \frac 1n$ est contradictoire, alors on a simplement montré $\neg(x=0)$ ce qui, ici, n'est pas pareil que $x=0$. L'idée est qu'en logique classique, on montre qu'il "doit bien y avoir une décimale non nulle quelque part", et le constructiviste répond: "d'accord, laquelle" ? C'est cette information manquante qui est donnée par $n$.

Dans le même ordre d'idée, si on a $x=0 \vee x >0$, on peut en déduire $x\geq 0$, mais la réciproque n'est pas vraie: il se peut qu'on ne puisse pas déterminer, pour un réel $x\geq 0$, s'il est nul ou strictement positif.

On obtient constructivement les résultats suivants: si $x>0$ alors il existe un rationnel positif $a$ tel que $x>a$. En effet, prenons $(x_n)$ une suite régulière qui définit $x$ et $n$ un entier tel que $x_n > \frac 1n$. Prenons $a = \frac 12 \left(x_n - \frac 1n \right)$. Alors $x-a \geq x_n - \frac 1n - a = \frac 12 \left(x_n - \frac 1n \right)>0$, donc $x >a$. En utilisant cela, on montre par exemple que si $x+y>0$ alors $x>0$ ou $y>0$.

On peut définir constructivement des suites de réels convergentes: on dira qu'une suite $(x_N)$ de réels (à ne pas confondre avec les suites régulières de rationnels, qui définissent les réels) converge vers un réel $\ell$ si, pour tout entier $k$, il existe $N_k$ tel que, pour tout $N\geq N_k$, $|x_N - \ell | < \frac 1n$. Comme toujours en maths constructives, il faut, pour montrer qu'une suite converge, exhiber le $N_k$ "qui marche". Ainsi, la suite $(\frac 1N)_N$ converge vers 0, comme on le voit en prenant $N_k = k$.

Avec cette notion, on peut montrer qu'une suite converge si, et seulement si, elle est de Cauchy au sens constructiviste, c'est-à-dire, si pour tout $k$ il existe un entier $N_k$ tel que, pour tous $N, N' \geq N_k$, $|x_N - x_{N'}| < \frac 1k$.

En revanche, le théorème "classique" qui affirme que toute suite croissante majorée converge n'est pas valide en mathématiques constructives. Par exemple, une suite croissante dont tous les termes sont soit 0 soit 1, mais dont on ne sait pas si tous les termes sont nuls, a une limite (soit 0, soit 1), mais comme on ne sait pas décider laquelle, une telle suite ne converge pas au sens constructif.

Le problème porte plus largement sur la notion de borne supérieure d'un ensemble de réels majoré. Cette notion est mal définie en mathématiques constructives: on ne peut la récupérer que pour les ensembles $A$ tels que, pour tous réels $x< y$, on sait affirmer (constructivement !) que soit y majore A, soit x ne majore pas A - auquel cas il faut exhiber un $a\in A$ tel que $x< a$. On peut alors utiliser des couples de réels de plus en plus rapprochés pour construire une suite d'éléments de $A$ qui approche la borne sup aussi près qu'on veut, ce qui permet de la définir constructivement.

La continuité des fonctions pose des problèmes tout aussi épineux. L'un des théorèmes les plus caractéristiques de l'analyse dans $\mathbb R$ est le théorème des valeurs intermédiaires :

Si $f: [a,b] \rightarrow \mathbb R$ est une fonction continue sur $[a,b]$ telle que $f(a) \leq 0 \leq f(b)$ alors il existe $c\in [a,b]$ tel que $f(c)=0$.


Une preuve "traditionnelles" du TVI consiste à procéder par dichotomie: on définit une suite d'intervalles de plus en plus petits, en commençant par $[a,b]= [a_0, b_0]$, et, pour tout entier $n$, $$ c_n= \frac{a_n+b_n}2, \ [a_{n+1}, b_{n+1}] = \begin{cases} [a_n, c_n] \text{ si } f(c_n)>0\\ [c_n, b_n] \text{ sinon.} \end{cases} $$ Ainsi, $a_n$ et $b_n$ se rapprochent de plus en plus, tandis que $f(a_n) \leq 0 \leq f(b_n)$. En continuant ainsi ad infinitum, comme dirait Jules César, on voit qu'à force de rétrécir les intervalles, il finissent par ne plus contenir qu'un seul point, $c$, qui vérifie du coup $f(c)=0$.

Mais la définition de ces intervalles décroissants repose sur le principe du tiers exclus ! (Avez vous repéré le "sinon" ?) Ce n'est pas une preuve constructive valide. Et on n'arrivera pas à "réparer" le problème; pour voir cela, reprenons notre réel $x$ défini plus haut et définissons une brave fonction continue sur $[0,1]$ définie par des bouts de droites, de sorte que $f(0) = -1, f(\frac 13) = f(\frac 23) = x$ et $f(1) = 1$.

La brave fonction $f$.


Alors, à la première itération de la dichotomie, on doit déterminer si $x$ est positif ou non, ce qu'on ne sait notoirement pas faire.

Par contre, on peut constructivement récupérer un "TVI approché": si $f : [a,b] \rightarrow \mathbb R$ est une fonction continue telle que $f(a) < f(b)$, alors, pour tout $y$ entre $f(a)$ et $f(b)$ et pour tout $\varepsilon>0$, il existe $x$ tel que $|f(x) - y| < \varepsilon$. On approche ainsi d'une solution de $f(x)=y$ aussi près qu'on veut. En revanche, la construction d'un réel $x$ qui serait une vraie solution de $f(x)=y$ ne peut être obtenu qu'en renforçant les hypothèses (par exemple, on peut le faire si $f$ est strictement croissante).

Calcul infinitésimal

En analyse constructive, il existe des nombres étranges, introuvables en maths classiques, qui vérifient $d^2=0$ mais pas forcément $d=0$. Pour de tels nombres, la proposition "$d$ est non nul" sera fausse, mais, comme on ne peut pas éliminer les doubles négations, cela ne permet pas de dire que $d$ est nul.

Ces nombres bizarres sont en quelque sorte les infinitésimaux de Leibniz sortis de leur tombe tels une horde de zombies dans un film avec Simon Pegg, et tous comme eux, rendent la notion de limite illicitement simple.

Ainsi, on peut s'en servir pour définir la dérivée $f'$ d'une fonction $f$, en définissant $f'(x)$ comme l'unique réel tel que

$$f(x+d) = f(x)+d\cdot f'(x)$$

pour tout $d$ tel que $d^2=0$. Par exemple, si $f(x)=x^2$,

$$f(x+d) = (x+d)^2= x^2 + 2xd +d^2 = f(x)+ d \cdot (2x)$$

donc $f'(x) = 2x$

Quelle est cette magie noire ?


Elle illustre ce que l'on gagne à faire des maths constructives. On a surtout parlé jusqu'ici de ce que l'on perd, ou de ce qui devient compliqué lorsqu'on se prive du tiers exclus. Mais, de la même façon qu'en nous privant de cette règle de raisonnement, on peut démontrer moins de théorèmes classiquement vrais, on se retrouve aussi moins souvent devant des paradoxes. On peut donc ajouter des axiomes puissants, comme l'existence d'infinitésimaux, sans aboutir à une contradiction, car la contradiction dans le cas classique repose sur l'élimination des doubles négations. On y gagne donc une certaine liberté logique.

Conclusion

Les mathématiques constructives sont exigeantes en termes de prise de tête, mais une preuve constructive est souvent plus instructive qu'une preuve qui ne l'est pas, en ce qu'elle fournit un algorithme pour construire une solution au problème posé; fait d'autant plus intéressant à une époque où nombre de problèmes sont confiés à des ordinateurs susceptibles d'implémenter efficacement ces algorithmes.

L'étude des mathématiques constructives permet aussi une meilleure compréhension des mathématiques qu'on utilise déjà: on cerne mieux quelles propriétés sont fondamentalement non constructives, c'est à dire où la réponse sort vraiment d'un chapeau.

Références:

  • The Five Stages of Accepting Constructive Mathematics, de Andrej Bauer.
  • The weird and wonderful world of constructive mathematics, par Michael Shulman.
  • Introduction to Constructive Logic and Mathematics, par Thomas Streicher.
  •