À 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 ?
Réponses
-
Tu as tout dit dans ton PS : non, il y a des parties de N non décidables, et c'est précisément pour celles-là que ça ne marche pas.
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 ! -
Martial : J'oublie le sens de récursif. Si c'est "il y a un programme qui décide si $x$ est dedans ou pas, en temps fini [ pour les deux réponses ]", alors oui
(Ce n'est pas hors-sujet, la calculabilité est une interprétation du constructivisme, à mes yeux l'une des plus motivantes) -
Ça c'est la version classique.
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 ? -
@Max : "Si c'est "il y a un programme qui décide si x est dedans ou pas, en temps fini [ pour les deux réponses ]", alors oui.
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. -
Si je comprends bien, toutes les preuves basées sur le bon ordre de N, même les plus élémentaires en arithmétique, disparaissent en maths constructives ! Par exemple parmi celles nombreuses du lemme de Gauss (si a divise bc et si a est premier avec b, alors a divise c) il y a :
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 ? -
Merci d'avance pour une réponse.
-
Mais au fait ça veut dire quoi " le plus petit élément de $H$ qui contient $a$ et $b$" ?
-
Ok. Mais comment formulerais-tu l'expression de logique classique "Soit m le plus petit élément de H" pour qu'elle soit acceptable en logique intuitionniste ?
-
Je me suis mal exprimé. Je voulais dire : H contient a et b. Soit m le plus petit ..
-
Christophe avait fait un post récemment là dessus.
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").Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$. -
Merci Foys pour ces explications détaillées, mais je n'en demandais pas tant ! En fait, ma question était très terre-à-terre, et je viens de me rendre compte que Maxtimax y avait parfaitement répondu ! Dans le cas général, on ne peut démontrer qu'une partie arbitraire de N possède un plus petit élément, mais on le peut pour une partie décidable ! J'en ai même moi-même donné une preuve, je suis donc un peu débile ! :-)
-
@GG: en logique intuitionniste, on ne peut pas prouver qu'un ordre total ayant 2 éléments est un bon ordre.Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
-
@GG : je pense que ce que CC veut dire c'est que tu ne peux faire de raisonnement intuitionniste commençant par "soit $E$ un ensemble totalement ordonné à $2$ éléments" et se terminant par "donc $E$ est bien ordonné".
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. -
Pourquoi les sous-ensembles habités de {0, 1} sont-ils {0}, {1} et {0, 1}?
-
Pardon de ne pas m'être connecté. Alesha sait.
Il ne pose pas une question pour lui GG mais pour t'aider. Pour être habité, il suffit de contenir 1.Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi -
Ça me semble être la subtilité qui a été relevée par Maxtimax effectivement. Tu t'es servi de l'existence d'un test d'appartenance à $H$.
-
OK, merci Poirot.
-
@GG, si dans le cadre des axiomes de la théorie des ensembles (extensionnalité et compréhension suffisent ici, en plus de l'axiome des parties et de la paire pour montrer que les objets dont on parle existent) $\{0,1\}$ est bien ordonnable, alors on peut en déduire le tiers exclu.
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)$Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$. -
Oui, merci Foys. (Ageron donne la preuve du th. de Diaconescu).
-
@Alesha, je me rends compte que j'ai oublié de réagir à ton message. J'ai maintenant compris (du moins je le crois :-)) qu'une partie d'une partie décidable de N n'a aucune raison d'être décidable. Par exemple, la partie H de {0, 1} définie par $H = \{x \in N \mid x = 0 \vee ( x = 1 \wedge P) \} $ est décidable si et seulement si P est décidable.
@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 ? -
Cette phrase en italique est fausse (par Diaconescu cité plus haut).GG a écrit:
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 fausse. Qu'en est-il ?
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".Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$. -
J'ai effectivement dit une bêtise, je ne connais pas grand-chose en intuitionnisme.
-
mais GG, je ne rappelle plus avec certitude si tu es à l'aise en topologie élémentaire.
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.Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi -
Pour les gens qui ne veulent pas faire de syntaxe, je redonne la règle du jeu intuitionniste. L'avantage est que vous avez tout comme ça, quantificateurs et second ordre compris.
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]$Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi -
Je suis fasciné par ce théorème de complétude de la logique intuitionniste. Y a-t-il des exemples non triviaux de déduction que l'on peut en faire ?
-
Poirot: je l'ai souvent vu utilisé dans la direction facile (comme souvent pour ce genre de théorème d'ailleurs, étonnamment) : théorème intuitionniste $\implies$ valeur = espace tout entier (enfin, plus précisément, sa contraposée : si la valeur n'est pas l'espace tout entier, c'est que c'est pas prouvable intuitionnistement)
ç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 ) -
Figurez-vous que j'ai acheté ce livre de Pierre Ageron, pour avoir une petite idée de ces mystères logiques. Et voici qu'on le remet en cause, et qu'un ensemble à un élément semble déjà problématique. Même Poirot s'y perd, semble-t-il. Je vais finir par croire que les logiciens c'est comme les trotskystes, quand il y en a trois, il y a déjà une scission. Je vais quand même terminer le livre d'Ageron, qui est écrit avec un style agréable, et je vais m'en retourner à mes mathématiques en attendant que le Landerneau logique se mette d'accord.
Bonne soirée.
Fr. Ch. -
Il n'y a pas de scission, et Poirot a fait une erreur simplement parce qu'il n'est pas habitué à ce genre de questions
-
@chaurien: je ne me connecte pas beaucoup, mais je n'ai pas vraiment compris où tu as vu quelqu'un remettre en cause Ageron???
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}$Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi -
@Christophe : en 3 mots c'est quoi "La logique intuitionniste propositionnelle du second ordre" ?
-
Christophe a écrit:1/ La logique intuitionniste propositionnelle du second ordre est non décidable (je ne me rappelle pas du nom de découvreur)
Joe Wells -
Puisque d'après Ageron la décidabilité de l'égalité dans N découle d'une position philosophique (laquelle en fait?), a-t-on d'autres cas où le TE est accepté par les intuitionnistes comme découlant d'une position philosophique ?(Pour les entiers Ageron dit que leur connaissance se passe de tout intermédiaire...)
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. -
La décidabilité de l'égalité dans N découle du principe de récurrence, pas d'une position philosophique, ainsi que de ce que $s(x) \neq 0$ pour tout $x$ (un autre axiome). On prouve ainsi immédiatement que pour tout $x$,$ x=0\lor x\neq 0$, puis finalement on en déduit assez facilement (à nouveau par récurrence et injectivité de $s$, elle aussi supposée) la décidabilité de N
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 -
Quand on est ignare en la matière comme moi, et qu'on voit Ageron dire qu'il s'agit d'un principe philosophique comme quoi la connaissance des entiers se passe de tout intermédiaire, on le croit. Puis tu viens dire que ce n'est pas ça....Je suis comme Chaurien, je crois que j'abandonne tout espoir de comprendre.Et en plus Brouwer qui utilisait le tiers exclu dans certaines démonstrations,....
Bonne soirée et merci quand même.
Jean-Louis. -
@Jean-Louis : Brouwer est un cas d''espèce. Il te prouve par l'absurde l'existence d'un point fixe pour toute application continue du disque unité fermé dans lui-même sans donner aucune idée de la façon de construire ledit point fixe, et ensuite il se revendique du constructivisme.
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. -
@Martial: des phrases comme $\forall X\exists Y: (X\to Y)$
@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.Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi -
Christophe, tout cela me passe un peu au-dessus de la tête, je vais essayer de faire plus simple. J'ai à la maison 2 pots de peinture uniquement un blanc et un noir et je dois repeindre une porte avec l'un des deux. Alors on ne pourrait pas dire que la porte sera ou blanche ou noire? Bien sûr avant de commencer on le sait pas mai s quand même...
Cordialement.
Jean-Louis. -
@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...Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$. -
Vu tous vos propos je pense être à côté de la plaque. Je prends une pièce de monnaie. Je la lance. Mon adversaire me dit que le résultat n'est pas pile. J'en déduis donc par TE que c'est face. Bien sur la pièce pourrait tomber sur la tranche mais simplifions....
Dans ce petit raisonnement ras de la moquette (que je m'abstiens de fumer), où est l'erreur? -
Et si l'adversaire déclare "je ne confirme pas que ce n'est pas un pile"? On ne pourra pas confirmer que c'est un pile pour autant.Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
-
Dans l'interprétation de Brouwer-Heyting-Kolmogorov (devenue plus tard la correspondance de Curry-Howard), on a un mécanisme de certification qui vérifie les propriétés suivantes:
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$) Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$. -
Rappelons avant une plainte prévisible que la réalisabilité classique n'est pas la correspondance de Curry-Howard (mais un nouveau paradigme distinct, ce qui n'enlève rien à sa pertinence. Et puis Ocaml n'est pas exactement un langage typé puisqu'on peut contourner le système de typage avec des "objets magiques"...).Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
-
Une remarque en passant, peut-être est-elle susceptible d'éclairer Jean-Louis: l'énoncé
$(((a = 0 \vee a = 1) \wedge a \not= 0) \Rightarrow a = 1)$
est prouvable en logique intuitionniste (sans TE donc). -
@JLouis, d'abord je te prouve ce que dit Alesha, ensuite je réponds à tes questions d'au dessus.
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"Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Connectez-vous ou Inscrivez-vous pour répondre.
Bonjour!
Catégories
- 163.1K Toutes les catégories
- 7 Collège/Lycée
- 21.9K Algèbre
- 37.1K Analyse
- 6.2K Arithmétique
- 53 Catégories et structures
- 1K Combinatoire et Graphes
- 11 Sciences des données
- 5K Concours et Examens
- 11 CultureMath
- 47 Enseignement à distance
- 2.9K Fondements et Logique
- 10.3K Géométrie
- 62 Géométrie différentielle
- 1.1K Histoire des Mathématiques
- 68 Informatique théorique
- 3.8K LaTeX
- 39K Les-mathématiques
- 3.5K Livres, articles, revues, (...)
- 2.7K Logiciels pour les mathématiques
- 24 Mathématiques et finance
- 312 Mathématiques et Physique
- 4.9K Mathématiques et Société
- 3.3K Pédagogie, enseignement, orientation
- 10K Probabilités, théorie de la mesure
- 772 Shtam
- 4.2K Statistiques
- 3.7K Topologie
- 1.4K Vie du Forum et de ses membres
In this Discussion
Qui est en ligne 28
+19 Invités