Analyse constructive

La critique porte sur la façon dont est utilisée la notion d'existence, de disjonction et sur l'utilisation du raisonnement par l'absurde^[1].

L'analyse constructive peut être considérée comme apportant une précision sur les théorèmes classiques et leur démonstrations, en distinguant les énoncés considérés comme constructifs de ceux qui ne le sont pas. Ces derniers, classiquement vrais, demandent en analyse constructive à être prouvés d'une façon plus effective, ou bien à être remplacés par un énoncé constructif. Cette distinction entre énoncés constructifs et énoncés non constructifs ne manque pas d'intérêt par exemple dans la possibilité de mettre en œuvre des procédures numériques visant à appliquer un théorème, même si l'analyse constructive ne se limite pas à cet aspect algorithmique.

Considérons une propriété P dépendant d'un paramètre x. On se pose la question de montrer qu'il existe x tel que P(x) soit vérifié. Il y a essentiellement deux façons de répondre à cette question :

• la première consiste à définir un objet x particulier puis à vérifier que P(x) est vrai. Il s'agit d'une existence effective ;
• la deuxième consiste à raisonner par l'absurde. On suppose que, pour tout x, P(x) n'est pas vérifié, et l'on essaie d'en déduire une contradiction. Si l'on y parvient, on conclura que la non-existence de x est absurde et donc que x existe. Dans ce type de démonstration, on ne donne en général aucun moyen de définir explicitement le x en question. Il s'agit d'une existence formelle.

L'analyse mathématique classique ne fait pas de différence entre ces deux notions d'existence, alors que l'analyse constructive les distingue. La première notion est notée :

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

alors que la deuxième est notée :

${\displaystyle \neg (\forall x\;\neg P(x))}$ 

Les deux ne sont pas considérées identiques en analyse constructive. La première entraîne la seconde, mais la réciproque, vraie en analyse classique sous réserve de faire appel à un raisonnement par l'absurde, n'est pas considérée comme constructive. Pour prendre une image due à Hermann Weyl, dans le premier cas, on sait qu'il existe un trésor, et de plus, on dispose de la carte indiquant sa cache. Dans le second cas, on sait qu'il existe un trésor, mais on n'a pas la carte.

À titre d'exemple, considérons un réel donné x dont on ignore s'il est rationnel ou irrationnel (c'est le cas de la constante d'Euler-Mascheroni) et qu'on veuille prouver que x est rationnel. On peut envisager les deux méthodes de démonstration suivantes :

• supposer x irrationnel et aboutir à une contradiction ;
• introduire judicieusement deux entiers p et q et prouver que x = p / q.

On voit bien que la deuxième méthode donne plus d'information que la première, puisqu'elle prouve non seulement que x est rationnel, mais qu'elle donne également sa forme comme quotient de deux entiers explicites, chose que ne fait pas la première démonstration. Pour l'analyse constructive, les deux méthodes ne sont pas équivalentes : la première démonstration prouve que x est non irrationnel, la deuxième que x est rationnel. Mais pour l'analyse constructive, être rationnel est une propriété plus forte qu'être non irrationnel.

En mathématique classique, si P et Q sont deux propositions, on peut montrer que la disjonction ${\displaystyle P\lor Q}$  est vraie en montrant que la conjonction ${\displaystyle \neg P\land \neg Q}$  conduit à une contradiction. Cette démarche ne permet cependant pas de savoir laquelle des deux propositions est vraie, et elle n'est pas admise en analyse constructive. Prouver ${\displaystyle P\lor Q}$  en analyse constructive, c'est prouver que P est vrai ou bien prouver que Q est vrai.

De même, si P est une propriété quelconque, la proposition ${\displaystyle P\lor \neg P}$  est vraie (principe du tiers exclu) en analyse classique, même si on n'a aucune idée sur le fait de savoir effectivement si P est vraie ou si P est fausse. En analyse constructive, on n'admet pas ce principe. Si A est un ensemble et si P est une propriété dépendant d'un paramètre x de A, le fait d'affirmer que tous les éléments de A vérifient P ou que l'un des éléments de A ne vérifie pas P, s'appelle principe d'omniscience. Il n'est pas reconnu en analyse constructive. La plupart des théorèmes de l'analyse classique sont basés sur ce principe et sont donc considérés comme non constructifs..

Soit ${\displaystyle (a_{n})}$  une suite d'entiers. Le fait d'affirmer que, pour tout n, ${\displaystyle a_{n}}$  est nul ou bien il existe n tel que ${\displaystyle a_{n}}$  est non nul, s'appelle petit principe d'omniscience. Il est également rejeté en analyse constructive. La raison en est la suivante. Posons par exemple, pour n supérieur ou égal à 2, ${\displaystyle a_{n}=0}$  si 2n se décompose en somme de deux nombres premiers, et ${\displaystyle a_{n}=1}$  sinon. On ne dispose aujourd'hui d'aucune méthode permettant de savoir si tous les termes de la suite ${\displaystyle (a_{n})}$  sont nuls ou pas, la réponse à cette question résolvant la conjecture de Goldbach^[2].

Classiquement, il énonce que, si ${\displaystyle \neg P}$  conduit à une contradiction, alors P est vraie. Ce principe est analogue au principe du tiers exclu et est également rejeté en analyse constructive. Le fait que ${\displaystyle \neg P}$  conduise à une contradiction permet de conclure que ${\displaystyle \neg \neg P}$  est vraie, mais la double négation est considérée plus faible que l'affirmation. Ainsi, ${\displaystyle \exists x\;P(x)}$  affirme l'existence effective d'un élément x vérifiant P. Sa négation est ${\displaystyle \forall x\;\neg P(x)}$ . La négation de la négation énonce que ${\displaystyle \neg (\forall x\;\neg P(x))}$  qui, comme nous l'avons vu plus haut, énonce une existence formelle, mais non effective de x.

Ainsi, en analyse constructive, le raisonnement par l'absurde, l'élimination de la double négation, l'utilisation du tiers exclu, la contraposition sont évités. En cela, la démarche de l'analyse constructive se rapproche de celle de la logique intuitionniste. Cependant, cette dernière logique rejette les principes précédents, alors que l'analyse constructive s'autorise à les utiliser, à condition d'être justifiés. Par exemple, le raisonnement par l'absurde conduisant à la preuve d'une existence formelle est admis si le domaine où il s'applique est un ensemble fini. Le tiers exclu est également admis pour comparer deux entiers ou deux rationnels x et y : on a ou bien ${\displaystyle x>y}$  ou bien ${\displaystyle x\leq y}$  car il existe des procédures algorithmiques pour comparer deux entiers ou deux rationnels, mais la même conclusion n'est pas acceptée pour deux réels.

Il peut donc être utile de donner quelques exemples de raisonnements non constructifs, et constructifs.

Les raisonnements suivants, classiquement vrais, sont considérés comme non constructifs, car ils nécessitent l'utilisation du raisonnement par l'absurde ou du principe du tiers exclu. Précisons que la définition de la négation d'une proposition P consiste en le fait que P conduit à une contradiction. Cependant, l'analyse constructive essaie de se passer de la négation, en proposant en général deux définitions correspondant aux deux affirmations qui seraient classiquement négations l'une de l'autre.

• De ${\displaystyle \neg (A\land B)}$ , déduire ${\displaystyle \neg A\lor \neg B}$  : la conjonction de A et B conduit à une contradiction, mais ne permet de savoir laquelle des deux propositions est fausse. La disjonction des deux négations, acceptée classiquement, ne l'est pas en analyse constructive.

• De ${\displaystyle \neg B\rightarrow \neg A}$ , déduire que ${\displaystyle A\rightarrow B}$  : classiquement, l'utilisation de la contraposée est une variante du raisonnement par l'absurde. Elle n'est pas constructivement valide.

• ${\displaystyle A\lor \neg A}$  (tiers exclu) : comme nous l'avons dit, ce théorème classique n'est pas constructivement admis car on ignore si A est effectivement vraie ou si A est fausse.

• ${\displaystyle \neg \neg A\rightarrow A}$  (élimination de la double négation) : nous avons expliqué plus haut que la double négation est considérée comme plus faible que l'affirmation en analyse constructive.

• De ${\displaystyle A\rightarrow B}$ , déduire ${\displaystyle \neg A\lor B}$  : le fait que A implique B n'est pas considéré constructivement suffisant pour déterminer si A est faux ou si B est vrai. Une preuve de l'implication doit être telle qu'elle fournit une preuve de B si on a une preuve de A. Si on n'a pas de preuve de A, il est possible que l'on n'ait pas non plus une preuve de ${\displaystyle \neg A}$ .

• De ${\displaystyle \neg (\forall x\;A(x))}$ , déduire ${\displaystyle \exists x\;\neg A(x)}$  : comme nous l'avons déjà vu, l'analyse constructive distingue les deux notions d'existence intervenant ici. De la deuxième, on peut déduire la première, mais pas l'inverse.

On montre que les raisonnements suivants ne font pas appel au raisonnement par l'absurde ou au tiers exclu. Ils sont donc admis en analyse constructive.

• ${\displaystyle \neg A\land \neg B}$  équivaut classiquement, mais aussi constructivement, à ${\displaystyle \neg (A\lor B)}$ .

• De ${\displaystyle \neg A\lor \neg B}$ , on peut déduire ${\displaystyle \neg (A\land B)}$ , mais pas l'inverse.

• ${\displaystyle \neg (\exists x\;A(x))}$  équivaut classiquement, mais aussi constructivement, à ${\displaystyle \forall x\;\neg A(x)}$ .

• De ${\displaystyle \exists x\;\neg A(x)}$ , on peut déduire ${\displaystyle \neg (\forall x\;A(x))}$ , mais pas l'inverse.

Seules quelques notions élémentaires relatives aux suites et aux fonctions sont présentées ici, afin d'éclairer ce qu'est l'analyse constructive.

L'analyse constructive base ses notions sur les entiers et les rationnels, considérés comme les objets élémentaires, constructifs par nature. La définition d'un réel par une suite de Cauchy de rationnels n'est pas considérée comme constructive. En effet, la connaissance d'aucun élément particulier de la suite ne donne la moindre information sur la valeur du réel. On lui substitue les définitions suivantes :

• Une suite ${\displaystyle (x_{n})}$  de rationnels est régulière si, pour tout n et m strictement positifs, ${\displaystyle |x_{n}-x_{m}|\leq {\dfrac {1}{n}}+{\dfrac {1}{m}}}$ . En analyse constructive, une telle suite définit un réel x.
• Deux réels x et y sont égaux si, pour tout n, ${\displaystyle |x_{n}-y_{n}|\leq {\dfrac {2}{n}}}$ . Il s'agit d'une relation d'équivalence. On peut définir sur ces réels des opérations de somme et produit, de maximum, de minimum, de valeur absolue, ainsi que des inégalités. Plus précisément :
• Un réel x strictement positif est défini par une suite régulière et un entier n tels que ${\displaystyle x_{n}>{\dfrac {1}{n}}}$ .
• Un réel x est positif ou nul si, pour tout n, ${\displaystyle x_{n}\geq -{\dfrac {1}{n}}}$ .
• Un réel x est nul si, pour tout n, ${\displaystyle |x_{n}|\leq {\dfrac {1}{n}}}$ .
• Un réel x différent de 0 est défini par une suite régulière et un entier n tels que ${\displaystyle |x_{n}|>{\dfrac {1}{n}}}$ .

On peut montrer que, pour tout n, ${\displaystyle |x_{n}-x|\leq {\dfrac {1}{n}}}$ , ce qui permet de comprendre a posteriori la formulation des définitions précédentes.

On prendra garde que, pour montrer que x est non nul, il faut définir explicitement n tel que ${\displaystyle |x_{n}|>{\dfrac {1}{n}}}$ . Se borner à montrer que la condition ${\displaystyle \forall n\;|x_{n}|\leq {\dfrac {1}{n}}}$  conduit à une contradiction n'est pas constructivement suffisant. Ainsi ${\displaystyle \neg (x=0)}$  ne permet pas de déduire en analyse constructive que ${\displaystyle x\neq 0}$ , car il manque la donnée n. Par contre, ${\displaystyle x\neq 0}$  entraîne que ${\displaystyle \neg (x=0)}$ . Concrètement, le fait que ${\displaystyle x=0}$  conduise à une contradiction signifie classiquement que x est non nul, et donc qu'il existe par exemple un chiffre non nul dans son développement décimal, mais cela ne permet pas de dire quel est le rang de cette décimale. On voit donc de nouveau apparaître une existence formelle non admise en analyse constructive. À l'inverse, si x est non nul au sens constructif, alors on peut déterminer le rang d'une décimale non nulle. Numériquement, la différence est essentielle, car dans le second cas, on connaît la précision à laquelle il faut mener les calculs pour distinguer x de 0, alors que dans le premier cas, on l'ignore. L'analyse constructive distingue donc une différence forte ${\displaystyle x\neq 0}$  d'une différence faible ${\displaystyle \neg (x=0)}$ .

De même si on sait que ${\displaystyle x=0\lor x>0}$ , alors on peut conclure que ${\displaystyle x\geq 0}$ , puisque la conclusion est entraînée aussi bien par la première proposition de la disjonction que par la deuxième. Mais la réciproque n'est pas valide en analyse constructive. On peut très bien avoir ${\displaystyle x\geq 0}$  sans pouvoir déterminer laquelle des deux propositions ${\displaystyle x=0}$  ou ${\displaystyle x>0}$  est vraie.

Enfin, si ${\displaystyle x>0}$ , alors ${\displaystyle \neg (x\leq 0)}$ , mais la réciproque n'est pas acceptée en analyse constructive.

• Si ${\displaystyle x>0}$ , alors il existe a rationnel positif tel que ${\displaystyle a<x}$ . Cette propriété se montre constructivement de la façon suivante. Le réel x est donné par une suite régulière ${\displaystyle (x_{n})}$ , et il existe (sous-entendu explicitement) un entier n tel que ${\displaystyle x_{n}>{\dfrac {1}{n}}}$ . Prenons pour a le rationnel ${\displaystyle {\dfrac {1}{2}}(x_{n}-{\dfrac {1}{n}})}$ . Comme ${\displaystyle |x-x_{n}|\leq {\dfrac {1}{n}}}$ , on a :

${\displaystyle x-a\geq x_{n}-{\dfrac {1}{n}}-a={\dfrac {1}{2}}(x_{n}-{\dfrac {1}{n}})>0}$ 

• Si ${\displaystyle x+y>0}$ , alors ${\displaystyle x>0}$  ou ${\displaystyle y>0}$ . Une preuve constructive consiste à déterminer d'abord un rationnel a tel que ${\displaystyle a<x+y}$ . On détermine ensuite un rationnel u tel que ${\displaystyle |x-u|<{\dfrac {a}{4}}}$ . Il suffit pour cela de prendre un entier N strictement inférieur à ${\displaystyle {\dfrac {a}{4}}}$  et choisir pour u le terme ${\displaystyle x_{N}}$  de la suite régulière définissant x. On détermine de même un rationnel v tel que ${\displaystyle |y-v|<{\dfrac {a}{4}}}$ . On a alors ${\displaystyle u+v\geq x+y-|x-u|-|y-v|>{\dfrac {a}{2}}}$ . L'un des deux rationnels u et v est donc strictement supérieur à ${\displaystyle {\dfrac {a}{4}}}$ , et étant tous deux explicitement connus, on peut savoir lequel. Si c'est u, alors ${\displaystyle x>0}$ . Si c'est v, alors ${\displaystyle y>0}$ .

• Si x et y sont deux réels donnés, la proposition ${\displaystyle x>y}$  ou ${\displaystyle x\leq y}$  n'est pas acceptée en analyse constructive. Prenons le n-ème chiffre décimal de x égal à 1 si n est un nombre parfait impair et 0 sinon, et y = 0. On ne sait pas montrer constructivement que ${\displaystyle x>y}$  ou ${\displaystyle x\leq y}$ . Par contre, si y et z sont donnés avec ${\displaystyle y<z}$ , un calcul approché avec suffisamment de décimales permettra de déterminer effectivement l'une des deux affirmations ${\displaystyle x>y}$  ou ${\displaystyle x<z}$ . On peut apporter une preuve constructive générale de ce résultat. Il suffit pour cela de remarquer que ${\displaystyle 0<z-y=(z-x)+(x-y)}$  et d'appliquer le résultat précédent pour déduire que ${\displaystyle z-x>0}$  ou ${\displaystyle x-y>0}$ . Ce résultat est fondamental car nombre de démonstrations constructives reposent sur lui.

Constructivement, une suite ${\displaystyle (x_{n})}$  de réels converge vers un réel l si, pour tout entier k, il existe un entier ${\displaystyle N_{k}}$  tel que, pour tout entier n supérieur ou égal à ${\displaystyle N_{k}}$ , on a ${\displaystyle |x_{n}-l|\leq {\dfrac {1}{k}}}$ . La définition de ${\displaystyle N_{k}}$  doit être explicite à partir de k. Par exemple, la suite ${\displaystyle ({\dfrac {1}{n}})}$  converge vers 0. Il suffit de prendre ${\displaystyle N_{k}=k}$ .

La suite est une suite de Cauchy si, pour tout entier k, il existe un entier ${\displaystyle N_{k}}$  tel que, pour tout entier n et m supérieurs ou égaux à ${\displaystyle N_{k}}$ , on a ${\displaystyle |x_{n}-x_{m}|\leq {\dfrac {1}{k}}}$ . On peut montrer en analyse constructive qu'une suite de réels converge si et seulement si elle est de Cauchy, résultat analogue à l'analyse classique, mais avec les définitions constructives.

Cependant, en analyse classique, une suite réelle croissante majorée converge, alors que ce résultat n'est pas accepté en analyse constructive. Considérons une suite croissante d'entiers valant 0 ou 1, mais dont on ignore si tous les termes de la suite est nulle. Classiquement, la limite de cette suite est 0 ou 1, mais on est incapable de dire quelle est explicitement cette limite. Constructivement, la suite ne sera pas considérée comme ayant une limite.

Le paragraphe précédent montre que la notion de borne supérieure pose également problème en analyse constructive. Classiquement, tout ensemble de réels majoré admet une borne supérieure. Cependant, il est en général impossible d'en avoir la moindre valeur approchée. L'existence d'une telle borne est dans ce cas purement formelle et non admise en analyse constructive. Considérons de nouveau une suite ${\displaystyle (x_{n})}$  où, pour tout n, ${\displaystyle x_{n}}$  vaut soit 0 soit 1. Classiquement, la borne supérieure de cette suite est nulle si tous les termes de la suite sont nuls, et vaut 1 si l'un d'entre eux est non nul. La détermination exacte de la borne supérieure fait appel au principe d'omniscience évoqué plus haut. Mais on est cependant en général incapable de déterminer laquelle des deux affirmations est vraie, même si on dispose d'une définition ou d'un algorithme permettant de déterminer ${\displaystyle x_{n}}$  pour chaque n donné. Dans ce cas, l'analyste classique dira qu'il existe une borne supérieure, mais qu'il ne la connaît pas. L'analyste constructiviste dira que cette borne supérieure n'est pas définie et se refusera à considérer tout raisonnement basé sur son existence.

En analyse constructive, on peut montrer qu'une partie A bornée de ${\displaystyle \mathbb {R} }$  admettra effectivement une borne supérieure si et seulement si pour tout couple (x, y) de réels avec ${\displaystyle x<y}$ , alors ou bien y majore A, ou bien x ne le majore pas. Le couple étant donné, on doit donc déterminer explicitement quelle est l'alternative qui est vraie, et, dans le cas où x ne majore pas A, exhiber explicitement un élément a de A tel que ${\displaystyle x<a}$ . L'existence est prouvée en mettant en évidence une suite régulière qui définit cette borne supérieure. Celle-ci est donc connue numériquement par des valeurs approchées à toute précision désirée. C'est le cas de la suite ${\displaystyle (1-{\dfrac {1}{n}})}$ . Ce n'est pas le cas de la suite ${\displaystyle (x_{n})}$  où ${\displaystyle x_{n}=1}$  si n est un nombre parfait impair et = 0 sinon. La situation peut évoluer à l'avenir dans le second cas en fonction de l'accroissement de nos connaissances, mais notre ignorance actuelle montre le caractère non constructif de la notion de borne supérieure en général.

En analyse classique, on montre qu'une fonction continue sur un segment est uniformément continue. Mais la démonstration repose sur des principes non constructifs d'existence formelle, tels que le théorème de Bolzano-Weierstrass. L'analyse constructive ne peut démontrer ce théorème. On définit donc la continuité d'une fonction f sur un intervalle I par le fait qu'elle est uniformément continue sur tout segment J inclus dans I. La notion centrale en analyse constructive est donc l'uniforme continuité, donnée par un module de continuité ${\displaystyle \omega }$ . Pour tout entier k, on doit être capable de donner un réel ${\displaystyle \omega (k)}$  tel que, pour tout x et y de J, on a ${\displaystyle |f(x)-f(y)|<{\dfrac {1}{k}}}$  dès que ${\displaystyle |x-y|<\omega (k)}$ .

On peut montrer en analyse constructive qu'une fonction continue sur un segment admet une borne supérieure et une borne inférieure, mais on ne peut pas en général montrer que ces bornes sont un maximum et un minimum, dans le sens où il faudrait exhiber un x en lequel le maximum ou le minimum est atteint. Considérons par exemple une propriété P sur les entiers pour laquelle on ignore si ${\displaystyle \forall n\;P(n)}$  ou au contraire ${\displaystyle \exists n\;\neg P(n)}$  (dans le sens constructif, on ne dispose d'aucune démonstration de la première affirmation ni de la deuxième). Posons ${\displaystyle a_{n}=0}$  si ${\displaystyle P(n)}$  est vérifié, ${\displaystyle a_{n}=1}$  si ${\displaystyle P(n)}$  est faux et n pair, ${\displaystyle a_{n}=-1}$  si ${\displaystyle P(n)}$  est faux et n impair. Posons enfin ${\displaystyle a=\sum _{k=1}^{\infty }{\dfrac {a_{n}}{3^{n}}}}$ . On est incapable de dire si a est nul, strictement positif ou strictement négatif. Si on considère la fonction f affine sur ${\displaystyle [0,{\dfrac {1}{2}}]}$  et sur ${\displaystyle [{\dfrac {1}{2}},1]}$ , telle que ${\displaystyle f(0)=f(1)=0}$  et ${\displaystyle f(1/2)=a}$ , l'analyste classique dira que f admet un maximum, mais il ne pourra pas dire si ce maximum est atteint en 0 ou en ${\displaystyle {\dfrac {1}{2}}}$ . L'analyste constructiviste se bornera à dire que f admet une borne supérieure égale à max(0,a), une approximation numérique de celle-ci pouvant être atteinte à n'importe quelle précision.

Le théorème des valeurs intermédiaires classique n'est pas reconnu en analyse constructive. Sa démonstration repose en effet sur la notion de borne supérieure dont l'existence générale n'est pas constructive.

Une autre démonstration classique de ce théorème procède par dichotomie, mais elle n'est pas non plus constructive. Reprenons le a donné dans le paragraphe précédent, et définissons f affine sur ${\displaystyle [0,{\dfrac {1}{3}}]}$ , ${\displaystyle [{\dfrac {1}{3}},{\dfrac {2}{3}}]}$  et ${\displaystyle [{\dfrac {2}{3}},1]}$ , avec ${\displaystyle f(0)=-1}$ , ${\displaystyle f(1/3)=f(2/3)=a}$ , ${\displaystyle f(1)=1}$ . Cherchons le réel c tel que ${\displaystyle f(c)=0}$ . La méthode de dichotomie calcule ${\displaystyle f(1/2)=a}$  et doit déterminer si a est nul, strictement positif ou strictement négatif, ce qui est généralement impossible. Dans le cas présent, on est incapable de dire si c est inférieur à 1/3, supérieur à 2/3 ou peut être pris quelconque dans l'intervalle ${\displaystyle [{\dfrac {1}{3}},{\dfrac {2}{3}}]}$ .

L'analyse constructive propose donc un énoncé alternatif au théorème des valeurs intermédiaires. Soit f continue sur le segment ${\displaystyle [0,1]}$  et telle que ${\displaystyle f(0)<f(1)}$ . Alors pour tout ${\displaystyle \varepsilon >0}$ , et tout y de ${\displaystyle [f(0),f(1)]}$ , il existe x tel que ${\displaystyle |f(x)-y|<\varepsilon }$ .

L'existence effective d'un x tel que ${\displaystyle f(x)=y}$  peut être obtenue en renforçant les hypothèses, par exemple en précisant que f est strictement croissante. La démonstration se fait alors non pas par dichotomie, mais par trichotomie. On construit une suite de segments emboîtés ${\displaystyle [a_{n},b_{n}]}$ . Comme ${\displaystyle f(a_{n}+{\dfrac {b_{n}-a_{n}}{3}})<f(a_{n}+2{\dfrac {b_{n}-a_{n}}{3}})}$ , il est constructivement possible de décider si ${\displaystyle y>f(a_{n}+{\dfrac {b_{n}-a_{n}}{3}})}$  ou si ${\displaystyle y<f(a_{n}+2{\dfrac {b_{n}-a_{n}}{3}})}$ , et de définir explicitement ${\displaystyle [a_{n+1},b_{n+1}]}$  comme égal à ${\displaystyle [a_{n},a_{n}+2{\dfrac {b_{n}-a_{n}}{3}}]}$  ou à ${\displaystyle [a_{n}+{\dfrac {b_{n}-a_{n}}{3}},b_{n}]}$ . Le réel x est alors la limite des suites ${\displaystyle (a_{n})}$  et ${\displaystyle (b_{n})}$ .

Le principe d'omniscience consiste à énoncer que, si A est un ensemble et P est une propriété dépendant d'un paramètre x élément de A, alors tous les éléments de A vérifient P ou bien l'un des éléments de A ne vérifie pas P. C'est une propriété classique résultant du principe du tiers exclu, mais son utilisation signale généralement un énoncé ou une démonstration non constructive. Son utilisation n'est donc pas admise en analyse constructive.

Le plus couramment, une proposition non constructive utilise le petit principe d'omniscience, qui énonce que, si ${\displaystyle (a_{n})}$  est une suite d'entiers, alors pour tout n, ${\displaystyle a_{n}}$  est nul ou bien il existe n tel que ${\displaystyle a_{n}}$  est non nul. Il est rejeté en analyse constructive car il n'existe aucun algorithme permettant de décider laquelle des deux propriétés est vérifiée. Un programme tel que :

n := 1

tant que a_n = 0 faire n := n + 1 fin tant que

finira par trouver l'indice n tel que ${\displaystyle a_{n}\neq 0}$  si un tel indice existe, mais bouclera sans fin s'il n'existe pas. Ce petit principe est équivalent au fait d'énoncer que, pour tout réel x, ou bien x est nul, ou bien x est non nul. En analyse constructive, on connaît des réels x pour lesquels on ne possède aucune preuve ni qu'ils sont nuls, ni qu'ils sont non nuls, de sorte que la disjonction n'est pas constructivement prouvable.

Du petit principe d'omniscience, on peut déduire le principe suivant, dit principe de Markov : pour tout réel x, ${\displaystyle \neg (x=0)\rightarrow x\neq 0}$ . Cela revient également à énoncer que, pour toute suite ${\displaystyle (a_{n})}$  d'entiers, ${\displaystyle \neg (\forall n\;a_{n}=0)\rightarrow \exists n\;a_{n}\neq 0}$ . Mais on ne peut remonter au petit principe d'omniscience à partir du principe de Markov qu'en utilisant un raisonnement par l'absurde. Il en résulte que, en analyse constructive, le principe de Markov est considéré comme plus faible et moins contraignant que le petit principe d'omniscience. De plus, le principe de Markov dispose d'un statut particulier. On n'en connaît aucune preuve constructive ce qui tendrait à le faire rejeter, mais on ne connaît pas davantage de contre-exemple en analyse constructive. En effet, dans la plupart des systèmes logiques y compris constructifs, une preuve de ${\displaystyle \neg (\forall n\;a_{n}=0)}$  consiste à prouver ${\displaystyle \exists n\;a_{n}\neq 0}$ . Son statut en tant qu'axiome constructif est donc discuté.

Le principe de Markov intervient également dans la question suivante. Une fonction f est dite faiblement injective si ${\displaystyle \forall x\forall y\;(f(x)=f(y)\rightarrow x=y)}$ . Elle est dite fortement injective si ${\displaystyle \forall x\forall y\;(x\neq y\rightarrow f(x)\neq f(y))}$ . En analyse constructive, une fonction fortement injective est faiblement injective, mais la réciproque nécessite l'utilisation du principe de Markov.

• Constructivisme (mathématiques)
• Logique classique
• Logique intuitionniste
• Logique minimale

Les principales avancées en analyse constructive ont été menées par Erret Bishop :

• (en) Erret Bishop, Foundations of Constructive Mathematics, McGraw Hill (1967)
• (en) Erret Bishop, Douglas Bridges, Constructive Analysis, Springer-Verlag (1985)
• Pierre Ageron, Logique, ensemble, catégorie, le point de vue constructif, Ellipses (2000)
• Penser les mathématiques, Séminaires de philosophie et mathématiques de l’Ecole normale supérieure (J. Dieudonné, M. Loi, René Thom), point sciences, Éditions du seuil (1982)
• (en) Hermann Weyl, The Continuum: A Critical Examination of the Foundations of Analysis, Thomas Jefferson University Press (1987)

• (en) Constructive mathematics sur le site ncatlab.org

•   Portail de l'analyse
•   Portail de la logique