From madore@news.ens.fr References: Path: eleves.ens.fr!not-for-mail From: GroTeXdieck Newsgroups: ens.forum.archeo-forum.maths-info Message-ID: NNTP-Posting-Host: clipper.ens.fr Xref: eleves.ens.fr ens.forum.archeo-forum.maths-info:134 Date: 14 Jun 1998 19:27:08 MET Subject: logiques Bon, je vais essayer d'être un peu clair et de ne (pourtant :-) pas dire trop de bêtises. À la base, la logique, c'est quelque chose de purement syntactique (en tout cas, c'est une approche possible). On considère des propositions, et on cherche à en démontrer certaines au moyen de règles et d'axiomes, la plus importante étant la règle du modus ponens (si on sait montrer a->b et qu'on sait montrer a alors on peut en déduire b). C'est après qu'on peut introduire l'idée de valeurs de vérité : on cherche un ensemble de valeurs à affecter à chaque formule, et des opérations sur ces valeurs qui correspondent aux connecteurs logiques, avec en plus une (ou plusieurs) valeur(s) spéciale(s) appelée(s) « vrai(e)(s) », de telle sorte que lorsqu'une formule est un théorème, sa valeur est vraie, et, si possible, réciproquement. Là, on passe de la syntaxe à la sémantique, et la partie directe (tout théorème est « vrai ») s'appelle la soundness [traduc ?]) de la sémantique, tandis que la partie réciproque (tout ce qui est « vrai » est un théorème) s'appelle la complétude de cette sémantique. Le cas de base, c'est le calcul propositionnel classique. Il est formé des connecteurs -> (implication), /\ (conjonction), \/ (disjonction), 1 (le Vrai) et 0 (le Faux) plus d'un stock arbitraire de variables propositionnelles. L'unique règle est la règle de modus ponens, et les axiomes sont (pour a et b des propositions quelconques) (K) a->b->a [« Ça change rien »] (S) (a->b->c)->(a->b)->a->c [« Supposons un peu »] (p1) a/\b->a [« En particulier »] (p2) a/\b->b [idem] (P) a->b->a/\b [Introduction du « et »] (q1) a->a\/b [« En particulier »] (q2) b->a\/b [idem] (Q) (a->c)->(b->c)->a\/b->c [« Dans les deux cas »] (V) 1 [Trivial] (F) 0->a [« Si les poules avaient des dents »] (W) ((a->b)->a)->a [Loi de Pierce] La « bonne » sémantique pour cette logique (celle qui est universelle dans un sens technique, qui est sound et complète, et qui est essentiellement la seule à l'être) consiste à attribuer à chaque formule une valeur de vérité qui est une fonction de {0,1}^X vers {0,1}, où X est l'ensemble des variables propositionnelles. Le « vrai », ce sont les fonctions constantes égales à 1, et les connecteurs correspondent aux fonctions que l'on sait. On dit donc qu'il s'agit d'une logique à deux valeurs de vérité. Ce n'est peut-être pas une très bonne expression, puisque après tout, une variable propositionnelle toute seule n'est ni vraie ni fausse. Quoi qu'il en soit, la « bonne » structure sémantique, c'est l'algèbre de Boole. La négation se définie par ~a = a->0 (« a est complètement absurde ! »). La loi de Pierce peut, moyennant les autres axiomes, se reformuler de plusieurs façons différentes : a\/~a (loi du tiers exclu, ou « tertium non datur » pour faire savant), ou ~~a->a (raisonnement par l'absurde). Sa forme originale (si on sait démontrer un théorème en lui supposant plein de conséquences mirifiques, alors on sait le démontrer de toute façon) n'est peut-être pas très claire, mais elle a l'avantage de ne faire intervenir que l'implication. Quand on passe du calcul propositionnel au calcul des prédicats, la notion de sémantique adoptée classiquement, c'est celle de « modèles ». Chaque modèle pris séparément est une sémantique sound, et à deux valeurs de vérité (un modèle attribue à chaque assertion la valeur « vraie » ou la valeur « fausse »), mais ce n'est que quand on considère _tous_ les modèles que la sémantique devient complète (c'est le théorème de complétude de Gödel : une affirmation du calcul des prédicats est démontrable si et seulement si elle est vraie dans tous les modèles). Mais alors il ne s'agit plus vraiment d'une sémantique à deux valeurs de vérité, puisqu'une affirmation indécidable à partir des axiomes est vraie dans certains modèles et fausse dans d'autres : les valeurs de vérité forment une algèbre de Boole compliquée, appelée l'algèbre de Lindenbaum. Effectivement, une affirmation indécidable n'est ni « vraie » ni « fausse » dans le sens qu'elle n'a ni la valeur de vérité 1 ni la valeur de vérité 0 dans l'algèbre de Lindenbaum ; pour un formaliste, les choses s'arrêtent là. Pour un platoniste, persuadé qu'il y a un modèle « naturel » des mathématiques, les notions de « vrai » et de « démontrable » diffèrent. Le théorème d'incomplétude de Gödel affirme que tout système intéressant est incomplet. Et depuis Cohen on sait que l'axiome du choix est indémontrable. Mais ça ne fait pas vraiment un lien entre l'axiome du choix (ou le théorème de Gödel) et l'intuitionnisme. L'intuitionnisme, c'est la logique qu'on obtient en retirant la loi de Pierce (W ci-dessus) des axiomes du calcul propositionnel. L'idée c'est qu'en logique intuitionnisme, ~a dit vraiment que a est complètement absurde, et que quelque chose qui n'est pas (et même pas du tout !) complètement absurde n'est pas pour autant vrai. Ceci permet d'éliminer des raisonnements non constructifs, dans lesquels on montre l'existence d'un objet sans le fournir explicitement, tout simplement parce que son inexistence est absurde. L'intuitionnisme introduit une complication dans les valeurs de vérité : on n'a plus une algèbre de Boole mais une algèbre de Heyting (grosso modo, la structure que forment les ouverts d'un espace topologique). Alors que {0,1} est d'une certaine manière « à la base » de toute algèbre de Boole, les algèbres de Heyting ont une structure plus compliquée. Non seulement on ne peut pas forcément montrer a ou ~a, mais on ne peut même plus montrer a\/~a (alors qu'en logique classique, même si a est indécidable, c'est une tautologie). En fait, c'est à mon avis une erreur de considérer que la logique classique est bivalente, et c'est à cause de ça, je pense, que le forcing n'a pas été découvert plus tôt. Puisque, même si toute algèbre de Boole ressemble furieusement à {0,1}, le forcing impose d'en utiliser d'autres. Maintenant, il y a d'autres types de logique, plus ou moins fumeux et philosophiques, qui compliquent encore la structure des valeurs de vérité. Les deux types les plus importants sont sûrement la logique modale (dans laquelle on rajoute deux connecteurs, les modalisateurs, unaires, qui affirment « il est nécessaire que... » et « il est possible que... »), dont on connaît la sémantique sound et complète depuis Kripke, et la logique linéaire inventée par Girard. En revanche, certaines logiques ne correspondent pas à des syntaxes claires, ni à des structures sémantiques bien définies, et ne présentent guère d'intérêt. Une que je rejette particulièrement, c'est la logique floue, dans laquelle la structure des valeurs de vérité est l'intervalle [0;1]. Pour la syntaxe, ça me semble être surtout du méga-top-pipo. (J'espère que personne ici ne fait de logique floue.) Une idée à la base de l'intuitionnisme, ce sont les postulats de constructivité, par exemple le postulat de disjonction : si on sait montrer a\/b alors on sait montrer a ou bien on sait montrer b ; si on sait montrer qu'il existe un x tel que P(x) alors on sait montrer P(x) pour un certain x, et ainsi de suite. Une erreur commune, cependant, est de croire que tout système intuitionniste vérifie ces principes ; mais il est vrai qu'ils sont vérifiés dans certains systèmes importants (par exemple, l'arithmétique de Peano intuitionniste). L'axiome du choix est un résultat horriblement non constructif (encore que... certains axiomes ultra-constructifs, comme l'axiome de constructibilité justement, entraînent l'axiome du choix ; mais ils sont tout de même constructifs puisqu'ils déterminent explicitement un choix). On s'attend donc qu'il ne cohabite pas bien avec la logique intuitionniste. Effectivement, dans la formulation habituelle de la théorie des ensembles à la ZF en logique intuitionniste (celle que j'ai formalisée en Coq, http://www.eleves.ens.fr/home/madore/sets.v), l'axiome du choix non seulement n'est pas démontrable, mais même implique que la logique est classique. Ce résultat est dû à Diaconescu (j'ai cité la démonstration antérieurement dans ce forum). A priori, ça peut surprendre : comme Papageno le faisait remarquer, il semble naturel de tenir le raisonnement (épistémologique) suivant : si x est un ensemble, et que pour tout élément y de x on sait trouver un élément z de y (c'est le sens de l'existence intuitionniste : « on sait trouver »), alors on devrait savoir trouver une fonction qui à chaque élément y de x associe un élément z de y (c'est l'axiome du choix). En fait, ça ne marche pas, non pas vraiment que la difficulté vienne du fait que x peut avoir « trop » d'éléments pour faire le choix, mais que ces éléments peuvent être « mal séparés » (une fonction devra réussir à les séparer). Ce qui m'avait ennuyé, c'est que Coq est capable de démontrer un théorème qu'ils ont appelé l'axiome du choix. En fait, le problème vient de ce qu'on appelle un ensemble : si l'axiome du choix n'est pas démontrable en logique intuitionniste (puisqu'il ne l'est déjà pas en logique classique !) lorsqu'on part des axiomes de ZF, en revanche si on définit les ensembles par des procédés inductifs comme il est fait dans Coq (ce n'est pas ce que je fais dans le fichier mentionné ci-dessus), alors ce n'est pas le même genre d'ensemble (je dirais même que ce n'est pas le « bon » genre d'ensemble), et l'axiome du choix devient un théorème (assez évident). Mais le « vrai » axiome du choix, celui qui affirme que « Si U est un type, et x:(U->Prop)->Prop est tel que pour tout y:U->Prop vérifiant (x y) il y a un z:U tel que (y z) ; alors il existe h:(U->Prop)->U->Prop, une relation fonctionnelle (c'est-à-dire que si y:U->Prop vérifie (x y) alors il existe un _unique_ z tel que (h y z)) qui choisit un élément de chaque élément de x (c'est-à-dire que si y:U->Prop vérifie (x y) alors l'unique z tel que (h y z) vérifie (y z)). » n'est pas démontrable en Coq (je n'ai pas eu le courage de le formaliser ; si quelqu'un veut essayer). Encore moins ne l'est celui, plus fort, qui affirme la même chose avec une fonction au lieu d'une relation fonctionnelle : « Si U est un type, et x:(U->Prop)->Prop est tel que pour tout y:U->Prop vérifiant (x y) il y a un z:U tel que (y z) ; alors il existe f:(U->Prop)->U qui choisit un élément de chaque élément de x (c'est-à-dire que si y:U->Prop vérifie (x y) alors (y (f x))). » (Le passage de l'une à l'autre serait automatique dans un topos, par le théorème de description, cf. théorème 5.9, page 151 du Lambek&Scott, mais Coq n'est pas un topos.)