Comments on (Nouvelle tentative d')introduction aux mathématiques constructives : histoire, motivations et principes

Ruxor (2022-11-24T14:14:15Z)

Je viens faire une correction à cette entrée pour signaler que chacun de ‘∧’ et ‘∨’ est distributif sur l'autre : j'avais prétendu qu'il n'y avait distributivité que de ‘∧’ sur ‘∨’, en fait ça marche dans les deux sens (comme en logique classique, donc), mais j'ai agité les mains pour expliquer qu'il peut quand même y avoir une raison de trouver la distributivité de ‘∧’ sur ‘∨’ plus fondamentale, plus intuitive ou « meilleure » que celle de ‘∨’ sur ‘∧’.

ln (2022-10-30T20:47:48Z)

Une utilisation des maths intuitionnistes en physique : <URL: https://www.unige.ch/lejournal/evenements/automne-2021/les-3-erreurs-deinstein/ >

Esthé (2022-09-26T13:25:48Z)

Tu parles des mathématiques à rebours. Il y a d'autres contextes que la logique ou la recherche où les maths à rebours sont naturelles, c'est en enseignement. Là, la question n'est pas celle du socle logique minimal (la longueur des démos étant non bornée) mais celle de la façon la plus rapide où la plus pédagogique d'atteindre, à partir de ce qu'ils savent, les objectifs fixés par le programme.

Ou dans les leçons d'agrég, "Blabla, exemples et applications". Pour traiter tels exemples, quels sont les théorèmes vraiment utilisés ? D'ailleurs, en agrég, il y a souvent le sens direct et le sens rebours simultanément en tête, dans la conception de leçon. Ce qu'on veut vraiment, c'est couvrir tels théorèmes. Mais le jury veut qu'on justifie cette démarche théoricienne d'une façon qui peut convaincre un sceptique, c'est-à-dire dans une démarche appliquée. Donc on cherche des applications à nos théorèmes pour après coup prétendre que ces applications étaient nos motivations.

Dans ton image mentale des maths comme un arbre, procéder à rebours revient ici à élaguer toutes les parties qui n'aboutissent pas à nos fruits, à prendre le sous-arbre minimal contenant le sol (les axiomes) et les fruits escomptés.

Je ne me prononce pas sur la qualité de cette démarche en enseignement. Elle a pour elle l'avantage de l'efficacité, en un certain sens. Mais pas en tous les sens : si on se donne une liste de 100 problèmes, pour chacun des problèmes isolés, il est plus court de le résoudre de façon ad hoc, mais si on veut tous les résoudre, il est préférable de les faire tenir dans un édifice théorique qui donne de la hauteur. De plus, elle est efficace si on tient à aborder l'enseignement sous l'angle "atteindre tel horizon le plus rapidement possible", alors qu'on pourrait préférer le faire de la façon la plus profonde possible, en ayant la main leste sur le temps investi (passer plus de temps à faire un truc chouette n'est pas un coût mais du temps de qualité). On peut également être mal à l'aise avec l'idée d'aborder l'enseignement comme un vrai problème d'optimisation.

Désolé, j'ai conscience que le rapport avec l'entrée n'est pas tout à fait direct.

Vicnent (2022-06-29T12:45:45Z)

franchement, c'est plutôt bien écrit. J'avais des notions assez vague de tout ça et une seule lecture m'a permis de bien restructurer le tout. Merci.
Le fait de mettre en juxtaposition des "introduction en gros du concept" + du formalisme + des exemples, y compris aux bords pour montrer les différences et subtilités est très pédagogique.

mbow (2022-06-28T11:53:47Z)

Les topos font vraiment envie (la sémantique a l'air très riche) mais il faut être bien l'aise avec le langage catégorique et les manipulations de diagrammes. Tout le monde n'y arrive pas…

Ruxor (2022-06-25T15:42:27Z)

@f3et: Je ne suis pas sûr de comprendre la question, mais bon, je ne suis pas non plus sûr de comprendre le rapport philosophique précis entre finitisme et constructivisme, ni d'ailleurs, pour prendre une troisième direction possiblement apparentée, prédicativisme. Disons juste que, formellement, de ce que je comprends, le finitisme (et ses avatars, dont le prédicativisme est peut-être une forme faible) consiste à restreindre le principe de récurrence et/ou le principe de compréhension (en arithmétique du second ordre), tandis que le constructivisme consiste à restreindre la loi du tiers exclu. A priori c'est orthogonal, mais il se peut qu'il y ait des conséquences communes.

@glandu:

Pour commencer, il faut se demander ce que « fini » veut dire (on peut distinguer un ensemble S « fini », ce qui signifie qu'il y a un entier naturel n et une bijection {0,…,n−1}→S, autrement dit, on peut énumérer les éléments de S par les n premiers entiers naturels, de façon injective c'est-à-dire sans répétition, — et « finiment énuméré », ce qui signifie qu'il y a un entier naturel n et une surjection {0,…,n−1}→S, autrement dit, on peut énumérer les éléments de S par les n premiers entiers naturels, sans imposer l'injectivité).

Mais en tout état de cause, on ne peut pas affirmer qu'un sous-ensemble d'un singleton est forcément fini, ou même finiment énuméré. En effet, si p est une proposition (une valeur de vérité) et si S := {★ | p} est le sous-ensemble du singleton T := {★} formé des éléments tels que p soit vrai (i.e., de l'unique élément ★ si p est vrai), alors T est indiscutablement fini, mais si S est fini, il est soit vide (n=0), auquel cas on a ¬p, soit a un élément (n≥1), auquel cas on a p : on a donc p∨¬p : donc l'affirmation « tout sous-ensemble d'un singleton est fini » ou toute variante en remplaçant « singleton » par « ensemble fini », « ensemble finiment énuméré » et « fini » par « ensemble fini », « ensemble finiment énuméré », « vide ou un singleton » implique la loi du tiers exclu.

Intuitivement, dire que S est fini demande qu'on puisse compter ses éléments, donc savoir s'il y en a 0 ou 1 (car un entier naturel est soit 0 soit ≥1, y compris en logique intuitionniste) ; et si on prend un élément selon une condition p dont on ne peut pas affirmer la décidabilité, on fabrique un ensemble dont on ne peut pas affirmer la finitude, précisément parce qu'il faudrait décider p pour ça.

glandu (2022-06-25T04:26:10Z)

« [on ne peut] pas dire qu'une partie d'un ensemble fini est finie »

Ça me troue le c… mais au moins peut-on dire qu'elle n'est pas infinie ? ;-)

Ça coince où ? Qu'on ne peut pas exhiber les parties d'un ensemble fini, par exemple, dans le cas de ø ou {x} ?

Dionysos (2022-06-23T21:29:17Z)

Ok merci. Ce qui m'échappait (et continue encore dans une large mesure mais je pense tout simplement qu'il faut connaître les mathématiques "de l'intérieur" pour résorber ce type de limitations), c'est bien le rapport de l'infini et du constructible chez les intuitionnistes que j'ai tendance (faussement) à considérer pour des finitistes.
Sur le "sujet créateur" que tu évoques à un moment, je me rappelle quand je m'intéressais un peu à ça avoir lu quelque part qu'il y avait une forme de kantisme revendiqué chez Brouwer (je crois que c'est en rapport avec la construction du nombre dans l'intuition temporelle) mais ça fait vraiment longtemps que j'ai croisé cette remarque et bien des déformations ont pu se loger. Il y a sans doute un rapport d'une manière ou d'une autre avec "le sujet créateur" qui donne une tonalité fortement kantienne à l'oreille.

f3et (2022-06-23T15:28:47Z)

D'un coup, je me rend compte que les modèles non standard de N ont le même défaut, et pour la même raison : les entiers "infinis" ou plutôt "illimités" sont, et pour cause, non constructibles, les ensembles (ou plutôt les collections) de ces entiers n'ont souvent pas de plus petit élément, etc. De plus, le raisonnement par récurrence ne fonctionne plus exactement pareil (par exemple, la propriété "être standard" est héréditaire et pourtant pas toujours vraie :-)). Bref, y a-t-il un lien plus rigoureux entre les deux concepts, ou est-ce seulement une vague analogie ? Et au point où on en est, que faut-il penser de l'idée selon laquelle des entiers "trop grands" (peut-être pas 10^12, comme le voulaient les ultra-finitistes, mais mettons TREE (3)) n'existent pas ? Ce qui est sûr, c'est qu'on ne peut pas définir une fonction comme TREE dans des axiomatiques trop faibles, mais il ne devrait tout de même pas être possible de construire un truc interdisant complétement l'existence d'un certain entier précis, si ?

Ruxor (2022-06-23T10:13:03Z)

@Dionysos:

Sur ce que pensait Brouwer de son propre théorème, je ne sais pas. Peut-être qu'il l'a désavoué ou même que c'est en réfléchissant sur ce cas précis qu'il a été amené à rejeter les preuves non-constructives, mais ce n'est que spéculation de ma part. Il y a différents moyens de sauver le théorème du point fixe dans le cadre des maths constructives, par exemple en le transformant en un résultat approché, en renforçant ses hypothèses, en affaiblissant sa conclusion (ne serait-ce qu'en ajoutant une double négation, ça doit marcher), mais je ne sais pas ce que Brouwer pensait de tout ça.

La récurrence est bien valable intuitionnistement, sous la forme « si P(0) est vrai et que pour tout n, (si P(n) est vrai alors P(n+1) l'est), alors pour tout n, P(n) est vrai » ou sous la forme d'une construction, « donné f(0) et un moyen de construire f(n+1) à partir de f(n), alors f(n) est construit pour tout n ». (Comme le fait remarquer justement f3et, d'autres formes, notamment « tout ensemble d'entiers naturels qui a un élément a un plus petit élément », classiquement équivalentes, ne sont plus valables.) La récurrence permet de construire des objets infinis, si on veut, mais ce n'est pas un problème pour les constructivistes (qui ne sont pas forcément finitistes ni réciproquement).

Il y a bien sûr toutes sortes de limitations sur ce qu'on peut faire avec les nombres réels : par exemple, il n'est pas valable constructivement qu'une série de nombres rationnels positifs dont les sommes partielles sont bornées est convergente (classiquement, c'est vrai), c'est peut-être à ce genre de choses que tu penses.

f3et (2022-06-23T08:30:44Z)

Je vais peut-être dire une bêtise, mais il me semble que le raisonnement par récurrence classique est constructif, puisque pour toute valeur de n explicite, il fournit une démonstration de P(n), ou une construction de u_n ; seulement les formes équivalentes en logique classique (existence d'un plus petit entier n tel que P(n) s'il en existe, descente infinie, etc.) ne le sont plus en intuitionnisme, et en particulier la preuve par descente de ce qu'il n'y a pas d'entier tel que … n'est plus valide.

Dionysos (2022-06-22T21:06:52Z)

Je n'ai pas compris sur la récurrence : il apparaît qu'il est conservé dans l'arithmétique intuitionniste de Heyting mais ça montre que je ne saisis pas ce que les intuitionnistes signifient par constructivité : n'y a-t-il pas dans un raisonnement entendant montrer que tous les éléments d'une série possède une propriété un passage à la limite où on infère quelque chose sans le construire complètement ?

Dionysos (2022-06-22T20:49:08Z)

Bonjour,
Il y a un point au début de ton entrée qui m'a laissé perplexe : dans l'intervalle de quelques mots, Brouwer est évoqué à la fois comme celui qui se défie d'une démonstration non constructiviste de son objet (ça je savais déjà) et comme celui qui avec son théorème du point fixe y a pourtant eu recours. Est-ce à dire qu'il désavouait sa propre trouvaille sur ce point ?
J'ai réagi sans avoir lu l'ensemble du post, ce que je m'apprête à faire, et notamment pour voir ce qu'il en est du raisonnement par récurrence dans l'intuitionnisme (si tu l'évoques) : je ne sais plus s'il l'accepte ou non (et je ne vois guère comment en le rejetant on n'ampute pas drastiquement le champ des mathématiques).

Dumber (2022-06-19T12:13:04Z)

C'est le genre de synthèse que j'aurais aimé avoir quand j'ai commencé à m'intéresser de loin à la question, en tant qu'informaticien qui joue avec Coq.

On trouve facilement des cours ou des articles qui adoptent un point de vue particulier (logique du premier ordre + diverses théories, lambda cube, systèmes de martin-lof etc…), mais qui n'offre jamais une vue un peu synthétique qui semble faire partie du folklore, notamment dans la communauté Coq.

Ça m'a toujours dérangé avec Coq de ne pas avoir eu de cours qui ne contenait pas une part de folklore et de terminologie pas très bien documenté (il y a 20 ans, donc ça a peut être changé !). De ce point de vue, je trouve que les systèmes de preuve basés sur des logiques du premier ordre (ou d'ordre supérieure) sont conceptuellement plus simples dans le sens où l'on peut facilement définir tous les concepts. Je ne sais toujours pas quelle est la sémantique d'un système logique comme Coq par exemple…

Ruxor (2022-06-18T22:00:24Z)

@YBM: Oui (d'ailleurs, j'ai suivi le cours de logique de J.-L. Krivine à l'ENS en 1996–1997). Mais il n'a pas spécialement travaillé sur les maths constructives, il me semble ; presque au contraire, j'ai envie de dire : il a adapté à la logique classique la réalisabilité de Kleene qui était formulée en logique intuitionniste.

@mandatory: L'énoncé « toute fonction de ℝ vers ℝ est continue » est manifestement faux en logique classique, donc ça ne peut pas être un théorème en logique intuitionniste (car ç'en serait un en logique classique). En revanche, en logique intuitionniste, on peut prendre certains axiomes qui seraient tout simplement contradictoires en logiques classique et qui, en logique intuitionniste, impliquent cet énoncé (et de fait, Brouwer tenait pour vrais certains tels axiomes, notamment le « principe du choix continu »).

mandatory (2022-06-18T20:29:20Z)

Je n'ai lu que le paragraphe introductif, mais cela m'apporte déjà une question : "un théorème en logique intuitionniste est encore un théorème en logique classique" -> Est-ce que "Toute fonction de R dans R est continue." est un théorème en logique intuitionniste ?

YBM (2022-06-18T14:36:39Z)

Très bonne synthèse !

Vous connaissez les travaux de J.-L. Krivine je suppose (https://www.irif.fr/~krivine/) ?