Raisonnement par l'absurde
Je me demandais si, partant d'une preuve qui utilise un raisonnement par l'absurde, il est toujours possible de la réécrire comme une preuve directe, ou non.
Je prends un exemple simple : l'infinité des nombres premiers. Je ne connais qu'une preuve du résultat, qui commence par "supposons qu'il n'y en ait qu'un nombre fini" et progresse jusqu'à trouver une absurdité. Je n'ai rien contre les raisonnements par l'absurde, hein. Mais je trouverais intéressant de savoir si les règles de logique disent que oui, il est systématiquement possible de faire sans raisonnement par l'absurde, ou au contraire que non, parfois c'est le seul moyen, et il y a une raison à ça (auquel cas, la raison m'intéresserait).
Qu'en est-il ?
Je prends un exemple simple : l'infinité des nombres premiers. Je ne connais qu'une preuve du résultat, qui commence par "supposons qu'il n'y en ait qu'un nombre fini" et progresse jusqu'à trouver une absurdité. Je n'ai rien contre les raisonnements par l'absurde, hein. Mais je trouverais intéressant de savoir si les règles de logique disent que oui, il est systématiquement possible de faire sans raisonnement par l'absurde, ou au contraire que non, parfois c'est le seul moyen, et il y a une raison à ça (auquel cas, la raison m'intéresserait).
Qu'en est-il ?
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
Cela provient de ce que:
1.1/ si $\forall a: [((R(a) \to tout)\to Tout) \to R(a)]$ alors $((C\to tout\to tout))$ quand $C:=\forall xR(x)$
1.2/ si $[(B\to tout)\to tout]\to B$ alors $[((A\to \to tout)\to tout]\to [A\to B]$
quand on n'utilise pas $\exists $ et $ou$ primitifs (sinon, tu peux aussi considérer les énoncés commençant par $\exists$ et "ou" comme des atomes, on peut essentiellement prouver qu'ils marchent comme s'lis avaient ce statut, c'est à dire que leur côté "borne inf" est au second plan (ie un "A ou B", est similaire à l'ajout d'un lettre C et d'une commodité d'avoir ajouté $A\to C$ et $B\to C$), etc).
2/ L'utilisation du RPA dans les maths usuelles est essentiellement un manière de dire, quand tu es face à des phrases $P$ qu'elles sont une hypothèse et une conclusion finale qui est "Tout". Autrement dit, contrairement à ce qu'on croit, ce n'est pas un raisonnement "magique" et un surplus, mais un statut accordé aux arbitres et aux joueurs que l'on loge tous avec la même arrivée finale. Donc la réponse est "presque oui" dans le sens que chaque fois qu'on convient que le but est d'arriver au paradis en faisant des hypothèses, là, oui, dans ce cas, le RPA est redondant.
3/ Mais si tu prends la théorie issue de la topologie grossière mise sur un espace topologique, tu vois bien que l'adhérence de n'importe quel ensemble non vide est l'espace entier, sans pour autant que le seul énoncé de l'espace autre que l'espace entier soit l'ensemble vide (les ouvert sont des énoncés). Dans ce cas, prouver un ouvert $U$, ce n'est pas comme supposer qu'il existe $V$ vérifiant $U=(V\to Tout)$, demander au quidam de prouver $Tout$ à l'aide de cette hypothèse et de considérer "qu'il n'a pu que passer par $U$ pour ce faire".
4/ D'une manière générale, sans le RPA tu ne prouves que des choses "que tu aurais pu prouvées depuis la nuit des temps, même si le contexte avait changé", alors qu'avec le RPA tu peux te servir de l'avenir pour établir un truc. (Attention, ne pas confondre avec la magie, on reste dans le contexte scientifique que tout ce qui est non justifié doit être visiblement écrit comme supposé, là n'est pas la question).
5/ Dans le contexte des nombres premiers, typiquement, ce n'est pas du tout clair sans précision de ce qu'on admet qu'il s'agisse d'un vrai RPA. Le plus petit diviseur de $n!+1$ existe par axiome. Sa NON-divisibilité par non triviaux est un énoncé intuitionniste (tu prouves "si divisible alors tout"). De plus il est constructif en un certain sens puisqu'un nombre seulement fini d'essais sont à faire (seule la complexité a priori augmente, mais elle provient de la taille de $n!$ devant laquelle elle est petite).
Dans ta démonstration de l'infinitude des nombres premiers tu n'as nul besoin du RPA. Il suffit de la formuler ainsi :
Soit p un nombre premier. Il est le $n^{ième}$ de la liste, donc les $n$ premiers nombres premiers s'écrivent : $p_1=2, p_2=3, ..., p_n=p$.
Tu poses $q=p_1.p_2...p_n+1$, et tu montres que $q$ est premier.
Morralité : pour tout nombre premier $p$, il existe un nombre premier $q>p$, ce qui conclut bien à l'infinitude, et pas de RPA là-dedans.
Notons $P$ la propriété $\exists x \in \mathbb{\Q}, x^2=2$.
Tu supposes $P$, blablabla, et tu arrives à une contradiction en exhibant une fraction qui est à la fois irréductible et simplifiable.
Moralité : tu as prouvé ce que Christophe appelle "P implique Tout", donc tu as prouvé $\neg P$, CQFD.
Et toujours pas de RPA là-dedans.
Soit $P$ la propriété ci-dessus.
Tu supposes $\neg P$, donc il y a un polynôme $P$ non constant qui n'admet pas de racine.
Donc $1/P$ est une fonction entière. Un argument de compacité simple te permet de prouver que $1/P$ est bornée, donc par Liouville elle est constante, donc $P$ est constant, contradiction.
Moralité : tu as prouvé que $\neg P$ implique Tout, soit $\neg \neg P$.
En l'absence de RPA tu ne peux pas en déduire $P$.
Je me suis peut-être mal exprimé dans ce dernier post, Christophe rectifiera.
Ok, $p=13$.
Ok, $n=6$, $p_1=2, p_2=3, p_3=5, p_4=7, p_5=11, p_6=13$
Ok, $q=2\times3\times5\times7\times11\times13+1=30031=59\times509$.
Montrons que $q$ est premier...
Un autre truc qui me chagrine, c'est que tu montres la chose suivante : pour toute partie fini $F$ de $\mathcal P$ (ensemble des nombres premiers), on a $F \neq \mathcal P$. Est-ce que ça entraîne avec le minimum syndical d'axiomes de $\mathsf{ZF}$ que $\mathcal P$ est infini au sens où il existe une injection de $\omega$ dans $\mathcal P$ ? Je sais qu'il y a des histoires de "Dedekind-fini" qui ne sont pas équivalents à la définition "être en bijection avec un ordinal $n < \omega$" en l'absence de choix, mais je ne retiens jamais dans quel sens ça marche. :-D
Je rappelle que la question de savoir si un énoncé "se prouve avec le RPA" n'a pas de sens clair.
1/ Tous les énoncés ont une preuve utilisant le RPA,
2/ Tous les énoncés ont au moins une preuve n'utilisant pas le RPA
3/ Quasiment tous les énoncés sont non prouvables (avec ou sans RPA), tant qu'on ne fait pas assez d'hypothèses (qu'on appelle pudiquement des axiomes)
4/ Que, du fait que les gens raisonnent en logique classique, les axiomes ne sont pas très très regardés dans le détail et il suffit de les changer pour faire disparaitre un RPA
5/ Que donc, la question de HT n'est pas assez précise. Mais que la réponse est sérieusement non, sinon le RPA lui-même pourrait se prouver sans RPA, ce qui me donne l'occasion de rappeler que le RPA est l'axiome:
$$\forall A: ([A\to Tout] \to [(A\to Tout)\to Tout]) \to A$$
et non pas l'axiome, contrairement à un préjugé populaire:
$$\forall A: [(A\to Tout)\to Tout] \to A$$
qui lui est "trivial" sans ajout extérieur de richesse logique.
6/ Concernant l'arithmétique, ces questions sont un peu floues aussi, puisque si on considère que les seules primitives sont $\forall ; \to$ (et éventuellement "et" qui ne pose pas de problème), alors l'arithmétique intuitioniste est égale à l'arithmétique classique et donc la preuve qu'il y a une infinité de nombres premiers est de ce fait intuitionniste.
7/ Quand ce genre de phénomène se produit, même en ajoutant $\exists$, et pour des énoncés "bêtes", la seule chose qui change c'st la longueur de la preuve, puisque dès lors que vous disposez d'une borne, le tiers exclus ne donne qu'un seul avantage, c'est de dire "il existe une preuve intuitionniste de moins de tant de caractères" (à vous de la ptrouver). Exemple: une preuve classique aux "échecs10000" que l'un des deux bords a une stratégie infaillible fait 3 lignes, alors qu'une preuve intuitionniste fera 10^je ne pas combien de lignes.
8/ Je signale une preuve partielle de pourquoi si on prouve $(X\to Tout)\to Tout$ en n'utilisant qu'une seule fois $X$, alors on a une preuve "évidente à partir de la précédente" de $X$.
8.1/ Soient les combinateurs $K,D,B$ tels que :
8.1.1/ $\forall x,y,z: Dxyz > x(yz)$
8.1.2/ $\forall x,y,: Bxy> yx$
8.1.3/ $\forall x,y,: Kxy> x$
8.2/ Une preuve qui n'utilise qu'une seule fois $X\to Tout$ (je mets le reste des axiomes dans une conjonction-contextuée avec $X$), se traduit par une expression écrite avec les 3 machins $D,B,K$ qui décrivent une fonction allant de $(X\to Tout)$ au paradis.
8.3/ J'ajoute une lettre $h$ qui signale que l'hypothèse $X\to Tout$ est faite. J'exécute le mot, de sorte que j'ai un mot $m$ qui désigne un élément du paradis.
8.4/ Ce mot ne peut pas commencer par $D$ et être de la forme $Dpq$, puisque $Dpq$ ne peut garantir que des phrases de la forme $U\to V$, ce qui n'est pas le cas de $Tout$.
8.5/ Ce mot ne peut pas commencer par $K$ et être de la forme $Kp$, puisque $Kp$ ne peut garantir que des phrases de la forme $U\to V$, ce qui n'est pas le cas de $Tout$.
8.6/ Ce mot ne peut pas commencer par $B$ et être de la forme $Bp$, puisque $KB$ ne peut garantir que des phrases de la forme $U\to V$, ce qui n'est pas le cas de $Tout$.
8.7/ Il commence donc par $h$ et est de la forme $hn$. Le mot $n$ NE CONTIENT PAS $h$, puisque $h$ n'a été utilisé qu'une fois. Or $n$ désigne un élément de $X$. On a donc une preuve de $X$ aisée à récupérer.
8.8/ A noter que l'exécution termine toujours puisque chaque pas élimine une lettre, donc il va raccourcir jusqu'à ne plus contenir de sous-mots à exécuter. L'exécution se fait suivant les règles décrites en 8.1 et ce genre de démarche est "généralement" qualifié "d'éliminatrice de coupures", mais ici on est dans un cas simplissime.
8.9/ Donc Homo Topi, oui quand tu n'utilises ton hypothèse $nonX$ qu'une seule fois pour arriver à une absurdité, tu es tranquille, ton RPA s'éliminera facilement.
8.10/ Sauf que attention: quasiment aucun matheux faisant un RPA n'aura "instinctivement" la bêtise de faire un RPA de cette manière. Le besoin qu'ils ressentent du RPA vient "bien évidemment" de la multi-utilisation de l'hypothèse ajoutée pour obtenir l'absurde.
8.11/ De la même manière que si tu files une fonction bluffe $f$ vendue comme allant de $A\to Paradis$ dans Paradis et qu'une personne te rétorque qu'avec elle, elle va au paradis, si elle la duplique 51746 fois pour ce faire, tu auras plein de $f(u(f))$ imbriqués (et de manière éventuellement bouclante) et ça ne te servira à rien de récupérer $u(f)$ en disant "ah ah il appartient à $A$, car il aura été construit avec un $f$ dedans qui était ton bluffe.
8.12/ De la même manière (c'est isomorphe) tu peux espérer (sauf infinis avec axChoix) récupérer un élément de l'espace vectoriel $E$ à partir d'une application affine de $L(L(E,\R), \R)$, même si ca canonicité comporte une partie "transcendantale", alors qu'à l'aide, je ne sais moi, d'une simple application continue, ou même polynomiale allant de $(E\to Tout)$ dans $Tout$; tu n'as strictement aucune chance dans bien des cas de trouver quel élément de $E$ lui serait canoniquement rattaché.
Pour la deuxième rubrique je ne sais pas trop, il faut que j'y réfléchisse. Tu me fais peur. J'aurais utilisé $AC_{\omega}$ sans m'en apercevoir ?
En fait c'est plus compliqué ça : j'ai la tête farcie de forcing, et en plus il faut que j'aille faire des courses à Auchan, et je cherche toutes les combines possibles et imaginables pour retarder... parmi lesquelles expliquer (mal) le RPA à Homo Topi.
Au fait tu as encore un dollar à corriger au paragraphe 8.9 de ton dernier post, lol..
1) A est fini s'il est en bijection avec un entier.
2) A est Dedekind-fini si toute injection de A dans A est surjective.
a) Fini implique Dedekind-fini est vrai dans ZF.
b) Dedekind-fini implique fini est vrai dans ZF + $AC_{\omega}$.
Il semble que la question de la réciproque (est-ce que le fait que tout Dedekind-fini est fini entraîne $AC_{\omega}$) semble être un problème ouvert.
Le raisonnement fait ci-dessus montre que, si $p \in P$, alors $\exists q>p, q \in P$.
L'application qui à tout $p \in P$ associe son successeur immédiat est donc une injection de $P$ dans $P$ qui n'est pas surjective, puisque $2$ n'est pas atteint.
Donc $P$ est Dedekind-infini et, par la contraposée de a) il est infini, même dans ZF.
Conclusion : on n'a pas utilisé $AC_{\omega}$.
Il reste 2 questions :
1) La preuve du a) utilise-t-elle RPA ?
2) Ai-je le droit d'utiliser la contraposée dans ce sens-là si je ne suppose pas RPA ?
@Christophe, tu en penses quoi ?
Ainsi si tu demandes "cette démonstration utilise-t-elle un raisonnement par l'absurde ?" tu pourras avoir une réponse différente si tu t'adresses à un mathématicien ou à un logicien. De la même façon si tu demandes "est-ce que la courgette est un fruit ?" à un biologiste ou à un cuisinier tu auras une réponse différente. Ils ne parlent tout simplement pas de la même chose.
Ce quiproquo à déjà fait couler beaucoup d'encre sur ce forum.
@Corto: la différence se situe essentiellement sur le fait que les matheux pratiquent toujours le même abus de langage qui consistent à croire que quand ils prouvent nonP et prouvant P=>Tout, ils ont raisonné par l'absurde. Voilà, je précise ce que tu dis à Homo Topi. Il est rare de voir un autre type de désaccord entre logiciens et peuple.
Quant à ce que moi j'évoque "la duplication" pour que ce soit "un vrai de chez vrai RPA", il se trouve qu'instinctivement, aucun matheux ou presque ne produit des RPA sans duplication ensuite dans l'exploitation de l'hypothèse non P. Ca, c'est un fait sociologique à noter et rigolo.
1/ Celle que tu dis, mais pas si répandue
2/ La suivante: $([A\to tout]\to A) \to A$ (qui est en fait la forme que je donne à un chouya près.
Il est fréquent qu'il redondent avec un "c'est absurde", mais seulement après avoir obtenu $A$ en supposant $nonA$
Bon après, je n'ai pas fait des stats très poussées sur les utilisations et tu as raison de rappeler qu'il n'y a pas de "préjugé" dans les noms. Ce que je voulais pointer est qu'ils préjugent n'avoir que supposé nonA, alors qu'il ont supposé
autant de fois que voulu
Pour moi, le RPA c'est $(non(A) \Longrightarrow FAUX) \Longrightarrow A$. Je ne comprends pas tes autres formulations.
Je vais essayer de préciser davantage ma question : le RPÄ est un axiome d'une théorie logique, le calcul des propositions. Est-ce qu'on pourrait obtenir exactement la même théorie (tous les théorèmes du calcul des propositions) SANS le RPA, et donc c'est un axiome redondant (donc : c'est un théorème déductible des autres axiomes du calcul des propositions, ou bien est-ce qu'on perd effectivement des théorèmes du calcul des propositions en enlevant le RPA des axiomes du calcul des propositions car le RPA est absolument essentiel pour prouver certains théorèmes ?
(Il faut l'enlever lui, et son compagnon de route, le tiers exclu, qui sont équivalents)
En d'autres termes, la logique intuitionniste est strictement plus faible que la logique classique.
Cependant, il faut savoir qu'en logique propositonnelle, tu le récupères juste en récupérant une seule chose: toutes tes formules finissent pas $Tout$.
Concernant le RPA quand tu dis "pour moi c'est", tu redis très exactement ce que j'ai signalé après Corto et foys. La finesse supplémentaire est qu'un vrai RPA est généralement fait avec deux utilisations de non(A). Mais tu peux oublier si ça te gène.
Et enfin rappel: non(A) signifie (A=>Tout) et FAUX=Tout.
Par contre, j'essaie surtout de comprendre pourquoi tu n'utilises pas la même formulation du RPA que moi. Il doit y avoir une subtilité que je ne comprends pas.
Quand je fais un raisonnement par l'absurde, ce que je fais, c'est : je suppose $A$, je fais un raisonnement, j'aboutis à $\neg A$. Donc j'ai prouvé $(A \Longrightarrow (A \wedge \neg A))$, c'est-à-dire $A \Longrightarrow faux$. On est d'accord que $faux = tout$. Bon, justement, si je peux déduire de $A$ qu'un truc qui est censé toujours être faux est vrai, j'ai un problème. Donc je veux que $((A \Longrightarrow faux) \Longrightarrow faux)$ soit vrai.
Je n'aboutis toujours pas à ta formulation...
> Quand je fais un raisonnement par l'absurde, ce que je fais, c'est : je suppose $A$, je fais un
> raisonnement, j'aboutis à $\neg A$. Donc j'ai prouvé $(A \Longrightarrow (A \wedge \neg A))$,
> c'est-à-dire $A \Longrightarrow faux$.
Autrement dit tu as démontré non A. Ben justement, ce n'est pas un vrai raisonnement par l'absurde : un intuitionniste ne trouvera rien à redire à cette démonstration de non A.
Un intuitionniste ralera si tu fais la chose suivante : tu veux démontrer A. Tu supposes non A, et tu en déduis faux ; et là tu dis "Ça y est, j'ai démontré A". L'intuitionniste te dira : "Non, tu as seulement démontré non non A, tu n'as pas démontré A".
2/ La chose à comprendre que vient de te rappeler GBZM, c'est qu'il y a une ENOOOORRRMEEEEE différence entre
2.1/ prouver que A => Tout et en supposant A et en déduisant Tout. Ca n'a rien d'un RPA, c'est une étourderie fréquente parce que les gens OUBLIENT que nonA C'est A=>Tout
2.2/ Prouver (A=>Tout)=>Tout et PRETENDRE qu'ainsi on a prouvé A.
3/ Ceci étant dit, tu peux ne pas lire la suite.
4/ La suite était que, quand j'ai lu ta demande de bon matin, "tu semblais espérer" que quand on a prouvé
(A=>Tout)=>Tout, "on voudrait bien DANS CERTAINS CAS, passer du temps récréatif ou sérieux à vérifier si on ne pourrait pas prouver directement A d'une AUTRE MANIERE.
5/ Et là, je t'ai juste informé d'un cas où c'est TOUJOURS POSSIBLE, qui est quand dans ta preuve de (A=>Tout)=>Tout, c'est à dire quand tu as supposé A=>Tout et finalement déduit A, tu n'as utilisé QU UNE SEULE FOIS l'hypothèse A=>Tout.
N'hésite pas si tu as des questions, mais je vais sortir donc ne t'inquiète pas.
Christophe écrit que le vrai RPA est $(\neg A\implies \neg\neg A) \implies A$ (VRPA). Mais ajouter cet axiome ou l'axiome tel que tu l'as formulé à la logique intuitionniste, c'est kif-kif. Je veux dire, quand on ajoute aux règles intuitionnistes les RPA pour tout A, on démontre les VRPA pour tout A, et idem dans l'autre sens.
Edit. coquille corrigée dans le VRPA
Je pense avoir compris ceci : techniquement, suivant cette logique, $((A \Longrightarrow faux) \Longrightarrow faux)$ c'est $\neg \neg A$. On a besoin d'un axiome pour justifier que c'est la même chose que $A$, d'où le $\neg \neg A \Longrightarrow A$ que Christophe avait écrit $[((A \Longrightarrow faux) \Longrightarrow faux) \Longrightarrow A]$.
Maintenant, Christophe dit qu'écrit tel quel, ce n'est pas encore l'axiome complet du RPA, c'est seulement le "préjugé populaire" du RPA, et il se déduit des règles de la double négation (qui sont admises en logique classique).
Entre Christophe et GBZM, l'un de vous deux à écrit une coquille, parce que dans ce message de Christophe, je lis que le VRPA est $((\neg A \Longrightarrow \neg \neg A) \Longrightarrow A)$, et GBZM a un $\neg A$ à la fin au lieu de $A$. La version de Christophe me parait compréhensible : si, partant de $\neg A$, j'en déduis $\neg \neg A$ (c'est-à-dire $A$), eh bien, $A$ et $\neg A$ seraient vrais en même temps, ce qui est effectivement absurde (non-contradiction), donc j'ai démontré que $\neg A$ implique $faux$, donc j'ai démontré $\neg \neg A$, donc $A$, encore une fois.
Si ce n'est pas comme ça qu'il faut le comprendre, j'aurai besoin de plus de détails...
Je peux préciser. On voit facilement que $(\neg A \implies \neg\neg A) \implies \neg\neg A$ est un théorème intuitionniste. On a donc même que $RPA(A) \implies VRPA(A)$ est un théorème intuitionniste.
$$ (A\to (A\to )$$
à $$ A\to B$$
axiome dont dispose la logique intuitionniste.
Du coup, quand j'ai signalé que "le vrai RPA" était que si
$$nonA\to (nonA\to Paradis)$$
alors on s'autorise à conclure "donc $A$",
il est important de bien préciser que j'étais "dans le domaine expert" (même s'il n'y a pas trop besoin d'être expert, mais bon), où je voulais insister sur la forme ( A+A ) => B qui n'est pas la forme A=>B.
Tout dépend de tes besoins, j'avais malencontreusement cru que tu avais déjà farfouillé un peu la question et demandait vraiment "des renforts" pour éliminer "le plus possible" le RPA, d'où mon excursion dans ces considérations.
Je mets bien un trait vertical pour te détailler des points qui sont maintenant UNIQUEMENT CONSACRES à la notion "non exprerte", à savoir le RPA de "Monsieur tout le monde" qui est $[non(nonA)] \to A$.
Tu as plein de façons équivalentes INTUITIONNISTEMENT de le dire. En voici quelques unes:
1/ A ou (nonA)
2/ ((A=>B)=>B) => ((B=>A)=>A)
3/ A ou (A=>B)
4/ non est injective (ie $\forall X,Y: [(nonX\iff nonY)\to (X\iff Y)]$
5/ Si (A=>B) => A alors A
6/ pour tout A, il existe B tel que $A\iff (nonB)$
Je ne continue pas (pas sûr que j'en ai énormément d'autres en tête qui me viennent d'ailleurs :-D ) . Quelques commentaires:
Le plus "choquant" est (3).
Le plus "cru sans souci" est (4).
L'un des moins connus "du peuple" est (5) (Axiome de Peirce)
Le (2) est "l'axiome de CC" :-D donc pas du tout évoqué en général. En logique classique il dit "si A ou B alors (B ou A)"
Le (1) est célébrissime
Le (6) est méconnu mais très important.
N'hésite pas si questions.
7/ [(nonA)=>(nonA)] => (je l'avais oublié, quelle honte :-D )
8/ ((A et => C) => ((A=>C) ou (B=>C))
9/ [ (nonA) =>B ] => (A ou
10/ [non(A=>B)] => A
Si tu veux un repère très simple: un théorème est intuitionniste quand il te donne un élément canonique d'un ensemble, comme suit (ce que je te dis là est officiel et prouvé):
D1/ (A et := (A×B)
D2/ (A=>B) := (ensemble des applications de A dans
D3/ (A ou := A union B
D4/ $\forall x\in J: R(x):=$ l'intersection des $R(x)$ quand $x$ parcourt $J$
D5/ $\exists x\in J: R(x) := $ la réunion des $R(x)$ quand $x$ parcourt $J$
Si tu ne parviens pas à SANS Y TOUCHER repenser juste ta preuve en ces termes, c'est qu'elle n'est pas intuitionniste.
Par exemple, si tu essaies de trouver un élément dans $[A$ union $(A\to ]$, tu seras le roi du monde, mais ce n'est pas possible (sans l'axiome du choix, car il faut voir les lettres comme dépendant d'un petit indice $i$ jamais écrit).
Ce repère est vraiment simple à appliquer pour un matheux lambda indépendamment de sa spécialité.
Par exemple, $A\to (A\to $ peut être envoyé dans $A\to B$, via $f\mapsto [x\mapsto f(x)(x)]$, mais tu vois la DUPLICATION évoquée ce matin.
Tu peux "te débarraser" d'un RPA n'ayant pas fait usage de duplication en (sans rien changer) REPENSANT à tes arguments comme s'ils étaient des applications affines (ou linéaires).
Et là, tu vois bien qu'avoir construit un élément du bidual, c'est avoir construit un élément de l'espace lui-même, SAUF si tu as dupliqué car alors ta preuve va par exemple te donner une forme BILINEAIRE de $E^*\times E^*$ dans $\R$ (j'identifie $\R$ au paradis, c'est une autre affaire), et là, tu n'as plus strictement aucune prise pour en tirer un élément de $E$. Ce phénomène intervient en magie quantique ( tu ne peux pas aller de $E$ dans $E\otimes E$, texto nommé non clonage quantique).
A partir de la linéaire c'est plus mystérieux car l'élément neutre , ie le $1$ du $(1\to x) = x$ n'est plus forcément plus grand que tout le monde. Par exemple dans $(\R, \leq , - )$, le $1$ c'est le $0$. Les théorèmes sont les nombres négatifs et les "trucs jetables" sont les nombres positifs. Et le $1$ est le plus fort des théorèmes. Et en plus de ça, le "non(1)" c'est $1$ lui-même. Mais la logique linéaire c'est tout de même spécial (au fond elle a très peu d'axiomes pour que ce soit chaque fois "significatif").
On a deux preuves par l'absurde célèbres des énoncés (avec les hypothèses adéquates) suivants:
1/ $a^2=0\to a=0$
2/ $(\forall x>0: a\leq x)\to (a\leq 0)$
Mais peut-être quelqu'un aura-t-il envie d'un truc "un peu plus cossu"?