À propos du "Ageron"
Bonjour à tous les afficionados du constructivisme !
(pour alléger le texte, je sous-entends le plus souvent l'appartenence à N)
La leçon 4 du "Logique, etc. Le point de vue constructif" de Pierre Ageron commence par énoncer trois principes, communs aux maths classiques et intuitionnistes :
4.1. Décidabilité de l'égalité dans N.
On a toujours $a = b$ ou $a \neq b$.
4.2. Totalité de l'ordre dans N.
On a toujours $a \leqslant b$ ou $b \leqslant a$.
4.3. Principe de récurrence.
Mais il ne donne pas de définition de la relation d'ordre $a \leqslant b$ . J'imagine (et donc je suppose) que c'est $\exists k $ $b = a+k$.
Puis il démontre :
4.5. Théorème. Les assertions suivantes sont équivalentes :
(i) la conjonction du principe du tiers exclus et du principe de récurrence ;
(ii) tout sous-ensemble habité de N possède un plus petit élément.
Or il me semble que j'arrive à démontrer (ii) par récurrence, sans utiliser le tiers exclus.
Je commence par montrer par récurrence que tout entier non nul possède un prédécesseur.
Puis que
$m > n \Rightarrow m \geqslant n+1$ :
Je suppose m > n. Il y a donc un k tel que m = n+k et k non nul. On a ainsi un k' tel que m =n+k+1 et donc $m \geqslant n+1$.
Pour montrer (ii) par récurrence, je considère la propriété $P(n)$ : Toute partie de N contenant n possède un plus petit élément.
Vrai pour n = 0.
Je suppose P(n), et considère une partie H de N contenant n+1.
F = H U {n} contient donc un plus petit élément k.
Alors soit k est différent de n, auquel cas k est dans H et est son plus petit élément,
soit k = n. Dans ce cas, si k est dans H, c'est son plus petit élément. Sinon, pour tout m de H, k < m, n+1 $\leqslant$ m et n+1 est le plus petit élément de H.
Ainsi on a P(n+1).
Où est mon (mes) erreur(s) ?
P.S. Il est clair que j'utilise $k \in H \vee k \notin H$. Mais considérer une partie H de N, n'est-ce pas précisément se donner une propriété H(n) décidable ?
(pour alléger le texte, je sous-entends le plus souvent l'appartenence à N)
La leçon 4 du "Logique, etc. Le point de vue constructif" de Pierre Ageron commence par énoncer trois principes, communs aux maths classiques et intuitionnistes :
4.1. Décidabilité de l'égalité dans N.
On a toujours $a = b$ ou $a \neq b$.
4.2. Totalité de l'ordre dans N.
On a toujours $a \leqslant b$ ou $b \leqslant a$.
4.3. Principe de récurrence.
Mais il ne donne pas de définition de la relation d'ordre $a \leqslant b$ . J'imagine (et donc je suppose) que c'est $\exists k $ $b = a+k$.
Puis il démontre :
4.5. Théorème. Les assertions suivantes sont équivalentes :
(i) la conjonction du principe du tiers exclus et du principe de récurrence ;
(ii) tout sous-ensemble habité de N possède un plus petit élément.
Or il me semble que j'arrive à démontrer (ii) par récurrence, sans utiliser le tiers exclus.
Je commence par montrer par récurrence que tout entier non nul possède un prédécesseur.
Puis que
$m > n \Rightarrow m \geqslant n+1$ :
Je suppose m > n. Il y a donc un k tel que m = n+k et k non nul. On a ainsi un k' tel que m =n+k+1 et donc $m \geqslant n+1$.
Pour montrer (ii) par récurrence, je considère la propriété $P(n)$ : Toute partie de N contenant n possède un plus petit élément.
Vrai pour n = 0.
Je suppose P(n), et considère une partie H de N contenant n+1.
F = H U {n} contient donc un plus petit élément k.
Alors soit k est différent de n, auquel cas k est dans H et est son plus petit élément,
soit k = n. Dans ce cas, si k est dans H, c'est son plus petit élément. Sinon, pour tout m de H, k < m, n+1 $\leqslant$ m et n+1 est le plus petit élément de H.
Ainsi on a P(n+1).
Où est mon (mes) erreur(s) ?
P.S. Il est clair que j'utilise $k \in H \vee k \notin H$. Mais considérer une partie H de N, n'est-ce pas précisément se donner une propriété H(n) décidable ?
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
Si tu réfléchis à ta preuve, elle correspond à l'algorithme suivant : je commence par tester si $0$ est dans $H$, puis si $1$ est dans $H$ puis si $k$ est dans $H$ etc. Lorsque $H$ n'est pas décidable, aucune chance !
Je ne connais pas grand-chose en intuitionnisme, mais si je suis ton raisonnement j'ai l'impression que "décidable" a le même sens que "récursif".
Je me trompe ?
(Ce n'est pas hors-sujet, la calculabilité est une interprétation du constructivisme, à mes yeux l'une des plus motivantes)
Une partie de N c'est juste un ensemble H tel que pour tout x, H(x) implique N(x)
Ce n'est pas défini dans ton texte ?
Oui c'est cela, en admettant la thèse de Church. Sinon c'est une partie de $\mathbb{N}$ dont la fonction indicatrice est récursive totale.
Une partie $E \subseteq \mathbb{N}$ est dite récursivement énumérable si elle est le domaine, ou l'image, d'une fonction récursive. Donc $E$ est décidable ssi $E$ et son complémentaire sont récursivement énumérables.
@GG : n'oublie pas qu'il n'y a qu'une famille dénombrable de parties de $\mathbb{N}$ qui sont décidables, alors qu'il y a autant de parties de $\mathbb{N}$ que de réels.
Soit H l'ensemble des entiers non nuls x tels que a divise cx.
Soit m le plus petit élément de H qui contient a et b. On voit que tous les éléments de H sont multiples de m. On a donc m = 1 et a divise c.
Peut-on rendre cette preuve constructive en gardant la même idée ?
Et de toutes façons ton ensemble $H$ est décidable : pour tout entier $x$ tu as un algorithme qui te permet de savoir en un temps fini si $cx$ est divisible par $a$ ou pas.
Etant donné un langage du premier ordre $\mathcal L$, un contexte $\mathcal C$ (i.e. l'ensemble des variables libres sur lesquelles sont construites les formules: on introduit la notion en vue d'assainir les affirmations sur les quantificateurs et ne parlerons que de démonstration naturelle avec contextes) et un ensemble d'énoncés $\Gamma$ sur $\mathcal L$ à variables libres dans $\mathcal C$ , on va dire qu'une formule $F$ de $\mathcal L$ est $\Gamma,\mathcal C$-régulière (ou simplement régulière s'il n'y a pas de risque de confusion) si $\Gamma \vdash_{\mathcal C} (\neg \neg F) \Rightarrow F$ en logique intuitionniste (l'adjectif "régulière" vient des ouverts réguliers d'un espace topologique vu comme algèbre de Heyting: i.e. les ouverts $U$ tels que $\sim \sim U=U$ où $\sim V$ désigne l'intérieur du complémentaire de $V$).
En fait, les formules régulières sont celles auxquelles le raisonnement par l'absurde est applicable.
On a les propriétés suivantes étant donnés $\Gamma,\mathcal C$ (exos tout à fait abordables et recommandés pour assimiler l'idée):
1°) Pour toute formule $F$, $\neg F$ est régulière.
2°) Toute formule $F$ décidable (i.e. telle que $\Gamma \vdash_{\mathcal C} F \vee \neg F$) est régulière
3°) Pour toutes formules $F,G$ régulières, $F \wedge G$ est régulière.
4°) $\perp$ est régulière
5°) Pour toute formule régulière $B$ et toute formule $A$, $A\Rightarrow B$ est régulière
6°) Pour toute lettre $u$ non dans $\mathcal C$ et toute formule $H$ ayant ses variables libres dans $\mathcal C \cup \{u\}$, si $H$ est $\Gamma,\mathcal C\cup \{u\}$ -régulière alors $\forall u,H$ est $\Gamma,\mathcal C$ régulière.
(autrement dit si $\Gamma \vdash_{\mathcal C \cup \{u\}} (\neg \neg H) \Rightarrow H$ alors $\Gamma \vdash_{\mathcal C} \left (\neg \neg \forall u, H \right ) \Rightarrow \forall u, H$).
Ainsi, si on se cantonne aux formules écrites à partie de formules régulières et des connecteurs $\neg, \wedge, \forall, \Rightarrow$ , toute démonstration en logique classique d'une formule régulière $G$ entraîne que ladite formule est un théorème intuitionniste (et que ce sont les $\exists$ et $\vee$ qui n'ont en fait pas le même sens qu'en logique classique: pour le mathématicien constructiviste/intuitionniste, "il existe x tel que P" veut dire "je sais livrer x tel que P" et "A ou B" veut dire:au moins une des formules A,B est vraie et je peux dire laquelle).
En arithmétique de Heyting (i.e. Peano intuitionniste), il est prouvable pour tous entiers $p,q$, que $p=q$ est décidable.
Comme toutes les formules atomiques de l'arithmétique sont de la forme $s=t$ où $s,t$ sont des termes, il en résulte que toute formule écrite sans les symboles $\exists,\vee$ (on appelle "formules de Harrop" de telles formules) et qui est un théorème de Peano classique est aussi un théorème de l'arithmétique intuitionniste de Heyting.
On en déduit aussi un procédé simple pour transformer une formule logique quelconque $F$ en formule logique $i(F)$ classiquement équivalente à $F$ et qui est telle que $F$ est un théorème classique si et seulement si $i(F)$ est un théorème intuitionniste ("traduction de Godel-Gentzen"): il suffit de virer tous les $\exists / \vee$et de remplacer les formules atomiques par leur double négation si elles ne sont pas régulières, autrement dit on définit par induction $i$ de la façon suivante
-Si $A$ est atomique, $i(A):=\neg \neg A$ (où à la rigueur $A$ si $A$ est régulière/décidable)
-$i(\perp):= \perp$; $i(\neg := \neg i(B)$
-$i(F\wedge G):= i(F) \wedge i(G)$; $i(F \Rightarrow G):= i(F) \rightarrow i(G)$
-$i(F \vee G) := \neg \left ( \neg i(F) \wedge \neg i(G) \right )$ (mais $\left ( i(F) \Rightarrow i(G)\right) \Rightarrow i(G)$ serait également possible)
-$i(\forall x, H) := \forall x, i(H)$
-$i(\exists x,H) := \neg \forall x,\left (\neg i(H) \right )$.
Il existe d'autres procédés de traductions de ce type ("traduction de Kuroda").
Si tu prends l'exemple concret $\{0, 1\}$ muni de l'ordre usuel alors il est intuitionnistement bien ordonné, mais ce n'est pas la question.
Il ne pose pas une question pour lui GG mais pour t'aider. Pour être habité, il suffit de contenir 1.
j'ai ouvert ce fil parce que je croyais, à tort, avoir démontré que toute partie habitée de N posséde un plus petit élément. En fait, ma preuve montre que toute partie habitée décidable de N possède un plus petit élément.
Peux-tu confirmer ?
C'est une conséquence du théorème de Diaconescu (cf moteur de recherche).
On peut d'ailleurs le prouver directement ici (tout ce qui suit est intuitionniste, les ellipses sont des exos): pour tout $x$, $x\in \{0,1\}$ si et seulement si $x=0$ ou $x=1$ par définition.
On en déduit que pour tous $a,b\in \{0,1\}$, $a=b$ ou $a\neq b$ (qui abrège $\neg (a=b)$).
Soit $P$ un énoncé quelconque (du premier order sur le langage de la théorie des ensembles).
Soient $A_0 := \{x\in \{0,1\} \mid x=0 \vee P\}$ et $A_1:= \{x \in \{0,1\} \mid x=1 \vee P\}$. Ces ensembles sont non vides ($0\in A_0$ et $1\in A_1$).
On suppose que $\leq$ est un ordre sur $\{0,1\}$ pour lequel ces deux ensembles ont chacun un plus petit élément, ces minimums seront notés respectivement $m_0$ et $m_1$.
Alors on déduit $P$ des résultats (exos) intuitionnistes suivants $(m_0=m_1)\Rightarrow P$, $(m_0\neq m_1) \Rightarrow \neg P$, et on conclut via $(m_0 = m_1) \vee (m_0 \neq m_1)$
@Poirot, du coup, il me semble que ta remarque
Si tu prends l'exemple concret $\{0, 1\}$ muni de l'ordre usuel alors il est intuitionnistement bien ordonné, mais ce n'est pas la question.
est inexacte (si la partie habitée $ \{x \mid x = 1 \vee ( x = 0 \wedge P) \} $ de $\{0, 1\}$ avait un plus petit élément, on aurait $P \vee \neg P$ et le tiers exclus).
Qu'en penses-tu ?
En fait par réflexe on fait intuitivement comme si l'ensemble des parties d'un ensemble fini était simple mais dès qu'il n'y a plus de tiers exclu c'est tout le contraire qui peut se produire.
Rien que $\mathcal P(\{1\})$ est déjà complètement barré (c'est le classifiant des sous-objets de la catégorie des ensembles: lire un cours sur les topos pour voir à quel point cette structure est riche).
C'est un ensemble de "valeurs de vérité". Il s'identifie aux classes d'équivalence d'énoncés de la façon suivante: si $F$ une formule close du premier ordre quelconque, on pose $X_F:= \{x\in \{1\} \mid F\}$.
Alors si $G,H$ sont deux telles formules, il est immédiat que ZF entraîne intuitionnistiquement $(G \Leftrightarrow H) \Leftrightarrow (X_G = X_H)$.
Si on a droit au tiers exclu, étant donné un énoncé $F$,on déduit de $F \vee \neg F$ le fait que $X_F=\{1\}$ ou $X_F=\emptyset$. En revanche, sans ça il y a beaucoup plus de classes d'équivalence d'énoncés et dans certaines sémantiques, $\mathcal P(\{1\})$ est "gros".
Mais si oui la logique intuitionniste ne doit plus avoir de secret pour toi: à la place de vrai et faux, tu prends les ouverts d'un espace topologique, c'est tout.
Au lieu de vivre dans $\{vrai; faux\}$, les valeurs de vérité vivent dans une topologie.
* "A et B" est l'intersection de A et de B
* "A ou B" est la réunion de A et de B
* A=>B est la réunion des ouverts X tels que (A inter X) inclus dans B
* $\forall x\in Gertrude: R(x)$ est l'intérieur de l'intersection des $R(w)$ quand $w$ parcourt $Gertrude$.
* $\exists x\in Chloe: R(x)$ est la réunion des $R(s)$ quand $s$ parcourt $Chloe$.
* non(A) est l'intérieur du complémentaire de A
Un théorème est intuitionniste quand il vaut l'espace entier quelque soit la topologie utilisée pour lui affecter une valeur.
L'énoncé [ A ou (non(A)) ] n'est pas un théorème car il y a plein d'espaces topologiques et d'ouverts pour lesquels le complémentaire n'est pas ouvert.
Exercice: non(non(A)) est l'intérieur de l'adhérence de A et diffère souvent de A
Tu prends par exemple l'espace $[0,3]$ doté de la topologie usuelle et la partie $X$ qui contient $0$ avec "proba" $]1,2[$ et $1$à coup sûr (ie avec "proba" $[0,3]$), je t'invite à calculer la "proba" de l'énoncé "X admet un minimum". J'ai choisi mon exemple au hasard tellement je suis "habitué" au fait qu'il est "rare" que tu obtiennes le vrai pur (c'est à dire ici $[0,3]$ ). Je n'ai même pas pris la peine de vérifier et je suis à peu près sûr (98%) que tu n'obtiendras pas $[0,3]$
ça permet des résultats d'impossibilité: "on ne peut pas prouver ci sans raisonnement par l'absurde" (e.g. théorème du buveur; mais parfois aussi des trucs plus sophistiqués)
C'est la version "topos de faisceaux" du même théorème de complétude pour tous les topoi, qu'on utilise à nouveau en général dans le sens facile (mais ce dernier commentaire ne plaira pas à Christophe :-D )
Bonne soirée.
Fr. Ch.
Sinon, tu as fait une bonne acquisition, mais la "bonne volonté" est toujours catalysatrice du progrès :-D Si tu pars avec tes préjugés, tu risques de jeter les "sots l'y laisse" du domaine.
@max: c'est quoi l'erreur de Poirot? Je n'ai pas tout lu, mais j'ai juste vu qu'il partageait une sensation :-S
@tous, la complétude "la plus dure à prouver" est la complétude historique, celle de la logique classique. Les complétudes découvertes ensuite n'ont pas d'auteurs véritables et ne sont que des explorations supplémentaires des mécanismes ayant émergé originellement lors de la preuve à la force du poignet et noyé dans la sueur de la canal historique.
Ce qui a été découvert n'est rien de plus qu'un mélange entre compacité et symétrie, choses qui ne se rencontrent habituellement pas en maths à part ... ah bin cadeau du ciel (au sens de PMF) ... en logique.
Ce qu'il se passe est très simple: quand un machin est important, il est compact (par exemple un ensemble de modèles) et quand il entre dans le champ de la logique (indépendance par rapport aux noms), il est symétrique. Et la compacité fait que quand tout modèle de machin blabla truc, il n'y a qu'un nombre fini d'endroits à regarder pour en être sûr. Ce qui donne, car qui dit fini, dit humainement programmable, une machine syntaxique (et non plus sémantique) et des règles du jeu dont vont sortir des "preuves".
La logique est strictement plus faible que l'axiome du choix au même titre que les idéaux premiers sont tous maximaux mais pas la réciproque. L'ensemble des idéaux premiers d'un anneau est un fermé de $P(LeDitAnneau)$ doté de la topologie usuelle, ce qui donne la règle du jeu :
$$ a\notin P, b\notin P \to ab\notin P$$
Vous n'avez pas de telles caractérisations des idéaux maximaux. Quand à l'adhérence de l'ensemble des idéaux maximaux (qui lui est un "ensemble syntaxique"), je me suis souvent demandé par quoi on pourrait le caractériser et je n'ai jamais répondu (ni vraiment cherché) à la question.
Pour en revenir à la logique que désire, en détestant le désirer, connaitre chaurien l'objet maintenant bien identifié est l'ensemble doté d'une loi opération binaire commutative ET associative, l'implication $X\to Y$ voulant dire
$$\{u\mid \forall x\in X: ux\in Y\}$$
et le reste à l'avenant.
Il est trivial dans les deux sens (il n'y a pas "de sens difficile") que c'est complet pour une logique appelée "linéaire", mais qui est en fait le socle bien identifié de toutes les logiques.
Le reste provient juste du fait qu'on s'intéresse à certains ensembles (si on ne met pas de contraintes, on reste en logique linéaire), à des "idéaux" (au sens $a\in J\to \forall x: ax\in J$), voire pire de chez pire, à des idéaux primaux, ou produits de max (primal donne l'intuitionnisme en gros et prmax la classique).
C'est la correspondance de Curry Howard qui unifie le tout. Les notations sont dégueulasses, mais hélas historiques, dans le fait qu'il faudrait passer au log pour avoir les bonnes: noter $a+b$ au lieu de $a\otimes b$ et $inf(a,b)$ au lieu de $a+b$ (en l'occurrence $a\oplus b$), mais la vie est dure et les chercheurs sont payés alors on leur demande d'expier.
La robustesse de tout ça fait qu'il n'y a rien d'étonnant à ce que la notion de topologie ait été inventée et corresponde à la sémantique de la logique intuitionniste. Ce n'est pas "une merveille", c'est "peu étonnant".
Et j'en profite pour rappeler sur ce forum pour la 20305843654ième fois car j'ai l'impression que ce ne sera jamais assez dit aux gens qui s'y intéressent, que ce n'est tellement pas étonnant qu'il en va de même pour la logique classique (sa sémantique est constituée par les ouverts intérieurs de leur adhérence d'une topologie)
Pour ce qui est de "UN" à l'opposé de "DES" modèles qu'on va mettre en produit** et considérer que ce produit constitue un prépack final avant quotientage, le passage est essentiellement toujours le même, MAIS ATTENTION, justement ce n'est pas la partie importante et elle "n'existe même plus" dans les logiques faibles. Cependant, c'est en se débarrassant*** de l'obligation de taffer dans un produit, y compris en logique classique, que Cohen (Paul) a découvert le forcing.
Après ce discours informel, je suis convaincu que tu es hyper-heureux chaurien :-D ;-)
@Poirot, oui, les exemples sont multiples, mais peut-être pas là où tu les attends, par exemple, le fait qu'on puisse faire avec 2 lettres une infinité de phrases propositionnelles non LI-prouvablement équivalentes (pour une lettre je ne me rappelle plus). Etc. C'est à dire qu'on ne va pas forcément développé un exemple, mais des séries d'exemples significatifs. En voici deux autres:
1/ La logique intuitionniste propositionnelle du second ordre est non décidable (je ne me rappelle pas du nom de découvreur)
edit: un grand merci à alesha qui a fourni l'auteur du théorème: Joe Wells
2/ La logique intuitionniste écrite avec QUE le signe $\to $ et des lettres est PSPACE-complète. Tu vois, c'est bien que "quelques exemples spectaculaires". (C'est le théorème de Statman, mais moyennant l'élimination des coupures admise, il est trivial).
** par exemple "on fait semblant quand on raisonne de travailler dans un monde (un modèle de ZF), mais comme on ne précise jamais lequel, on ne fait que calculer ce qu'il se passe dans le produit de tous les modèles. C'est "inné" aux matheux).
*** algèbre de Boole qui ne sont pas, et de manière profonde (ne pas être) des produit de $2$, ie des $2^{EnsemblesDeMondes}$
Joe Wells
Décidément, j'ai du mal avec TE. Bien sûr certains d'entre vous me sortent des cas compliqués où effectivement je comprends qu'il y ait problème. Mais j'ai du mal à être dans l'impossibilité d'admettre le raisonnement suivant: En 2021 le PSG gagnera la champions league ou il ne la gagnera pas. Pourquoi les nombreux exemples simples comme celui-là semblent être refusés par les spécialistes qui pondent toujours des cas (certainement vrais et solides) mais d'une extrême complexité. (est-ce parce qu'ils ne sont pas formalisés?)
Cordialement.
Jean-Louis.
Christophe: l'erreur de Poirot était de croire que $\{0,1\}$ était bien ordonné, prouvablement en logique intuitionniste - à nouveau ce n'est pas du tout une grosse erreur venant de quelqu'un qui n'a pas l'habitude de ce genre de sujets, pas la peine de s'attarder là dessus
Bonne soirée et merci quand même.
Jean-Louis.
Je pense sincèrement que le courant intuitionniste serait rapidement tombé en désuétude s'il n'y avait pas eu la correspondance de Curry-Howard, et aussi les liens avec les algèbres de Heyting... mais hélas je ne connais pas grand-chose à ces 2 domaines.
@Max: ça devait être un post antérieur de Poirot que je n'avais pas lu
@Jean Louis: le Ageron est "agréable" ce qui est différent "d'informant-dans-l'ordre". Il villégiature. Par moment il dit "gentiment n'importe quoi", car il écrit parfois comme une conversation conviviale.
@Martial: tu as à mon sens ENTIEREMENT RAISON dans ce que tu affirmes à ton dernier post. On parle parfois de robustesse pour ce genre de mécanisme. Mais l'histoire aurait pu être différente si l'idole de JLK (à savoir Timothy Griffin/Griffith) avait découvert comment exécuter le RPA avant que ces développement ne démarrent.
Longtemps les gens ont cru (à tort) que l'intuitionnisme différait du classicisme par sa constructivité en s'appuyant sur la non constructivité de A ou nonA, et plus généralement, celle, apparente des différents axiomes tous équivalents entre eux, affirmant le RPA.
Comme son exécutabilité a été découverte tard, ça n'a pas effacé les travaux antérieurs, mais disons qu'en gros, chez les spécialistes maintenant si le pistolet sur la tempe on les forçait à faire des discours de synthèse, ils reconnaitraient que $A\to (A+A)$ est bien plus magique que $non(nonA)\to A$.
Penser aux anneaux: $\forall x: x=x^2$ est ultracontraignant (entraine commutativité, premiers = maxs, [noetherianité=>finitude], etc). Alors que la symétrie attaque/défense (ie l'unique élément autre que le neutre de $S_2$) n'est pas "en soi" mystérieuse ou productrice. En calcul des séquents, LA SEULE différence entre LI et LC est le droit de mettre une liste et non pas une seule phrases à droite.
@Jean-Louis: pour ton match de foot, tu as deux et non pas une approche de l'inconnu futuriste. Bien des gens éduqués à vouer un culte à l'intuitionnisme historique se sont pavloliennement conditionnés à l'appliquer à ton exemple pour le plaisir du ni vrai, ni faux "car on sait pas encore". Mais en fait la deuxième approche, quantique (ou logique linéaire), qui dit que ce n'est pas un théorème d'avoir: $[non(A^\infty)]\to (nonA)^\infty$ semble plus pertinente.
L'approche intuitionniste qui construit un arbre de Krypke avec deux sous-branches (chacune faisant gagner son équipe) a l'inconvénient majeur d'imposer la structure arbre et d'écraser des choses qui mériteraient d'être surveillées. Ca a été "réparé" en corrigeant l'erreur plus en amont de la duplication des garanties, même s'il reste intéressant DANS DES CONTEXTES bien choisis d'approcher l'incertain par l'intuitionnisme.
Cordialement.
Jean-Louis.
Tu sais déjà qu'il n'est pas vrai que la porte ne sera ni blanche ni noire. Cependant si tu dois t'engager lundi à peindre la porte mardi d'une couleur donnée alors que tu veux te réserver la possibilité de choisir...
Dans ce petit raisonnement ras de la moquette (que je m'abstiens de fumer), où est l'erreur?
1°) Un cerificat de $A\wedge B$ est par définition un couple $(p,q)$ où $p$ est un certificat de $A$ et $q$ un certificat de $B$.
2°) Un certificat de $\forall i \in I,A(i)$ est une famille $(p_i)_{i \in I}$ où pour tous $i\in I$, $p_i$ est un cerificat de $A(i)$.
3°) Un certificat de $A\Rightarrow B$ est une fonction qui produit infailliblement un certificat de $B$ lorsqu'on lui fournit un certificat de $A$.
4°) Un certificat de $\exists i \in I, A(i)$ est un couple $(j,q)$ où $j\in I$ et $q$ est un certificat de $A_j$.
5°) Un certificat de $A\vee B$ est un couple $(j,q)$ où $j\in \{0,1\}$ et, si $j=0$, $q$ est un certificat de $A$ et si $j=1$, $q$ est un certificat de $B$ (intuitivement, $\exists i \in \{0,1\}, A_i$ et $A_0 \vee A_1$ veulent dire la même chose et le présent paradigme les traite de la même façon).
Un certificat de $\perp$ est un mécanisme qui produit infailliblement, pour tout énoncé $P$, un certificat de $P$ ($\perp$ signifie intuitivement "tout est vrai").
$\neg X$ abrège "$X \Rightarrow \perp$" ici.
Dans ces conditions, au nom de quoi on aurait, pour un énoncé quelconque, un certificat de $A \vee \neg A$?
******************
Quelques exemples illustratifs du paradigme précédent.
1°) Produisons, étant donné trous énoncés $A,B,C$, un certificat de $\left ((A\Rightarrow \wedge (B\Rightarrow C) \right) \Rightarrow (A\Rightarrow C)$.
Considérons un certificat $p$ de $(A\Rightarrow \wedge (B\Rightarrow C) $.
Alors $p$ est un couple $(q,r)$ avec $q$ certificat de $A\Rightarrow B$ et $r$ un certificat de $B\Rightarrow C$.
Un certificat de $A\Rightarrow C$ est une fonction transformant un certificat de $A$ en un certificat de $C$;
Soit $x$ un certificat de $A$. Alors $r\left (q (x)\right ) = r \circ q (x)$ est un certificat de $C$. La fonction cherchée est donc $r \circ q$ et la preuve du syllogisme $\left ((A\Rightarrow \wedge (B\Rightarrow C) \right) \Rightarrow (A\Rightarrow C)$ n'est rien d'autre que la composition des applications i.e. $(f,g)\mapsto g \circ f$.
2°) des certificats de $(A\wedge \Rightarrow A$ et de $(A \wedge \Rightarrow B$ sont donnés par les projections respectivement sur la première et deuxième coordonnée.
3°) si $f:A\Rightarrow C$ et $g:A \Rightarrow C$ sont des certificats,soit $h$ l'application qui à un certificat $x$ de $A\vee B$ fait correspondre
(i) $f(u)$ si $x=(0,u)$ et $u$ certifie $A$
(ii) $g(v)$ si $x=(1,v)$ et $v$ certifie $B$.
Alors $h$ est un certificat de $(A \vee \Rightarrow C$ (correspondant à une distinction de cas afin d'établir $C$ quand on est en possession de la certitude de $A\vee B$ et de celles de $A\Rightarrow C$ et de $B \Rightarrow C$)
$(((a = 0 \vee a = 1) \wedge a \not= 0) \Rightarrow a = 1)$
est prouvable en logique intuitionniste (sans TE donc).
Supposons que $a = 0 \to Tout$
1/ Supposons que $a=0$. On a alors Tout, donc $a=1$
2/ Supposons que $a=1$. On a alors $a=1$.
3/ Finalement on a $a=1$ à partir de l'hypothèse $a=0\vee a=1$
Tu fais beaucoup trop de philosophie et pas assez de "technique". Il n'y a pas "une substance transcendantale" qui va te dire quels sont les bons axiomes. Ta disjonction futuriste est vraie en logique classique, c'est tout. Tu ne cesses de rappeler et rappeler qu'elle est vraie... oui en logique classique. On donne froidement des noms aux choses: les évidences incontestables au premier coup d'oeil forment les axiomes ... de la logique classique.
Tu as l'air de vouloir te plaindre que les logiques plus faibles ne contiennent pas TOUTES ces évidences. Mais si elles les contenaient elles seraient EGALES à la logique classique.
Le feeling qu'il y a derrière la logique intuitionniste c'est qu'il y a plusieurs futurs d'une part, donc pile peut survenir dans les futurs 1;3;4;9 et face dans les autres. Aucun de ces deux ensembles ne forment le "vrai pur" (ensemble de tous les futurs).
Mais surtout, l'important, c'est que tu n'autorises pas tous les ensembles de mondes.. Si tu le fais tu obtiens un algèbre de Boole triviale où les seules incertitudes proviennet du fait qu'on ne sait pas dans quel monde on est. Ce qui fait que dans CHAQUE futur, il est vrai que $[a=0$ ou $a=1]$.
Les logiques plus faibles "n'acceptent pas" (la logique intuitionniste n'est pas la seule et en un certain sens elle est même "la plus pourrie" dans sa façon de ne pas l'accepter (structure ordonnée) comme le fait la classique que tes futurs soient des entités autonomes et qui ne communiquent pas entre elles de sorte que tu vas juste recenser où tel machin arrive et ou son opposé arrive (avec ici opposé = contraire)
Elles introduisent une interaction entre mondes. Par exemple, la logique intuitionniste, qui comme je te le disais est la plus pourri, décide de tuer les solitaires isolés (c'est la logique des cours de récréation où on exécute les victimes de bizutages répétés si tu veux une image). Elle ne retient donc que l'INTERIEUR (au sens topologique) de l'ensemble des mondes où le truc survient.
Par exemple pour ton histoire de pièce, les futurs de $[0,1[$ verront pile et ceux de $]1,2]$ verront face. Alors tu me diras, que voit $1$? Et bien c'est tout bête, il voit face. Mais la logique intuitionniste le dégage à coups de pieds dans le Q car il n'est pas dans un voisinage où tout le monde voit face. C'est "la victime" de la vindicte populaire du monde des futurs.
Bref, il n'y a rien de mystérieux, c'est de la technique d'étude des ensembles de mondes. La science a parfois besoin de "solidité", donc veut "des ouverts entiers, fussent-ils petits" où c'est constant pour être pris en compte, et privilégiera alors l'intuitionnisme.
Mais tu as encore de grosses magies dans l'intuitionnisme (au sens de grosses séparations entre les mondes) qui n'existent même plus dans les logique encore plus faibles où ils se parlent tous et s'interpellent même d'un bout à l'autre de la classe comme de méchants élèves turbulents.
Une part des maths pragmatiques appliquées a d'ailleurs su s'inspirer de ces approches variées pour créer "d'horribles théories" peu goutées par les logiciens (chacun son domaine) où on exploite à fond ça: par exemple dans des formats vidéo tels que le mp4. Ces formats à base d'ondelettes ,ne fournissent pas du tout des "successions d'images bien nettes" mais un fatras de machins calculés à coups de transformées de Fourier et basé sur la connaissance qu'on a de comment de toute façon le cerveau va reconstruire la netteté et "inventer" l'information que ne contient pas la vidéo.
Le cerveau est très puissant et des outils sont développés en connaissance de cause. Je te joins d'ailleurs une image (si je la trouve), où c'est très bien illustré : la case à droite de A et celle à gauche de B sont de la même couleur, mais le cerveau n'a pas besoin de ça pour construire "leur différence dans le roman que la photo raconte"