David Madore's WebLog: Quelques mots (essentiellement méta) sur l'intuitionnisme et les mathématiques constructives

Cela fait un certain temps que je me dis que je devrais écrire une ou plusieurs entrées sur ce blog sur des sujets tournant autour de la logique intuitionniste et des mathématiques constructives. La présente entrée est une sorte de TODO étendu où je mélange, de façon malheureusement confuse et désorganisée, des remarques introductives voire vulgarisatrices sur le sujet (et expliquant de quoi il est question), des remarques d'ordre méta (où je dis que je devrais parler de ceci ou de cela, ou bien me demande comment je pourrais le faire, ou encore me dis que je ne comprends pas bien telle ou telle chose) et des explications de fond assez disparates (et faites à des niveaux de prérequis, il faut bien le dire, complètement incohérents). Même l'ordre dans lequel je dis les choses est assez bizarre (à la limite, je me demande s'il ne vaut pas mieux lire cette entrée en commençant par la fin). Je pense que ça vaut quand même la peine de publier tout ça, en conseillant au lecteur de simplement sauter les passages qui lui semblent obscurs (puisque de toute façon il y a très peu de dépendances dans ce que je vais raconter).

★

En fait, au départ, je me suis surtout dit que ce serait intéressant d'écrire quelque chose sur le topos effectif et la réalisabilité de Kleene. Je peux au moins recopier l'introduction informelle que j'ai commencé à rédiger à ce sujet :

Pour dire très très très sommairement et très très très vaguement de quoi il est question,

• un topos est une sorte de « monde mathématique alternatif » régi par les lois de la logique intuitionniste (une logique plus faible que la logique usuelle, ou classique, dans laquelle on a essentiellement supprimé la loi du tiers exclu qui affirme que toute formule logique est soit vraie soit fausse, ou, de façon équivalente, que tout ce qui n'est pas faux est vrai) ; de façon un peu plus précise, un topos est une catégorie (peu importe ce qu'est exactement une « catégorie ») qui possède un certain nombre de propriétés communes avec la catégorie des ensembles, ce qui permet d'y mener un certain nombre de constructions mathématiques usuelles, mais dont le comportement va néanmoins être différent sur un certain nombre de choses, et notamment la logique ; et
• le topos effectif est un topos particulier qui présente un intérêt particulier en calculabilité : il présente un monde alternatif dans lequel toutes les fonctions ℕ→ℕ sont calculables, ce qui nous offre un regard neuf sur la calculabilité par rapport à sa présentation classique, où la logique intuitionniste éclaire ce que sont les raisonnements effectifs (voir à ce sujet cet article introductif d'Andrej Bauer, qui ne parle pas du topos effectif mais explique en quoi travailler en logique intuitionniste peut rendre plus facile ou plus naturelle la calculabilité).

Mais reculons d'un cran : pour parler du topos effectif, je me suis dit qu'il fallait d'abord que j'écrive quelque chose sur la réalisabilité de Kleene, qui en est en quelque sorte le prélude. (Si vous voulez savoir très très très sommairement et très très très vaguement de quoi il est question, S. C. Kleene a introduit dès 1945 une notion appelée « réalisabilité », en tentant de donner un sens précis à l'intuitionnisme, et — en très très très gros — le fait qu'une formule arithmétique φ soit « réalisable » [par un entier naturel n] signifie que n en apporte une sorte de « témoignage algorithmique », par exemple, si φ est une formule du type ∀x.ψ(x) affirmant que ψ(x) est vraie pour tout x, alors « réaliser » cette formule va se faire en apportant un programme qui prend en entrée un entier k et en sortie calcule un entier qui réalise ψ(k) ; pour un peu plus de détails, voir le début de cette question que j'ai posée sur MathOverflow, ou pour encore plus, voir le texte Realizability: An [sic] Historical Essay de Jaap van Oosten.) Le lien entre la réalisabilité de Kleene et le topos effectif est très fort : disons que le topos effectif est défini en cherchant une généralisation assez directe de la réalisabilité à des formules plus complexes que celles de l'arithmétique (et les formules arithmétiques qui sont réalisables sont exactement celles qui sont vraies dans le topos effectif).

Ajout : voir cette entrée ultérieure au sujet de la réalisabilité de Kleene, où je la définis proprement ; en voici depuis un sur la réalisabilité propositionnelle. Nouvel ajout : le billet sur le topos effectif est ici.

Bon, mais je me suis alors rendu compte que ce serait commencer in media res de parler du topos effectif ou même de réalisabilité si je ne commençais pas par parler d'intuitionnisme ou de mathématiques constructives. Et là, je suis embêté par le fait que j'ai à la fois trop de choses à dire et pas assez (trop, parce que ça touche à énormément de sujets ; pas assez, parce qu'en ce faisant ça touche aussi à trop de questions sur lesquelles je ne sais pas grand-chose).

Ajout : ce nouveau billet est une tentative de réécriture complète de celui qui suit, et il est peut-être plus clair (ou peut-être que les deux s'éclairent l'un l'autre, je ne sais pas).

★

La logique intuitionniste est une logique plus faible que la logique classique dans laquelle on s'interdit la loi du tiers exclu (qui dit que tout énoncé P est soit vrai soit faux ; c'est-à-dire : P∨¬P) ; cela revient essentiellement à s'interdire le raisonnement par l'absurde (ou plus exactement, le raisonnement par l'absurde de la forme je veux montrer P : supposons par l'absurde que P soit faux <…>, j'arrive à une contradiction, donc P ne peut pas être faux, c'est-à-dire qu'il est vrai — c'est la dernière partie qui coince en logique intuitionniste ; en revanche, on peut toujours dire je veux montrer que P est faux : supposons par l'absurde que P soit vrai <…>, j'arrive à une contradiction, c'est-à-dire que P est faux, parce que P est faux signifie précisément que la vérité de P est absurde). Faire des maths sans le tiers exclu peut ressembler à un exercice aussi futile qu'essayer de boxer avec les deux mains attachées derrière le dos, et dans une certaine mesure ça y ressemble effectivement, mais cela présente néanmoins un certain intérêt : non seulement c'est intéressant du point de vue de la pure logique de se demander ce qu'on peut faire sans cet axiome (et cette question a des connexions inattendue avec toutes sortes d'autres parties des mathématiques) ; mais par ailleurs, une démonstration en logique intuitionniste apporte véritablement plus de contenu qu'une démonstration classique : pour commencer, elle est valable de façon plus large (et notamment dans les topoï [pluriel de topos]), mais aussi, elle est constructive (au moins si on part de certains axiomes), c'est-à-dire qu'elle exhibe les objets dont elle affirme l'existence.

Une des idées centrales des maths constructives (qui sont à peu près, quoique pas forcément exactement, la même chose que les mathématiques exercées dans le cadre de la logique intuitionniste) est que si on veut prouver P ou Q (en symboles, P∨Q), il devrait être suffisant mais aussi nécessaire de prouver soit P, soit Q (et notamment, de savoir lequel des deux est vrai !) : ceci va manifestement complètement à l'encontre du tiers exclu qui postule que pour tout énoncé P, soit P est vrai soit ¬P l'est, sans qu'on puisse forcément trancher lequel (et parfois, effectivement, on ne peut prouver ni l'un ni l'autre). De même, si on veut prouver il existe un x tel que P(x) (en symboles, ∃x.P(x)), il devrait être suffisant mais aussi nécessaire d'exhiber un x pour lequel on peut prouver P(x) : de nouveau, ceci va à l'encontre des raisonnements par l'absurde qui ressemblent à supposons qu'aucun tel x n'existe <…>, j'arrive à une contradiction, donc un tel x doit exister (mais au final ne donnent aucune information pour en construire un).

Ajout (2019-04-15T23:37+02:00) : Juste après avoir publié cette entrée je me rends compte que j'ai oublié d'insérer un paragraphe que je comptais écrire sur l'interprétation de Brouwer-Heyting-Kolmogorov qui tente d'expliquer au moins informellement le sens des connecteurs de la logique intuitionniste. Spécifiquement, il s'agit de variations autour des explications suivantes :

• une preuve de P∧Q (conjonction) est un couple formé d'une preuve de P et d'une de Q,
• une preuve de P∨Q (disjonction) est la donnée d'une preuve de P ou d'une preuve de Q (avec, bien sûr, l'information de laquelle des deux),
• une preuve de P⇒Q (implication) est une manière de transformer une preuve de P en une preuve de Q,
• une preuve de ⊤ (le vrai) est triviale,
• une preuve de ⊥ (le faux) n'existe pas,
• une preuve de ∀x.P(x) est une manière de transformer un x en une preuve de P(x),
• une preuve de ∃x.P(x) est la donnée d'un t particulier et d'une preuve de P(t).

Je répète que, telles quelles, ces explications n'ont pas vraiment de sens (notamment à cause des mots manière de transformer), et d'ailleurs il en existe beaucoup de variations (Kolmogorov parlait de problèmes et de solutions de ces problèmes plutôt que de preuves d'énoncés ; c'est d'ailleurs ce qui motive la logique de Medvedev dont je parlerai plus bas). Mais elles servent au moins à motiver la manière dont on veut que la logique intuitionniste se comporte, et ce sont des formalisations de ces idées qui conduisent à la réalisabilité de Kleene (ce dernier essayait de rendre précise l'interprétation de Brouwer-Heyting-Kolmogorov) et la logique de Medvedev (cf. plus loin).

★

Je ne suis pas historien des maths et pas spécialement compétent pour en parler, et par ailleurs l'article Wikipédia sur la controverse Hilbert-Brouwer me semble bizarrement écrit et lui-même sujet à controverse ; donc je ne tenterai pas sérieusement de faire l'histoire du sujet. Ce que L. E. J. Brouwer, inventeur de l'intuitionnisme, appelait intuitionnisme, n'est pas vraiment ce que les matheux actuels appellent ainsi (notamment parce que je crois comprendre que Brouwer avait une grande méfiance de la logique, et plus encore de la logique formelle, alors que maintenant — depuis Gödel, il me semble — on considère tout ce sujet à la lumière de la logique), mais le tiers exclu est assurément un point central d'achoppement entre Brouwer, qui le rejetait pour son caractère non-constructif, et Hilbert, qui l'acceptait comme une évidence de l'orthodoxie logique. Ironiquement, la controverse est partiellement due à deux théorèmes d'existence non-constructifs dus à Hilbert et Brouwer eux-mêmes, à savoir le théorème de la base de Hilbert (dont la recherche d'une démonstration constructive a cependant mené indirectement à la théorie des bases de Gröbner) et le théorème du point fixe de Brouwer.

Mais pour donner peut-être une saveur de [hum, comment on dit a taste of en français, déjà ?] choses qui pouvaient déranger Brouwer, je peux proposer l'exemple de raisonnement suivant, qui me semble intéressant parce qu'un de mes collègues, pourtant informatheux expérimenté, a été vraiment dérangé par cet argument avant de concéder qu'il était valable :

Contexte : On ignore, actuellement, essentiellement tout sur l'écriture décimale de π (à part qu'elle n'est pas ultimement périodique puisque π n'est pas rationnel). On ne sait, notamment, pas prouver que chaque chiffre ou à plus forte raison chaque suite finie de chiffres, y apparaît infiniment souvent, et on ne sait même pas le prouver pour un chiffre ou une suite finie particulière de chiffres. On conjecture cependant que les décimales de π se comportent, pour ce genre de choses, essentiellement comme si elles étaient tirées au hasard, c'est-à-dire que chaque suite finie de longueur r apparaît en moyenne une fois toutes les 10^r décimales (et notamment, infiniment souvent). Je ne fais aucune hypothèse particulière sur les décimales de π dans ce qui suit (et vous pouvez le remplacer par le nombre réel calculable de votre choix).

Affirmation : Il existe un programme qui, donné un entier k en entrée, termine toujours en temps fini et renvoie soit l'emplacement de la première occurrence de k fois consécutivement le chiffre 7 dans l'écriture décimale de π, soit faux (ou ∞ si on préfère) si une telle occurrence n'existe pas.

Preuve : Soit f: ℕ → ℕ∪{∞} la fonction qui à k associe l'emplacement de la première occurrence de k chiffres 7 consécutifs dans l'écriture décimale de π, ou bien ∞ si cette occurrence n'existe pas. Il s'agit de montrer que cette fonction f est calculable algorithmiquement. De deux choses l'une : soit il existe k₀ tel que f(k)=∞ pour k≥k₀ (i.e., k₀−1 est la longueur de la plus grande suite de 7 consécutifs dans π) ; soit f(k)<∞ pour tout k. Dans le premier cas, la fonction f est calculable algorithmiquement par un programme puisqu'elle est constante à partir d'un certain rang (le programme peut renvoyer ∞ pour k≥k₀ et faire un nombre fini de cas pour toutes les valeurs inférieures) ; dans le second cas, il existe des suites de 7 consécutifs arbitrairement longues, et f est calculable par le programme qui calcule toutes les décimales successivement jusqu'à trouver une telle suite de longueur assez grande.

Commentaire : Ce qui rend ce raisonnement gênant est que beaucoup de gens (dont le collègue évoqué ci-dessus) vont rétorquer oui, mais on ne sait pas calculer k₀, ni même s'il existe ! — pourtant, ce raisonnement, qui ferait sans doute frémir d'horreur Brouwer, est classiquement correct, c'est-à-dire correct dans la théorie de la calculabilité enseignée dans le cadre des mathématiques usuelles (classiques, orthodoxes, comme vous voudrez l'appeler). Le problème est que je montre que quelque chose est calculable (qu'un programme pour le calculer existe) sans exhiber un tel programme : quelle que soit la valeur de k₀ (ou si k₀ n'existe pas), un tel programme existe, mais moi je ne sais pas ce qu'il est. Seulement, classiquement, f est calculable signifie qu'un programme calculant f existe, pas que je suis capable de l'exhiber. (Bon, on peut quand même se mettre d'accord que la convention usuelle de langage, en l'absence d'éclaircissement par ailleurs, quand on dit f est calculable est qu'en fait non seulement f est calculable mais qu'on s'apprête à en exhiber un algorithme explicite ; mais c'est déjà une forme de constructivisme.)

★

Maintenant, faire des maths en logique intuitionniste ressemble effectivement un peu à faire de la boxe sans utiliser ses poings (la comparaison est de Hilbert) : un matheux habitué aux maths classiques sera horrifié de ne pas avoir le droit de dire que, si x est un réel, on a soit x>0 soit x<0 soit x=0 ; ou qu'une partie d'un ensemble fini est finie ; ou que l'image d'un ensemble fini est finie ; ou toutes sortes de choses de ce genre. Pourtant, on peut quand même faire beaucoup de maths, et de façon même pas si différente de ce dont on a l'habitude : c'est quelque chose qu'E. Bishop et ses disciples ont montré (constructivement !).

À part l'aspect scientifique proprement dit, je suis tenté de trouver que ça a un réel intérêt pédagogique (voire métapédagogique, i.e., pour enseigner la pédagogie) : en obligeant à se rendre compte de la manière dont on utilise le tiers exclu (et à chercher à l'éviter), cela amène à réfléchir à la manière dont on construit des raisonnements mathématiques (et dont toutes sortes de faits « évidents » comme si tous les éléments d'un ensemble sont égaux alors il existe un élément auquel ils sont tous égaux sont démontrés) ; cela peut aussi amener le mathématicien classique, en le plaçant sur un terrain non familier et glissant pour lui, à reréfléchir à ce qu'il trouve évident, et peut-être à mieux comprendre les étudiants et autres débutants en mathématiques en comprenant leurs difficultés. Je pense d'ailleurs un peu la même chose du fait de s'obliger à repérer ou à éviter l'usage de l'axiome du choix (cf. d'ailleurs cette question sur la comparaison entre les deux) ou d'autres axiomes de la théorie des ensembles (Remplacement me vient à l'esprit).

En fait, ce qui est peut-être remarquable, c'est qu'on s'habitue relativement vite à raisonner en logique intuitionniste, et notamment, que même les matheux qui ne connaissent pas la logique formelle comprennent ce que cela signifie que de s'interdire le tiers exclu (alors qu'on pourrait se dire a priori que cela dépend du mécanisme mental précis qu'ils ont en tête pour représenter la logique classique).

(Cf. aussi cette entrée passée qui a un rapport avec le sujet.)

★

★

★

L'intuitionnisme et les mathématiques constructives intéressent aussi l'informatique et les informaticiens, notamment par le biais d'un dictionnaire appelé la correspondance [ou l'isomorphisme] de Curry-Howard ou la correspondance preuves-programmes, qui fait correspondre, dans des conditions qu'il n'est pas ici lieu d'expliciter plus précisément, les preuves mathématiques et les théorèmes démontrés par ces preuves, avec des programmes (termes serait sans doute plus exacts) dans des langages de programmations fonctionnels fortement typés et les types de ces termes. (Une façon de définir la correspondance serait, dans les règles de démonstration que j'ai énumérées ci-dessus, de dire à chaque fois à quoi elles correspondent au niveau de la construction de termes, où Γ⊢P va correspondre à un terme de type P ayant des variables libres de types Γ ; par exemple, la coupure correspond à la substitution d'un terme dans un autre, l'identité à l'utilisation d'une variable libre, l'élimination du ⇒ à l'application d'une fonction à un terme et l'introduction du ⇒, au contraire, à la création d'une fonction par lambda-abstraction. À titre d'exemple, le terme S := λx.λy.λz.(xz)(yz), c'est-à-dire la fonction qui prend en entrée trois variables x, y, z et renvoie le résultat de l'application de x à z appliqué au résultat de l'application de y à z, a pour type (p→q→r)→(p→q)→p→r en notant u→v le type des fonctions prenant en entrée le type u et en sortie le type v, où p→q→r serait le type de x, p→q celui de y et p celui de z ; et il correspond par l'isomorphisme de Curry-Howard à la preuve de la tautologie (p⇒q⇒r)⇒(p⇒q)⇒p⇒r consistant à dire : supposons (x) que p⇒q⇒r soit vrai et (y) que p⇒q le soit et (z) que p le soit ; alors d'après (x) et (z), on voit que q⇒r est vrai, et par ailleurs d'après (y) et (z) que q l'est, donc finalement r est vrai comme annoncé.) La correspondance de Curry-Howard est assez naturellement intuitionniste en ce sens que les preuves dont il est question sont des preuves en logique intuitionniste ; et c'est plus ou moins cette correspondance qui assure que la logique intuitionniste est constructive au sens où d'une preuve on peut (dans certaines conditions) extraire un programme calculant l'objet dont elle affirme l'existence.

Ajout : je renvoie à ce billet ultérieur pour une explication de la correspondance de Curry-Howard que j'espère meilleure que le paragraphe bordélique ci-dessus.

☆ Il faut néanmoins nuancer tout ça par le fait que la loi de Peirce, c'est-à-dire la tautologie de la logique classique ((p⇒q)⇒p)⇒p essentiellement équivalente à la règle du tiers exclu, correspond au type ((p→q)→p)→p de la fonction classique call/cc de langages tels que Scheme ou SML/NJ (sur laquelle j'avais commencé à écrire une page il y a une éternité, qui n'a jamais été finie ; mais je remarque au passage que je suis mentionné dans la page Wikipédia sur le call/cc). Bref, l'usage du call/cc correspond à peu près, par rapport à un langage de programmation qui ne l'a pas, à l'usage du tiers exclu (enfin, de la loi de Peirce) par rapport à la logique intuitionniste. (Et donc on se dit que sans doute, d'une preuve en logique classique on doit pouvoir extraire des programmes utilisant le call/cc qui est, après tout, tout à fait implémentable — il faudrait creuser pour voir exactement ce qui vaut et ne vaut pas.)

Ajout/digression (2019-04-16T11:22+02:00) : Décrivons cependant brièvement à quoi peut ressembler un terme de type p∨¬p écrit en utilisant le call/cc. Autrement dit, il s'agit, de renvoyer un type union entre un type p (quelconque, donné, sur lequel on ne sait rien) et le type p→⊥ des fonctions prenant un p en entrée et renvoyant quelque chose qui n'existe pas : on est donc censé renvoyer soit l'un soit l'autre (en précisant lequel). Voici ce que fait le programme : il renvoie (dans le type union) une fonction de type p→⊥ qui se comporte de la façon suivante : si on lui passe un objet de type p (auquel cas il est censé renvoyer quelque chose d'impossible !), il « change d'avis », revient en arrière dans le temps (enfin, dans la pile d'appels) en utilisant la continuation qu'il avait soigneusement sauvegardée au moyen du call/cc, et renvoie plutôt (dans le type union) l'objet de type p qu'on lui a passé. Ceci satisfait la promesse annoncée : on fournit un objet de type p→⊥ jusqu'à ce qu'un objet de type p se manifeste, auquel cas on fournit un objet de type p ; mais on peut se dire que ce programme a manifestement triché ! En quelque sorte, je suis tenté de dire que le problème en présence du call/cc est que les types union peuvent changer d'avis sur ce qu'ils font par l'invocation d'une continuation plus tard dans le programme.

★

Bref, je voudrais écrire quelque chose sur l'intuitionnisme, mais je ne sais pas par quel bout le prendre, et j'ai peut-être trop de choses à dire.

Une possibilité serait de commencer par parler du seul calcul propositionnel, c'est-à-dire sans quantificateurs, juste avec les connecteurs logiques ⇒ (implication), ∧ (conjonction), ∨ (disjonction), ¬ (négation, mais ¬P est juste une abréviation de P⇒⊥), ⊤ (vrai) et ⊥ (faux), un peu comme j'ai parlé de logique linéaire il n'y a pas si longtemps, et avec laquelle je pourrais essayer de faire le lien. La logique intuitionniste est intéressante même au niveau du simple calcul propositionnel (alors que la logique classique ne l'est franchement pas trop : il s'agit juste de faire des tables de vérité pour décider ce qui est tautologique ou pas), et il y a déjà énormément à en dire. Par exemple, juste avec une variable, on peut fabriquer une infinité d'énoncés différents et non équivalents entre eux (on parle du treillis de Rieger-Nishimura ; pour comparaison, en logique classique on ne peut en faire que quatre, ⊥, p, ¬p et ⊤ ; cf. aussi cette question MathOverflow et la belle réponse que j'a reçue). Il y a une structure algébrique qui est l'équivalent pour la logique intuitionniste de ce que sont les algèbres de Boole pour la logique classique, à savoir les algèbres de Heyting. On peut y penser comme les ouverts d'un espace topologique (enfin, si on sait ce que ça veut dire) : si sur un espace topologique X on définit les opérations entre ouverts de X que sont l'intersection (notée A∩B ou A∧B) et la réunion (notée A∪B ou A∨B) mais surtout en notant A⇒B pour l'intérieur Int(B∪(X∖A)) de la réunion B∪(X∖A) de B et du complémentaire de A (et notamment ¬A pour Int(X∖A), complémentaire de l'adhérence de A, également appelé pseudocomplémentaire de A), et si on interprète ⊥ comme X tout entier et ⊤ comme ∅ (le vide), alors les ouverts de X forment une algèbre de Heyting (par ailleurs complète ; ceci est à mettre en parallèle avec le fait que les ouverts réguliers, de X forment une algèbre de Boole complète, les opérations étant un petit peu différentes de celles que j'ai définies) ; et un formule propositionnelle est démontrable dans la logique intuitionniste si et seulement si elle donne l'ouvert plein dans n'importe quel espace topologique (c'est le cas, par exemple, de p⇒p, mais pas de p∨¬p). Une autre façon d'interpréter (i.e., donner une sémantique à) la logique intuitionniste passe par les modèles de Kripke, et fait le lien avec la logique modale.

Rien que le sujet du calcul propositionnel est, en logique intuitionniste, déjà fort intéressant. Il y a quantité de formules propositionnelles qui sont démontrables en logique classique, pas en logique intuitionniste, mais qui sont néanmoins valides dans telle ou telle sémantique particulière de la logique intuitionniste, par exemple certains espaces topologiques (ou certains topoï), ou par exemple dans le cadre de la réalisabilité de Kleene (ou, ce qui revient au même, dans le topos effectif), ou encore dans le cadre de la « logique de Medvedev » dont je dois aussi dire un mot. Par exemple l'axiome de Scott ((¬¬p⇒p) ⇒ (p∨¬p)) ⇒ (¬¬p∨¬p) ou bien l'axiome de Kreisel-Putnam (¬p⇒(q₁∨q₂)) ⇒ ((¬p⇒q₁) ∨ (¬p⇒q₂)), dont le sens intuitif n'est pas du tout évident à imaginer, pas plus que la signification sur un espace topologique (voir ici au sujet du premier, là pour le second), qui ne sont, en l'occurrence, pas valides dans la réalisabilité de Kleene mais le sont dans la logique de Medvedev (voir aussi cette réponse MathOverflow) ; la formule de Ceitin (¬(p₁∧p₂) ∧ (¬p₁⇒(q₁∨q₂)) ∧ (¬p₂⇒(q₁∨q₂))) ⇒ ((¬p₁⇒q₁) ∨ (¬p₁⇒q₂) ∨ (¬p₂⇒q₁) ∨ (¬p₂⇒q₂)) qui est valide dans la réalisabilité de Kleene et dans la logique de Medvedev mais n'est quand même pas un théorème de la pure logique intuitionniste ; ou encore l'étrange formule ((¬¬p₁⇔(¬p₂∧¬p₃)) ∧ (¬¬p₂⇔(¬p₃∧¬p₁)) ∧ (¬¬p₃⇔(¬p₁∧¬p₂)) ∧ ((¬p₁⇒(¬p₂∨¬p₃)) ⇒ (¬p₂∨¬p₃)) ∧ ((¬p₂⇒(¬p₃∨¬p₁)) ⇒ (¬p₃∨¬p₁)) ∧ ((¬p₃⇒(¬p₁∨¬p₂)) ⇒ (¬p₁∨¬p₂))) ⇒ (¬p₁ ∨ ¬p₂ ∨ ¬p₃) qui, elle, est valide dans la réalisabilité de Kleene mais pas dans la logique de Medvedev (enfin, il paraît — franchement, je n'y vois rien). J'aimerais me faire une idée intuitive de ce que ces formules « signifient » mais je reste face à elles comme une poule face à un couteau. [Ajout : cette entrée ultérieure sur la réalisabilité propositionnelle tente de répondre à ces questions.] Je crois cependant comprendre que je ne suis pas le seul et que c'est un sujet sur lequel « on » ne sait vraiment pas dire grand-chose. Tout le sujet des logiques intermédiaires (entre les logiques classique et intuitionniste) est miné de problèmes ouverts.

★

La définition de la logique de Medvedev est assez jolie et simple pour mériter ici une mention rapide en un paragraphe. On appellera problème fini un couple (X,S) où X≠∅ est un ensemble fini non vide appelé l'ensemble des candidats du problème et S⊆X en est une partie appelée ensemble des solutions du problème. On définit les connecteurs logiques entre problèmes finis de la façon suivante : (X,S)∧(Y,T) := (X×Y, S×T) (i.e., les candidats et les solutions d'une conjonction sont juste les couples des objets correspondants des deux problèmes) ; (X,S)∨(Y,T) := (X⊎Y, S⊎T) où X⊎Y := (X×{0})∪(Y×{1}) dénote la réunion rendue disjointe (i.e., les candidats et les solutions d'une disjonction sont juste les objets correspondants de l'un ou l'autre des deux problèmes) ; et (X,S)⇒(Y,T) := (Y^X, U) où Y^X est l'ensemble des fonctions X→Y et U est la partie formée des f∈Y^X telles que f(s)∈T pour tout s∈S (autrement dit, les candidats et les solutions d'une implication sont respectivement les fonctions entre candidats et celles qui transforment une solution de l'un en solution de l'autre) ; enfin, ⊥ est défini comme ({*},∅) et ⊤ comme ({*},{*}), ce qui permet d'identifier ¬(X,S) comme ({*},{*:S=∅}) et ¬¬(X,S) comme ({*},{*:S≠∅}). Bref. Une formule propositionnelle, faisant intervenir des variables p₁,…,p_k est dite valide dans la logique de Medvedev lorsque pour tous ensembles X₁,…,X_k non vides il existe un s (ne dépendant que de X₁,…,X_k) tel que quels que soient S_i⊆X_i l'élément s soit solution du problème obtenu en substituant (X_i,S_i) à la place de p_i dans la formule. Autrement dit, il s'agit des formules décrivant des problèmes qu'on peut résoudre uniformément quels que soient les problèmes qu'on injecte dedans (uniformément au sens des ensembles S_i de solutions). Par exemple, la formule p⇒p est validé en prenant pour s l'identité dans X^X, mais la formule p∨¬p n'est pas valide dans la logique de Medvedev car on ne peut pas trouver un élément de X⊎{*} qui appartienne à toute partie S non vide de X et soit en même temps égal à * si S=∅. Les formules valides de la logique de Medvedev incluent tout ce qui est démontrable dans le calcul propositionnel intuitionniste et sont incluses dans celles qui sont démontrables en logique classique, mais ces deux inclusions sont strictes (et les axiomes de Scott et de Kreisel-Putnam évoqués plus haut donnent des exemples de formules Medvedev-valides mais non démontrables intuitionnistement). Malgré sa définition très simple, on sait finalement très peu de choses sur la logique de Medvedev. Notons que la réalisabilité de Kleene est assez analogue, en fait, à la logique de Medvedev mais en remplaçant les ensembles finis par des parties de ℕ et les fonctions par des fonctions calculables. [Ajout : encore une fois, voir cette entrée ultérieure pour une description de la réalisabilité de Kleene, celle-ci pour la réalisabilité propositionnelle, et celle-ci sur le topos effectif.]

★

Il y a ensuite aussi énormément de choses à dire en dépassant le calcul propositionnel et en allant chercher la logique du premier ordre, voire d'ordre supérieur. On peut formuler tout un tas de principes valables en mathématiques classiques mais pas en mathématiques constructives (à titre d'exemple, le principe de Markov (∀n.(P(n)∨¬P(n)) ∧ ¬∀n.¬(P(n))) ⇒ ∃n.(P(n)) qui affirme que si α:ℕ→{0,1} est une suite binaire, dont tous les termes ne valent pas 0 alors elle a un terme qui vaut 1 ; celui-ci est classiquement valide et aussi validé par la réalisabilité de Kleene mais pas validé par les mathématiques constructives les plus générales), et chercher les implications entre elles : ceci donne naissance à une théorie des mathématiques à rebours mais (partiellement !) constructives : voir ce texte pour en savoir plus.

★

Bon, cette entrée est déjà beaucoup trop longue alors que je n'ai rien dit sauf parler de ce que je voudrais dire, donc je vais m'arrêter là un peu en queue de poisson : ça manque de conclusion mais je ne sais pas quoi y mettre, et il vaut mieux que je publie maintenant que laisser ce texte moisir dans mes cartons comme ça arrivera inévitablement si je me dis que je veux l'améliorer. (En plus, mon poussinet a allumé la télé qui parle en boucle de l'incendie de Notre-Dame, ça m'empêche de réfléchir.)