Intuitionnisme.
Bonjour à tous, d'après Wikipédia, pour Brouwer les objets mathématiques doivent être accessibles à l'intuition. Or qu'y a-t-il de plus intuitif que le tiers exclu. Alors, pourquoi Brouwer le rejette-t-il?
Merci pour vos éclairages.
Cordialement.
Jean-Louis.
Merci pour vos éclairages.
Cordialement.
Jean-Louis.
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
Le problème c'est que le tiers exclu est équivalent au raisonnement par l'absurde, qui, lui, permet de démontrer l'existence d'objets sans être capables de les construire.
Typiquement : d'Alembert-Gauss : soit $P$ un polynôme non constant à coefficients dans $\C$. Si $P$ n'a pas de racine, alors blablabla, et on arrive à une contradiction sans être foutu de fabriquer une racine de $P$.
Le plus drôle dans l'histoire c'est que Brouwer lui-même a utilisé le raisonnement par l'absurde dans certains de ses travaux, Christophe a sûrement un exemple sous la main...
Par exemple, si je te disais que (en acceptant le tiers exclu) j'ai la capacité d'écrire un algorithme en quelques minutes, sur mon ordi à moi dans ma chambre, qui retourne "oui" si l'hypothèse de Riemann est vraie, "non" sinon, tu me croirais ?
Bah pourtant c'est le cas si tu m'autorises le tiers exclu, et je pourrais te le prouver.
Jean-Louis.
Un sorcier capable de voyager dans le temps procèderait comme suit:
Il annonce au monde qu'il a un tel programme (print "non"). Puis si quelqu'un un jour proteste en lui montrant une preuve de RH, il retourne au moment de l'annonce et remplace son programme par print "oui".
(les travaux sur la réalisabilité classique on montré qu'il était possible de rajouter le tiers exclu à la correpondance de Curry-Howard avec des gestions d'exception et des sauvegardes).
@Maxtimax tu pourrais m'expliquer comment tu utilises le tiers exclu ici stp car je ne vois pas.
Or, d'après Gödel, dans toute théorie "suffisante", il existe un énoncé $B$ tel qu'il n'existe pas de certificat qui prouve $B$ ni de certificat qui prouve $\non (B)$. Donc pas de tiers exclus !
Mais Gödel ne dit rien sur l'énoncé $\non (\non $.
Donc peut-être qu'il existe un énoncé $C$ tel qu'il n'existe pas de certificat qui prouve $C$ ni de certificat qui prouve $\non (C)$ mais un certificat qui prouve $\non (\non C)$.
Donc pas de raisonnement par l'absurde !
En espérant ne pas être banni du forum ! :-D
Par contre je pense qu'ils méritent une remarque musclée du genre : "Tu es complètement à côté de la plaque et tu écris n'importe quoi !"
A ma connaissance les travaux de Gödel n'ont RIEN A VOIR avec l'intuitionnisme !!!
@Maxtimax : j'attends avec impatience ta preuve du truc avec l'ordi sur ton pieu...
Bon, je sors. :-D
(i) en gros un énoncé est assimilé au nom de l'ensemble (ou du type) de ses preuves
(ii)Une preuve de $A\wedge B$ est un couple $(p,q)$ où $p$ est une preuve de $A$ et $q$ une preuve de $B$ (donc d'après (i): $A\wedge B = A \times B$)
(iii)Une preuve de $A\Rightarrow B$ est une fonction-comprendre ici un programme dans un langage fonctionnel- transformant infailliblement toute preuve de $A$ en une preuve de $B$ (autrement dit, via (i): $A\Rightarrow B = B^A$)
(iv)Une preuve de $A\vee B$ est un couple $(\varepsilon,r)$ où $\varepsilon=0$ et $r$ est une preuve de $A$, ou bien $\varepsilon=1$ et $r$ est une preuve de $B$ (en gros: $A\vee B = A \coprod B$)
(v)$\perp$ est un énoncé qui dit intuitivement "tout est vrai" ce qui se traduit formellement par l'existence pour tout énoncé $A$,d'une preuve $abs_A :\perp \Rightarrow A$
(vi) pour tout énoncé $A$, $\neg A$ abrège $A \Rightarrow \perp$
(vii) $\forall x\in E, A(x) = \prod_{u \in E} A(u)$ (généralise (ii))
(viii) $\exists x\in E, A(x) = \coprod_{v \in E} A(v)$ (généralise (iv))
Par exemple:
-si $A,B,C$ sont des énoncés, la curryfication (application qui à $f:A\Rightarrow (B\Rightarrow C)$ fait correspondre l'application qui à $(x,y) \in A \times B $ fait correspondre $f(x)(y)$) est une preuve de $(A\Rightarrow (B\Rightarrow C)) \Rightarrow ((A\times \Rightarrow C)$, son opération inverse est la preuve de la réciproque.
-la composition des applications, i.e. l'application $f\mapsto (g \mapsto g \circ f)$ ,est une preuve du syllogisme $(A \Rightarrow \Rightarrow ((B \Rightarrow C) \Rightarrow (A \Rightarrow C))$.
-en posant $C:=\perp$ dans l'exemple ci-dessus on retrouve compte tenu de (vi) une preuve de la contraposition $(A \Rightarrow \Rightarrow ((\neg \Rightarrow (\neg A))$.
***********
En revanche étant donné un énoncé $A$ , il n'existe en général, dans le système décrit ci-dessus, aucune preuve de $A\vee \neg A$, en fait aucune preuve de $A \vee (A \Rightarrow $ pour un autre $B$ quelconque (alors qu'il s'agit d'une tautologie du calcul propositionnel).
C'est à la suite de travaux datant des années 90 (Tim Griffin) que la correspondance de Curry Howard a pu être modifiée à l'aide de mécanismes de gestion d'exceptions pour inclure le tiers exclu. Une possibilité est la suivante:
On a un programme $p$ de type $A \vee (A\Rightarrow $ qui fait lorsqu'on l'appelle une sauvegarde $e$ de l'état du système puis renvoie un objet $k:A\Rightarrow B$ dont le comportement est le suivant: si on l'appelle sur un objet $x$ de type $A$, il sauvegarde $x$, puis arrête le système et rétablit la sauvegarde $e$ et retourne $x$ de type $A$.
C'est pour ça que quand vous pouvez voyager dans le temps(!!!), même si vous êtes nul en maths vous pouvez retourner un programme qui dit oui si RH est prouvable et non si elle n'est pas prouvable: le programme d'une ligne "afficher <<non>>" convient: si RH n'est jamais prouvée vous avez raison et si elle l'est vous revenez au moment où vous promettez d'avoir un tel programme et vous livrez "afficher <<oui>>" à la place. On gagne à tous les coups.
Merci d'avance of course.
Je trouve le tiers-exclus très contre-intuitif. Pour gagner de la place dans la suite, je note P l'hypothèse du continu. Avec le tiers-exclus, je ne peux pas prouver P, je ne peux pas prouver non(P), mais je peux prouver P ou non(P).
C'est une règle conventionnelle comme une autre qui ne me choque nullement, mais qui ne correspond pas à mon intuition première (même s'il est possible de modifier ses intuitions avec un peu de motivation, mais c'est là une encore autre affaire).
On abrège par P la phrase "il existe un programme tel que si RH alors il affiche oui et si (non(RH)) alors il affiche non".
-Supposons RH. Alors le programme qui affiche systématiquement oui, est tel que:si RH il affiche oui et si (non(RH)) il affiche non. Donc P.
-Supposons non(RH). Alors le programme qui affiche systématiquement non, est tel que:si RH il affiche oui et si (non(RH)) il affiche non. Donc P.
Finalement (RH ou non(RH)) entraîne P (en vertu du théorème (F->U)->((G->U)->((F \/ G )-> U)) valide pour tous énoncés F,G,U même en logique intuitionniste! )
Si l'hypothèse de Riemann est prouvable [avec une modification de Foys, merci !], alors je suis capable d'écrire ce programme : j'écris l'équivalent de "print ' oui' " dans mon langage préféré
Si l'hypothèse de Riemann n'est pas prouvable, alors je suis capable d'écrire ce programme : j'écris l'équivalent de "print 'non' " dans mon langage préféré.
Que l'hypothèse de Riemann soit prouvable ou non, je suis capable d'écrire un tel programme. Donc [c'est dans ce "donc" que ce cache le tiers exclu] je suis capable d'écrire un tel programme (le même argument marche avec l'existence de dieu en admettant que la question ait un sens, si on veut la présenter à un public plus large)
On voit que c'est un peu ce qui a été expliqué au dessus : le problème dans ce que je raconte est que je teste $A\lor \neg A$ sur un $A$ dont il m'est impossible (pour le moment :-D) de déterminer la valeur de vérité, j'obtiens donc quelque chose sans "témoin", quelque chose que je ne peux pas tester: ici je suis capable d'écrire le programme, mais je ne sais pas lequel c'est !
Si on n'est pas convaincu on pourra se rappeler de la règle suivante qui gère "ou" : Si $A\vdash C, B\vdash C$ ($P\vdash Q$ se lit approximativement "à partir de $P$ on prouve $Q$", ou quelque chose dans ce goût), alors $A\lor B \vdash C$; ainsi que : si $A\vdash B$ et $\vdash A$ alors $\vdash B$. En particulier, ici j'applique tout ça : "HR est prouvable $\vdash$ je peux écrire le programme", "HR n'est pas prouvable $\vdash$ je peux écrire le programme" et "$\vdash$ HR est prouvable ou ne l'est pas".
En logique intuitionniste, ce genre de phénomène n'apparaît pas, une preuve apporte avec elle un "témoin", autrement dit un "contenu computationnel" (Foys dit qu'on peut étendre la correspondance de Curry-Howard à la logique classique, donc étendre cet aspect "contenu computationnel", et j'ai aussi déjà vu ça, mais c'est avec différentes modifications du sens de cette expression) : en particulier quand une preuve affirme l'existence de quelque chose, on peut extraire de la preuve un témoin de cette existence. C'est un sens en lequel elle est "plus intuitive" que la classique (où on peut affirmer "truc existe" sans exhiber truc)
(PS: si ça amuse Martial j'étais effectivement dans mon lit pour écrire ça :-D)
Maintenant j'ai compris X:-(
Du coup l'affirmation "il existe un programme tel que si RH alors il affiche oui et si (non(RH)) alors il affiche non" qui m'avait l'air surprenante avant ne l'est plus maintenant :-(
À l'époque j'avais acheté ce bouquin et j'ai relu rapidement les premières pages qui parlent des séquents, et effectivement à la page 40 il y a le tiers exclu que vous avez appliqué :
"HR est prouvable" $\vdash$ "je peux écrire le programme", "HR n'est pas prouvable" $\vdash$ "je peux écrire le programme" donc, $$\vdash \text{"je peux écrire le programme".}$$
Yes, Je peux écrire ce programme !!!!
Mon point de vue à ce sujet est qu'il n'y a pas de sens à se demander "est-ce que le tiers exclu est vrai ?", mais qu'il faut plutôt voir les choses sous l'angle de la pertinence : est-il pertinent d'utiliser le tiers exclu dans telle discussion ? Même chose pour d'autres règles de logique.
J'ai essayé de comprendre $(A\Rightarrow (B\Rightarrow C)) \Rightarrow ((A\times \Rightarrow C)$.
Il s'agit de montrer qu'il existe une application $\varphi$ de $(A\Rightarrow (B\Rightarrow C))=(C^B)^A$ dans $((A\times \Rightarrow C)=C^{A\times B}$.
Soit $f\in (C^B)^A$. $f$ est une application $A\to C^B$ donc pour tout $x\in A$, $f(x)\in C^B$, i.e. $f(x)$ est une application $B\to C$.
Donc, pour tout $y\in B$, $f(x)(y)\in C$.
Ainsi, $\varphi:f\mapsto ((x,y)\mapsto f(x)(y))$ convient.
De même, l'application qui à $x\in A$ associe l'application $f\in\perp^A\;\mapsto f(x)$ est une preuve de $A\Rightarrow \neg\neg A$.
Et j'imagine qu'on n'a pas de preuve de $\neg\neg A\Rightarrow A$. :-)
Je poste rarement en Logique et quand cela m'arrive, en général je fais un hors-sujet. Cela pourrait être encore le cas ici. De plus, ce que je raconte est ultra-connu. Je voudrais savoir ce que tu penses du résultat (?) mathématique suivant :
Il existe deux irrationnels strictement positifs $a,b$ tels que $a^b$ soit rationnel.
En voici la preuve (sic) :
Cas I. Si $\sqrt 3^{\sqrt 2}$ est irrationnel, prendre $a = \sqrt 3^{\sqrt 2}$ et $b = \sqrt 2$ (on sait prouver que $\sqrt 2$ est irrationnel).
Cas II. Si $\sqrt 3^{\sqrt 2}$ est rationnel, prendre $a = \sqrt 3$ et $b = \sqrt 2$ (bis : on sait prouver que $\sqrt 2, \sqrt 3$ sont irrationnels).
Qu'en dis tu de ce résultat ? Est ce que tu le mets par exemple sur le même plan que le résultat suivant : tout premier $p \equiv 1 \bmod 4$ est la somme de deux carrés. Ou le théorème de Pappus dans le plan projectif ou ...etc.. (on pourrait citer des milliers de résultats que je qualifie de tangibles).
Je termine par une remarque (achevant probablement l'aspect hors-sujet). Cas I, cas II, c'est ce que l'on appelle une alternative. Cela arrive beaucoup en programmation. Je confesse : il m'arrive de programmer un peu et qu'en fasse face d'une telle alternative, je me sentirais très mal.
Jean-Louis.
Dans ton exemple tu distingues surtout ce qu'on appelle la complexité des énoncés c'est à dire leur decidabilite in fine. La logique intuitionniste n'y est pour rien.
D'un PC je détaillerai.
La logique intuitionniste est juste là classique avec un axiome en moins.
1. J'ai ``peur'' que dans tes explications d'un PC, tu restes (sans le vouloir) dans ton monde, avec peut-être le bilan que je vais rien comprendre. Mais attendons.
2. Quel est le statut de l'énoncé ``il existe 2 irrationnels strictement positifs $a,b$ tels que $a^b$ soit rationnel'' en logique intuitionniste ? D'ailleurs, est ce que cette phrase que je viens d'écrire a un sens ?
3. Mais pourquoi que les autres (plus disponibles ?) ne m'ont rien dit sur le fait que je faisais un hors-sujet (j'avais d'ailleurs prévenu) ? Ils auraient pu par exemple prendre le temps d'avertir un modérateur pour dire que C.Q. trolle encore sur un fil de logique, non ?
De là à dire qu'elles sont intuitionnistes, je ne sais pas (il faut voir la construction de $\ln$ dans les différents modèles de $\mathbb R$ qui ne sont plus équivalents).
Même si on se restreint à $a$ et $b$ algébriques de degré $\geq 2$, il va être difficile de certifier que $a^b$ est rationnel.
Ok pour les entrées, bof pour la sortie.
pour tous énoncés $A,B,X$, l'énoncé suivant est un théorème de la logique intuitionniste: $$[(A \vee \wedge (A\Rightarrow X) \wedge (B\Rightarrow X)] \Rightarrow X \tag{$\dagger$}$$
Et on exploite ce fait comme suit:
-Si on a une preuve de $A \vee B$ ($A$ ou $B$) et qu'on souhaite prouver $X$, on va prouver que $A$ entraîne $X$ et ausi que $B$ entraîne $X$. Si on pense à la programmation, dans la correspondance de Curry Howard historique (qui est intuitionniste; cf http://www.les-mathematiques.net/phorum/read.php?16,1866650,1866802#msg-1866802), l'ensemble des preuves de $A \vee B$ est (carrément par définition même selon certains points de vue) est le coproduit de l'ensemble des preuves de $A$ et de l'ensemble des preuves de $B$ et par suite, comme une preuve de $Y\Rightarrow Z$ est essentiellement une fonction de l'ensemble des preuves de $Y$ dans l'ensemble des preuves de $Z$, on voit que $(\dagger)$ et la phrase qui suit ne sont rien d'autre que la correspondance bijective entre les fonctions dont le domaine est un coproduit et les couples de fonctions définies sur chacun des membres dudit coproduit.
Bref, l'énoncé $$\left [(\sqrt 3 ^{\sqrt 2} \in \Q) \vee \neg (\sqrt 3 ^{\sqrt 2} \in \Q) \right ] \Rightarrow \exists a,b \in \R\backslash \Q,a^b \in \Q $$ est un théorème intuitionniste de la théorie des ensembles.
Le problème est que (sauf circonstance spéciale inconnue de moi) $(\sqrt 3 ^{\sqrt 2} \in \Q) \vee \neg (\sqrt 3 ^{\sqrt 2} \in \Q)$ n'en est pas un a priori.
Soit $E$ un ensemble dit "de phrases", ordonné** de manière complète (toute partie de $E$ a une borne inf).
** lire $a\leq b$ comme abrégeant $<<b$ est un cas particulier de $a>>$
Vous avez plusieurs niveaux de certitudes, que je décris de manière décroissante ($\to$ abrège l'implication et c'est une application de $E^2$ dans $E$).
Premier niveau:
N1.1/ il y a un élément qui s'appelle $1$ tel que $\forall x: (1\to x) = x$
N1.2/ $\forall x,y,z: ( x\to (y\to z) )=( y\to (x\to z) )$
N1.3/ pour tous $x,y: [(x\leq y)$ si et seulement si $1\leq (x\to y)]$
Ce premier niveau est assez "linguistique" dans les certitudes scientifiques et ne force pas du tout les éléments de $E$ à pouvoir être considéré comme l'ensemble des valeurs de phrases. Certes on n'est plus à un niveau "libre" (au sens de groupe libre), puisqu'on a par exemple l'égalité $((x\to y)\to (x\to y)) = (x\to ((x\to y)\to y))$, certes quasi-inoffensives, mais déjà telle qu'elle peut, pour les mal comprenants, provoquer des polémiques "nom/valeur", comme les provoque le fait que $7+3$ est un produit, puisque c'est $1\times 10$.
Par contre les axiomes de ce niveau est INCONTESTE par qui que ce soit, même les plus "étrange" psychopathes.
Deuxième niveau: là, on commence à trouver des choses que CERTAINS ETRES HUMAINS ont du mal à faire remonter au conscient (ils en sont convaincus, mais mettent du temps à prendre conscience qu'ils en sont convaincus).
N2.1/ $\forall x\in E: x\leq 1$.
Ca a comme conséquence que $\forall x,y: x\leq (y\to x)$, connu sous la description plus populaire que des hypothèses inutiles ne changent rien à la capacité de prouver ou croire aux conclusions que certaines autres entrainent.
Exemple: si $[3 = a+b$ alors $a\times 1 = a]$ n'est pas considéré comme moins sûr que $a\times 1=a$
N2.2/ Ces deux socles sont, même s'il faut un peu plus de temps, généralement considérés comme sûr par tout le monde.
Si on note $\perp$ la borne inférieure des éléments de $E$, mais le nom le plus adapté évidemment serait de l'appeler "tout", c'est à ce niveau que vit le théorème disant $non(A)$ équivaut à "A=> toute phrase"
Niveau3: Curieusement, à ce niveau 3 vit l'axiome LE PLUS PUISSANT ET DE LOIN de tous les axiomes admis par la science. Et pourtant (c'est ça la curiosité), le "peuple" l'admet PLUS FACILEMENT que le niveau 2
En termes populaires, c'est l'axiome: "(A et A) = A" que personne ne conteste et surtout que tout le monde croit à tort inoffensif. Alors qu'en fait sans lui, les maths seraient très différentes.
Techniquement, c'est $\forall x,y: [(x\to (x\to y))\leq (x\to y)]$
Niveau4: $\leq$ est isomorphe à $\geq$. (En pratique, ça revient à considérer que toute phrase vaut la négation d'une phrase, ie que l'ensemble des valeurs possibles pour une phrase n'est en particulier pas "bien fondé").
Arrivé au niveau3, en fait on a toutes les maths, et le préjugé populaire qui veut qu'il y aurait une différence de constructivité entre logique classique et intuitionniste est FAUX.
En fait, en pratique la logique intuitionniste EST PLUS COMPLEXE (propositionnellement elle est trivialement PSPACE complète, quand la classique "n'est que" NP-complète) et moins "constructive" (in somme sense) que la classique.
Le niveau4 est juste un niveau auquel "on gagne du temps" en SYMETRISANT le message qu'on espère envoyé par les extrêmes $\{\perp; 1\}$, respectivement plus petit et plus grand élément de $E$.
C'est là que s'insère la logique intuitionniste. Elle dit juste que les HYPOTHESES sont duplicables mais pas les conclusions. C'est "bêtement" un accident historique dû à notre "désir de commencer quelque part" qui n'a en fait aucun fondement.
Pour le dire autrement, la logique intuitionniste est accidentellement générée par le fait qu'il existe tout un tas de $x\in E$ tels que $\forall y\in E: y\neq x$.
En effet, il suffit que $\forall x\in E\exists y\in E: ((y\to \perp)\to \perp) = x$ pour qu'elle n'existe plus (enfin précisément ne soit plus représentée par $E$).
Elle est à comparer au refus des nombres irrationnels en 1000 avant JC et toute sorte d'addictions similaires.
Attention, je n'en fais pas une critique négative et elle est bien strictement incluse dans la classique en termes de théorèmes, donc bien évidemment qu'une preuve intuitionniste EST UN CAS PARTICULIER de preuve classique. Elle n'est pas "étrangère".
Prenons maintenant un espace topologique connexe et deux ouverts non vides disjoints $U,V$. Et bien personne ne s'évanouit devant la remarque que $U\cup V$ NE PEUT PAS valoir l'espace entier.
Pour TRES EXACTEMENT LES MËMES RAISONS SEMANTIQUES, certaines phrases $p$ sont "inrecouvrables" et vérifient, si on s'en tient à l'intuitionniste $\forall x:\ [$ si $p\leq (x\vee \neg x)$ alors $((p\leq x)$ ou $(p\leq \neg x))]$.
Cet "accident" a provoqué de gros remous et donné le préjugé (complètement faux en général) qu'il s'agit d'une forme de constructivité. La réalité est beaucoup moins sexy, comme le montre le fait que $(x\vee \neg x) \leq (x\vee \neg x) $ sans pour autant que $[(x\vee \neg x) \leq x]$ ou $[(x\vee \neg x) \leq (\neg x) ]$
Pour conclure, elle est passionnante et en termes de "temps de vie à être étudiée intensément", elle dépasse ses jeunes soeurs (logique linéaire (que le niveau1) et logique affine (niveau 1+2)).
Pour revenir à ce qu'a dit Claude, et même si je sais que l'exemple qu'il prend est présenté (c'est quasiment toujours le même) 100000 fois dans l'enseignement supérieur pour illustrer ce thème, il faut bien rappeler que c'est une question de FORME DE PREUVES et non de "contenu sémantique sensé".
Le fait que [($a$ est rationnel) ou ($a$ n'est pas rationnel)] est un axiome classique, mais pas intuitionniste est FORMELLEMENT administratif. C'est juste "vrai" (il suffit de consulter les listes respectives d'axiomes de ces logiques (ou de règles démonstratives de ces logiques) pour le "constater administrativement")
Mais les exemples ne sont pas parlants car jouent sur un oubli totalement accidentel:
est une duale parfaitement respectable des exemples courant de enseignants non logiciens en L2 et pourtant c'est un théorème tout ce qu'il y a de plus parfaitement intuitionniste
* Vous pouvez aussi penser à $non(a \in \Q$ et $a\notin \Q)$
Abréviations:
Aux niveaux 1 et 2, il y a 2 et et deux ou
Ils collapsent à partir du niveau 3
A (et1) B est l'abréviation de $<<$ la borne inférieure des éléments de $E$ suivants $(A\to (B\to x))\to x$ quand $x$ parcourt $E>>$
A (et2) B est juste $inf(\{A;B\})$
A (ou1) B est l'abréviation de $<<$ la borne inférieure des éléments de $E$ suivants $((A\to x)\to ((B\to x)\to x))$ quand $x$ parcourt $E>>$
A (ou2) B est juste $sup(\{A;B\})$
Le préjugé de constructivité de la logique intuitionniste avait conduit à écarter l'axiome non intuitionniste (ie les formes équivalentes : TE; nonnon=id). Mais c'était un déni PUREMENT PSYCHOLOGIQUE. Dans les faits, c'était juste une erreur (un peu comme quelqu'un qui a payé ses shoes 700E a plus de mal à penser qu'on en obtient des vraies à 40E aux puces et préfère croire que les puces est un vaste marché illégal organisé en toute lumière et avec pignon sur rue dans le nord de Paris)
Ca a permis à un scientifique nommé Timothy Griffin de devenir l'idole à égalité avec Godel de notre contemporain Jean-Louis Krivine qui considère sa découverte comme aussi importante que celle de Godel.
La découverte que l'axiome du tiers exclu est "tout autant" programmable que le reste des axiomes de la science est la suivante:
Vous disposez d'une stratégie qui connaissant le digicode de la porte qui permet de passer du lieu $(A\to Paradis)$ au lieu $Paradis$ est capable de vous emmener au paradis à coup sûr.
Et bien à partir de là, vous avez un moyen***** d'aller dans le lieu A: il suffit de donner n'importe quel code (qui n'a aucunement besoin d'être valable) à votre stratégie, et "elle gueulera"*** seulement quand vous serez arrivé dans A, taperez sur le digicode de la porte qui vous mène au paradis et vous apercevrez.... que ce digicode n'est pas le bon.
*** enfin c'est vous qui "gueulerez, si vous vouliez aller au paradis. Mais vous êtes arrivé dans A
En pratique, c'est juste "try .... finally ..." à la place de "begin ... end" (c'est juste un "goto" qui évite de perdre du temps.
***** je donne une "preuve" de l'axiome non intuitionniste ((A=>Paradis)=>Paradis)=>A
Est-ce que ces deux situations sont identiques pour toi?
-1 jouer au poker
-2 jouer au poker avec des sauvegardes (comme dans un jeu vidéo émulé) et revenir à un point antérieur chaque fois que ça se passe mal?
La distinction entre CH et réalisabilité classique me paraît indispensable pour cette raison.
Le "constructivisme" consiste à prendre acte d'un certain manque d'information disponible.
Je serais intéressé par les points spécifiques qui te déplaisent (en plus de celui cité ci-dessus)
A-t-on une preuve intuitionniste de $\neg\neg A\Rightarrow A$ ?
Tu peux consulter ce fil http://www.les-mathematiques.net/phorum/read.php?16,1859928 pour une autre interprétation des énoncés de la logique intuitionniste, qui permet de répondre à ce genre de question (les ouverts d'un espace topologique $X$ sont vus comme des énoncés avec, étant donnés deux ouverts $V,W$, $V \wedge W := V \cap W$, $V\vee W:= V \cup W$, $V \Rightarrow W := \text{intérieur de } (W \cup (X \backslash V))$, $\perp := \emptyset$ et $\top := X$). Les théorèmes intuitionnistes sont égaux à $X$ tout entier.
Si $\neg \neg A \Rightarrow A$ était prouvable, en gros on aurait pour tout espace topologique $X$ et tout ouvert $V$ de $X$, l'inclusion $n(n(V)) \subseteq V$ avec $n(U):= \text{intérieur de } (X \backslash U)$.
Ceci est démenti par le cas où $X=\R$ et $V:= \R \backslash \{0\}$.
1/ Une logique c'est juste un ensemble d'axiomes. Et c'est formel.
2/ La recherche d'exemples "qui ont du sens" auront toujours, donc, une tendance à faire glisser le lecteur vers du hors-sujet.
3/ Par exemple, avec des $a$ particuliers, illustrer la LI en disant qu'elle ne dit pas au titre d'axiome que :
$$ a\in \Q\ ou\ a\notin \Q$$
est DESINFORMANT (enfin peut faire glisser vers le HS assez vite les lecteurs.
4/ Car en réalité, c'est surtout pour le cas où $a$ est inconnu (une constante à propos de laquelle on n'a rien supposé) qu'elle ne le dit pas. Et ça c'est vraiment très simple à comprendre. La LC le dit elle, y compris pour $a$ totalement inconnu. Et là aussi c'est très simple à comprendre.
5/ Aller puiser dans des CONNAISSANCES EXPERTES (c'est à dire dans le fait qu'il n'est pas "évidemment décidable" que $\pi ^ \sqrt{e} \in \Q$ ) peut laisser penser aux lecteurs que ces choses se situent à bac + 3 alors qu'elles se situent à bac -10. Et même si on veut rester à Bac+1, la LI ne prouve pas (comme il a déjà été dit) de manière "pauvre" qu'il existe des fonctions discontinues (par exemple, la LI ne voit pas sans enrichissement autre que
est une fonction définie sur $\R$)
Est-ce que cela signifie qu'on ne peut pas construire un programme avec un nombre réel $x$ en entrée et qui réponde à la question de savoir si on a $x=0$ ? Grosso modo, la machine se trompe pour $x$ non nul suffisamment proche de $0$.
Indiquons un cadre unifié pour Curry-Howard telle que présentée ci-dessus et l'interprétation topologique.
Les considérations de http://www.les-mathematiques.net/phorum/read.php?16,1866650,1866802#msg-1866802 peuvent se généraliser au cas d'une catégorie.
I)Soit $\mathcal C$ une catégorie. Les éléments de $\mathcal C$ sont requalifiés en "énoncés". Soient $A,B\in \mathcal C$
1°)Si $A,B\in \mathcal C$, les éléments de $Hom(A,B)$ sont appelés "preuves de $B$ sous l'hypothèse $A$".
2°) S'il existe un produit cartésien de $A,B$ (noté $A \wedge B$ plutôt que $A\times B$), les projections $A\wedge B \overset{\pi_A^{A,B}}{\longrightarrow} A$ et $A\wedge B \overset{\pi_B^{A,B}}{\longrightarrow} B$ sont alors les preuves de $A$ (resp sous l'hypothèse $A\wedge B$ et pour tout $D\in \mathcal C$, $Hom(D,A\wedge $ est en bijection avec $Hom(D,A) \times Hom(D,B)$, autrement dit "prouver $A\wedge B$ en supposant $D$ revient à prouver $A$ sous $D$ et à prouver $B$ sous $D$.
3°) S'il existe un coproduit de $A$ et de $B$ (noté $A\vee B$ plutôt que $A \coprod B$ dans la suite), les morphismes canoniques $\iota_A^{A,B}: A \to A \vee B$ et $\iota_B^{A,B}: B \to A \vee B$. Pour tout $E\in \mathcal C$ et couple $(f,g)\in Hom(E,A) \times Hom(E,B)$ (i.e.tel que $f$ est une preuve de $E$ sous $A$ et $g$ est une preuve de $E$ sous $B$), l'unique $h:A \vee B \to E$ tel que $h \circ \iota_A^{A,B} = f$ et $h \circ \iota_B^{A,B} = g$ est une preuve de $E$ sous $A \vee B$.
4°) On suppose ici pour pour tout couple $(X,Y)$ d'éléments de $\mathcal C$, l'existence d'un produit cartésien $X\times Y=X \wedge Y$ dont on notera $\pi_{X}^{X,Y} : X\wedge Y \to X$ et $\pi_{Y}^{X,Y} : X\wedge Y \to Y$ les projections canoniques. Lorsque $X,Y,Z,T\in \mathcal C$, $f\in Hom(X,Z)$ et $g\in Hom(Y,T)$, on désignera ci-dessous par $f \times g$ l'unique élément de $Hom(X\wedge Y, Z\wedge T)$ tel que $\pi_Z^{Z,T} \circ (f \times g)=f \circ \pi_X^{X,Y} $ et $\pi_T^{Z,T} \circ (f \times g)=g\circ \pi_Y^{X,Y} $. Pour tout $U\in \mathcal C$ on notera $id_U:U\to U$ le morphisme identité.
On appelle objet exponentiel associé à $A$ et $B$ un couple constitué d'un objet de $\mathcal C$ (noté habituellement $B^A$ mais ici on écrira plutôt $A\Rightarrow B$) et d'un morphisme $\varepsilon_{A,B} \in Hom (A \Rightarrow B \times A,B)$ tels que pour tout $F\in \mathcal C$, l'application $u\in Hom(F,A\Rightarrow \mapsto \varepsilon_{A,B} \circ (u \times id_B)$ est bijective, autrement dit tels que pour toute $f:F\times A \to B$, il existe un unique $\lambda_{F,A,B}(f):F \to (A \Rightarrow $ tel que $f=\varepsilon_{A,B} \circ (\lambda_{F,A,G} (f) \times id_A)$.
Dans la catégorie des ensembles, $A\Rightarrow B$ n'est rien d'autre que l'ensemble des applications de $A$ dans $B$ et $\varepsilon_{A,B}$ l'évaluation qui à $(f,x) \in B^A \times A$ fait correspondre $f(x)$.
L'important ici est que pour tout $E\in \mathcal C$, $Hom(E\wedge A,B)$ et $Hom(E,A\Rightarrow $ sont en bjection, généralisant ce qui a été dit plus haut.
5°) On note respectivement $\top$ et $\perp$ les éléments final et initial (edit: il a fallu les échanger) de $\mathcal C$ lorsqu'ils existent. Ils jouent le rôle de vrai et de faux. Un objet $A$ est un théorème lorsque $Hom(\top, A)$ est non vide (ou de façon équivalente lorsque pour tout $D\in \mathcal C$, $Hom(D,A)$ est non vide).
6°) Les produits et coproduits éventuellement infinis $\prod_{x \in I} A(x)$ et $\coprod_{x \in I} B(x)$ jouent le rôle d'expressions quantifiées $\forall x \in I,A(x)$ et $\exists x \in J, B(x)$.
***********
II) Soit $(H,\leq )$ un ensemble ordonné. On définit une structure de catégorie sur $H$ en posant $Hom(x,y)=\{\emptyset\}$ si $x\leq y$ et $Hom(x,y):=\emptyset$ dans le cas contraire (en gros $card(Hom(x,y))$ vaut toujours $1$ ou $0$ et vaut $1$ ssi $x\leq y$); alors:
-L' élément initial (resp final) de $H$ pour cette structure est, lorsqu'il existe, le plus petit (resp le plus grand) élément de $H$
-Pour tous $a,b\in H$, le produit cartésien (resp coproduit) de $a$ et de $b$ est, lorsqu'il existe, la borne supérieure (resp inférieure) de $\{a,b\}$
-Si toute paire de $H$ admet une borne inférieure, pour tous $a,b\in H$, l'objet exponentiel $a\Rightarrow b = b^a$ est, lorsqu'il existe, le plus grand élément de l'ensemble des $x\in H$ tels que $\inf \{a,x\} \leq b$ (car alors on a pour tout $x$: $x \leq b^a$ si et seulement si $\inf \{a,x\} \leq b$ ou encore: il existe une unique bijection entre $Hom(\inf \{a,x\},b)$ et $Hom(x,b^a)$).
Au final on appelle algèbre de Heyting un ensemble ordonné $(H,\leq)$ dans lequel les points I.1°) à I.5°) ci-dessus s'appliquent, autrement dit tel que:
-toutes les parties finies de $H$ admettent dans $H$ une borne inférieure et une borne supérieure
-pour tous $a,b\in H$, l'ensemble des $\{x\in H \mid \inf \{a,x\} \leq b\}$ admet un plus grand élément.
Une algèbre de Heyting est dite en outre complète si toutes ses parties possèdent une borne supérieure (et donc aussi une borne inférieure - exo).
La topologie d'un espace topologique, ordonnée par l'inclusion, est une algèbre de Heyting complète (avec $A\Rightarrow B :=$ intérieur de l'union de $B$ et du complémentaire de $A$).
Pour être honnête avec toi, je n'y connais pas grand chose en catégorie mais c'est peut-être l'occasion pour moi d'y jeter un œil plus aiguisé. :-S
Je reviendrai vers toi dès que possible pour l'exo borne supérieure implique borne inférieure...
Je suis désolé de faire redescendre le niveau de ce fil mais voilà ce qui me préoccupe: les intuitionnistes refusent-ils le tiers exclu même dans les cas d'évidence (enfin il me semble) comme "soit un réel a , alors a est positif ou (négatif ou nul)", et qu'en est-il quand Andrew rencontre Bernhard dans un bistrot devant un demi bien frais, peut-il lui dire: "cette année le PSG sera champion d'Europe ou bien il ne le sera pas"?
Merci de vos précisions. Le bouquin de Pierre Ageron traitant en particulier un peu de logique intuitionnisme vous parait-il intéressant sur ce sujet?
Cordialement.
Jean-Louis.
En conséquence de quoi, tu ramènes $P$ quelconque à la demande d'égalité à $0$ d'un ensemble.