Comments on Encore une tentative pour expliquer Gödel

Ruxor (2019-05-01T11:16:59Z)

@Laurent: Oui, je n'ai jamais spécialement pensé que « l'astuce de Quine » était due à Quine, mais j'aurais pu être plus explicite là-dessus. Le terme est (au moins indirectement) de Hofstadter, qui ne l'attribue pas non plus à Quine mais le nomme en son honneur. C'est une application du principe d'Arnol'd (qui n'est lui-même pas dû à Arnol'd…), que, personnellement, je considère comme pas spécialement problématique : de même que les rues de Paris sont nommées en l'honneur de personnes qui ne sont pas ceux qui les ont creusées, je n'ai pas de problème à nommer des théorèmes ou concepts mathématiques en l'honneur d'autres que ceux qui les ont découverts. 😀

Laurent (2019-05-01T10:19:23Z)

Bonjour,

je peux me tromper, je ne connais pas bien les travaux de Quine, mais il me semble que lui attribuer l'astuce de la construction de la formule de Gödel est erroné. Il se trouve que, venant de donner un cours sur le théorème d'incomplétude, je m'interrogeais justement sur l'origine de cette astuce qui semble vraiment sortie de l'espace (et qui ne représente que la partie la plus spectaculaire mais sans doute pas la plus profonde de la preuve de Gödel) et la lecture de cet article m'a motivé à faire quelques recherches sur wikipedia. Si je puis me permettre de hasarder une chronologie (complètement hypothétique) de la génèse de cette astuce :
- fin XIXe, les prémisses de l'idée viennent bien sûr, mais c'est loin de tout expliquer, de l'argument diagonal de Cantor[1] ;
- début des années 1930, une contribution conceptuelle essentielle est l'invention du lambda-calcul de Church[2] (lui-même inspiré des logiques combinatoires de Schöenfinkel, Curry[3]) qui introduit la possibilité d'appliquer un lambda-terme à un lambda-terme, tout comme la formule de Gödel est construite en appliquant une formule à (le code d') une formule ;
- 1935, le paradoxe de Kleene-Rosser[4] montre l'incohérence du système de Church (en tant que système logique) ; je crois savoir comment est fait ce paradoxe et je pense qu'il a inspiré l'invention du terme de point fixe en lambda-calcul[5] et le théorème de récursion de Kleene en 1938[6], deux résultats qui sont fortement analogues à la construction de la formule de Gödel, j'en déduis donc qu'il a probablement également inspiré ycelui.

Encore une fois je ne connais pas bien les travaux de Quine, apparemment l'idée des programmes "quines"[6] auto-réplicants qui est effectivement dans la même culture logique est bien postérieure au théorème de Gödel, ce qui n'empêche que Quine ayant été actif dès les années 30 a certainement pu interagir directement ou indirectement avec Gödel.

D'autre part pour ceux que ça intéresse, en préparant mon cours j'ai découvert un poly excellent de Alexandre Miquel qui donne une démonstration très complète, détaillée et remarquablement bien rédigée du théorème de Gödel[7].

[1] <URL: https://en.wikipedia.org/wiki/Cantor%27s_diagonal_argument >
[2] <URL: https://en.wikipedia.org/wiki/Lambda_calculus >
[3] <URL: https://en.wikipedia.org/wiki/Combinatory_logic >
[4] <URL: https://en.wikipedia.org/wiki/Kleene%E2%80%93Rosser_paradox >
[5] <URL: https://en.wikipedia.org/wiki/Fixed-point_combinator >
[6] <URL: https://en.wikipedia.org/wiki/Quine_(computing) >
[7] <URL: http://perso.ens-lyon.fr/natacha.portier/enseign/logique/GoedelParAlex.pdf >

JML (2019-04-10T12:32:36Z)

Les théorèmes de Gödel c'est pas comme le vélo : j'y passe quelques heures, je comprends à nouveau très bien, puis comme je ne m'en sers pas, quelques mois ou années plus tard je suis revenu à « zut, comment ça marche et qu'est-ce que ça dit précisément ».
Ton entrée a le mérite de bien démêler les confusions entre les différents niveaux, ça va accélérer le processus pour la prochaine fois :)

Bob (2019-04-10T10:37:29Z)

Excellent, ces clarifications sont très précieuses pour ceux qui, comme moi, s'intéressent à (mais ne sont certainement pas spécialistes de) la logique formelle!