,
9 tweets,
2 min read
Read on Twitter
Si on veut un exemple d'un théorème qui est prouvé sans axiome du choix et qui pourtant n'est pas "constructif", je pense qu'un bon exemple c'est le théorème de Cantor-Bernstein, et on le voit quand on veut l'appliquer.
Et sans surprise, sa non-constructivité vient... du tiers exclu ! L'exemple qui me frappe toujours c'est la bijection entre R et P(N) : c'est très facile de trouver des injections dans les deux sens;
et C-B nous fournit "explicitement" (si, si, regardez la preuve!) une bijection R-> P(N) à partir de ces injections. Pourtant, qui est capable de donner une formule pour cette bijection ? (formule à prendre en un sens un peu large, mais qui par exemple permet de déterminer f(pi))
En tout cas moi je ne connais pas de telle formule, et ça réside dans le fait que C-B nous définit la bijection comme "si x est dans tel truc, alors f(x) = machin; sinon f(x) = bidule", et déterminer si "x est dans tel truc" est essentiellement impossible
dans le cas des injections usuelles R-> P(N) et P(N)-> R (sauf évidemment dans des cas triviaux ou artificiels).
On voit ici l' "argument de la calculabilité" pour l'intuitionnisme : utiliser gratuitement "P ou non P" dans une définition, pour un P dont on ne sait pas déterminer s'il est vrai ou non, c'est s'assurer qu'on ne pourra pas expliciter le résultat de la définition.
C'est le même genre de souci que l'exemple dont je parle au début de mon exposé @sav_pour_tous , ou même dont l'exposé traite (je me fais un peu de pub : seminairespourtous.ens.fr/mpt/1819/expos… )
La morale c'est : même en n'étant pas intuitionniste, si on peut éviter les recours à "P ou non P", on gagne en pouvoir d'explicitation (?) et en calculabilité, et c'est toujours intéressant mathématiquement
(En écrivant ça je me rends compte à quel point l'informatique et ses problématiques ont bouleversé la manière dont on pense aux maths)
