Cet après-midi, au sujet des théorèmes de complétude et d'incomplétude de Gödel (oui, Gödel, qui n'était pas un imbécile, a démontré à la fois la complétude, en thèse, et l'incomplétude, en habilitation) :

DM : Nous sommes d'accord, nous ne remettons pas en cause les maths normales que nous faisons comme d'habitude, la métalogique.

[…]

DM : Cette formule exprime arithmétiquement l'existence d'une preuve de l'absurde dans l'arithmétique de Peano. Mais cette théorie n'est pas absurde, puisque les entiers naturels existent…

un élève, m'interrompant : Mais c'est un acte de foi !

DM : On avait dit qu'on ne remettait pas en cause la métalogique !

Si on remet en cause la métalogique, il n'y a plus de bornes aux limites, comme diraient les Veilleurs.

Plus sérieusement, oui, en effet, sans aller jusqu'à l'acte de foi (d'ailleurs acte de foi se dit auto da fé en portugais, comme quoi il faut être prudent quant à ce que l'on fait pour la foi !), les mathématiques informelles sont un cadre de communication intersubjectif sur lequel il existe une espèce de consensus. Même ceux qui font de la logique intuitionniste (oui, même toi qui me lis avec ProofGeneral dans l'autre fenêtre) ont tendance à parler en mathématiques informelles classiques. Je sais bien que Kronecker (qui n'était pas un imbécile) disait que les entiers naturels avaient été créés par Dieu, mais je ne vois même pas le besoin de croire.

Les mathématiciens souscrivent généralement à l'idéologie que, s'ils en avaient le temps et la volonté, ils pourraient transcrire leurs raisonnements dans la théorie des ensembles axiomatisées par Zermelo et Fraenkel (qui n'étaient pas ses imbéciles) avec l'axiome du choix. En fait, je pense que la plupart s'en fichent et n'affichent cette idéologie que pour se donner une contenance. De toute façon, comme le montrent les travaux de Georges Gonthier (qui n'est pas un imbécile) et al (al est ce mec qui a un h-index de délire), la base fondamentale n'est guère importante : tant que l'on fait des mathématiques normales (hors logique), un codage à base de double négation pour récupérer la logique classique et on passe sans problème en théorie des types d'ordre supérieur. Autrement dit, je ne pense pas que les fondements soient vraiment importants ; je n'ai pas peur de me retrouver comme le coyote des dessins animés, qui avance jusqu'à ce qu'il se rende compte qu'il est dans le vide avec le bip-bip 100 mètres sous lui.

Mais revenons-en aux entiers naturels. Crois-je aux entiers naturels ? Cette question n'a de sens que si on la précise en « crois-je en l'existence d'une classe d'objets ayant les propriétés que nous associons usuellements aux entiers naturels » ? Ma réponse est qu'ai un peu de mal à éprouver quoi que ce soit quant à des nombres du style 10^(10^(10^(10^(10^10)))) (oui, j'ai des tendances ultrafinitistes, malgré les efforts de David Madore pour me convaincre que c'est mal), et de toute façon je me fiche de leur existence : ils font partie des règles du jeu. Ce jeu a diverses conséquences plus ou moins tangibles, par exemple produire des algorithmes utiles (transmissions de vidéos de chat sur Internet, guidage de missiles..) et a divers à-côtés plus ou moins amusants (par exemple la possibilité de mettre une note classante avec moyenne à 12, permettant de sélectionner de futurs directeurs de cabinets ministériels). Je ne vois pas ce que la foi vient faire dedans.

Les entiers naturels, on s'en fiche, au fond, qu'ils existent ou pas. Ça marche très bien de faire comme s'ils existaient, alors continuons comme ça.

Il est temps d'aller lire Bernard Cazeneuve sur Twitter.