*Godot est mort !*
Et si le programme de Hilbert tenait toujours ?
(Et si Gödel, Church, Turing, Kleene avaient été de mauvaise foi ?)
J’adore quand vous parlez de mathématique, et P vs NP me replonge dans mes cours d’informatique théorique de maîtrise. J’ai malheureusement pas eu un super prof, mais j’ai les bases pour vous comprendre, et ça ma passionne !
A propos de Hilbert :
Medellín, le 14 mars 2021
@Paul Jorion, avec amitiés:
¨So that our suffering and death will not have been in vain¨ (Dirk Struik)
L’homme qui a connu tellement bien tous les acteurs mentionés par vous en personne, Dirk Struik: 102 ans au moment de ce discours:
https://www.c-span.org/video/?77208-1/history-future-socialism
(et ne l’oublions pas les souffrances subies par son frere Anton Struik apres ses souffrances dans la Russie de Ulyanov, les camps Nazis, et un bombardement erroné des Anglais, et cet autre idéaliste, Dirk Schermerhorn, frere de l’héro Willem Schermerhorn, constructeur du métro de Moscou, exécuté par les laches bolsjewistes stalinistes, et réhabilité en 1956 par Khrouchtchev, son ex-collegue pendant la construction du métro de Moscou.)
Dans- ou hors sujet ?
https://www.neozone.org/science/un-scientifique-a-developpe-un-algorithme-qui-peut-prouver-que-le-monde-est-une-simulation/
Et le lien direct en fin d’article vers la vidéo intitulée » Sommes-nous des simulations ? » :
https://youtu.be/AtTTn7KMIys
Montrer que le devenir est déterministe ne prouve pas qu’on soit dans une simulation, cela pourrait simplement mettre en évidence que la loi du devenir soit celle d’un automate cellulaire, comme l’ont déjà postulé Konrad Zuse dans les années 1960 et Stephen Wolfram très récemment.
Il existe des preuves mécanisées du théorème de Gödel, c’est à dire complètement formelles et vérifiées par une machine qui n’applique que des règles syntaxiques (cf programme de Hilbert):
Oui bien sûr, mais à la main ou à la machine, la question de la valeur probante ou non de chacune des étapes et des articulations reste entière. Si une étape dit « apparition d’un paradoxe » = « contradiction », je siffle la faute et donne un carton rouge à l’humain ou à la machine ayant commis cette faute impardonnable.
Ce que je veux dire, c’est que la preuve mécanisée citée dans mon message est effectuée en plein accord avec le programme de Hilbert, c’est à dire, qu’il n’y a aucune référence à l’intuition. Bien-sûr, pour accepter cette preuve du théorème de Gödel, vous devez comprendre le langage formel dans lequel le résultat est exprimé et vous convaincre que c’est bien le théorème de Gödel qui est prouvé là. Mais c’est une question qui se pose pour toute formalisation! La suite de symboles veut-elle dire la même chose ce que j’ai en tête. Et ce n’est pas possible d’établir formellement une correspondance entre ce qui est formel et ce qui ne l’est pas.
Une fois ceci dit, je le répète, la preuve se déroule à l’intérieur d’un calcul dont les règles sont strictes et non sujettes à l’interprétation, c’est à dire conformément à ce que voulait Hilbert. La partie du programme de Hilbert qui a échoué est l’automatisation complète: il n’est pas possible de distinguer les théorèmes des non-théorèmes par une procédure générale (sauf pour certaines logiques plus pauvres que l’arithmétique de Peano). Par contre, la logique assistée par ordinateur vient sauver ce programme: il est tout-à-fait possible de distinguer les preuves et les non-preuves automatiquement.
« la preuve mécanisée citée dans mon message est effectuée en plein accord avec le programme de Hilbert, c’est à dire, qu’il n’y a aucune référence à l’intuition. »
Il n’y a pas de référence non plus à l’intuition dans la démonstration par Gödel de son théorème. Mais il y a recours permanent, involontaire et non-maîtrisé à l’intuition dans sa démonstration. Pourquoi ? Parce qu’il s’en fiche, parce qu’il est platonicien : il ne doit pas faire attention à ce qu’il fait (comme le ferait un inventeur) : il est un découvreur de continents pour qui tous les moyens sont bons (cf. Cortés, Pizarro, etc.)
« le programme de Hilbert qui a échoué est l’automatisation complète : il n’est pas possible de distinguer les théorèmes des non-théorèmes par une procédure générale »
Faux : s’il n’est pas possible de distinguer les théorèmes des non-théorèmes par une procédure générale chez Gödel, Church, Turing, Kleene, c’est qu’ils confondent syntaxe et sémantique (dont Hilbert avait donné la recette pour éviter la confusion : distinguer mathématiques et méta-mathématiques), s’autorisent des paradoxes (mis hors-la-loi par Hilbert) en permettant l’auto-référence (déjà bannie par la théorie des types), et assimilent paradoxe (création d’une boucle infinie) à contradiction (affirmer A ET non-A).
Pourquoi croyez-vous que je sous-titre ma vidéo « Et si Gödel, Church, Turing, Kleene avaient été de mauvaise foi ? »
La vérité est le chemin.
Faut pas que le chemin ramène au départ…
(Considérer que c’est la même vérité au début et à la fin du chemin,
c’est prendre le périphérique à Platon-city (un jour sans embouteillage))
« Il n’y a pas de référence non plus à l’intuition dans la démonstration par Gödel de son théorème. Mais il y a recours permanent, involontaire et non-maîtrisé à l’intuition dans sa démonstration. »
A première vue, ces deux phrases me semblent incohérentes entre elles. Si vous voulez dire que sa démonstration n’est pas complètement formalisée, c’est un procès que vous pouvez faire à (presque) tous les mathématiciens. Lire une démonstration complètement formelle n’est pas à la portée d’un humain sauf pour des résultats très simples et encore. Vous ne voulez lire une preuve formelle de a+b=b+a (a,b entiers) dans la théories de ensemble !! Vous ne voulez même écrire complètement la phrase formelle qui exprime ce résultat.
La où je suis d’accord avec vous c’est que le théorème de Gödel est un résultat méta-mathématique. Le langage de l’arithmétique (ou de la théories des ensembles) ne permet pas de parler de preuves: ce ne sont pas des objets de première classe de ces théories car les preuves sont méta-mathématiques dans ces théories. Donc il n’est pas possible d’écrire un résultat mathématique sur les preuves dans ces théories. Ce que fait Gödel et d’autres après lui, c’est qu’il code ces théories à l’intérieur d’elles-mêmes (par des nombres) et le résultat porte sur ces théories encodées.
C’est un raccourci erroné effectivement que de prendre ce résultat méta-mathématique pour un résultat mathématique, car il ne peut pas l’être: le langage de l’arithmétique est trop pauvre. Si vous voulez une mathématique qui parle des preuves aussi bien que de nombres ou d’ensembles, il faut passer à la théorie des types.
« des paradoxes (mis hors-la-loi par Hilbert) »,
« paradoxe (création d’une boucle infinie) . »
« contradiction ((affirmer A ET non-A) ».
Pouvez-vous être plus précis dans votre distinction. Le paradoxe de Russell par exemple est une contradiction (preuve d’une absurdité) dans la théorie naïve des ensembles, qui est une théorie tout à fait formelle comprenant l’axiome de compréhension non restreint. Boucle infinie, ça ne veut pas dire grand chose pour un mathématicien. Vous voulez dire mal-fondé peut-être? Mais je suis d’accord qu’il y a un lien entre boucle infinie et absurdité, en théorie des types.
@Garorock Le dernier billet de Lordon, sur l’union, justement. A méditer, et à savourer pour le style 😉 https://blog.mondediplo.net/l-union-quelle-union
Me semble bien que Tik-tok soit présent en chine. Mais bridé! Contrairement au Pangolin* qui était en roue libre. Y’en…
Si le capitalisme avait tout misé sur les communs, on appellerait « dividendes » le sourire des enfants.
Nous allons dépasser les plus 2° degrés en 2030. Autant dire que les plus réalistes savent depuis longtemps que ça…
» Jésus n’a pas vraiment réussi son coup » Oui mais c’est pas lui qui tenait le marteau. Ce sera…
Avant 2027, il peut y avoir censure, donc dissolution, donc élections. Ce sera interressant, si le NFP n’est pas remis…
@dominique Dupuis Comment se fait-il encore que votre pensée soit si figée et conforme à ceux que finalement les puissants…
Elle tente surtout, me semble t-il, de faire perdurer ce qui avait été construit par tous et très rapidement à…
Et les dernières ‘nouvelles’ de l’avenir des gazaouïs …sans oser extrapoler sur celui de l’ « entité »?/la « nation » palestinienne.. : ((« H…
L’Epiphanie de l’arrêt du conflit Israël-Iran à base de missiles et anti-missile montre que l’on ne fait bien la guerre…
Allemagne Aristote BCE Bourse Brexit capitalisme ChatGPT Chine Coronavirus Covid-19 dette dette publique Donald Trump Emmanuel Macron Espagne Etats-Unis Europe extinction du genre humain FMI France Grands Modèles de Langage Grèce intelligence artificielle interdiction des paris sur les fluctuations de prix Italie Japon Joe Biden John Maynard Keynes Karl Marx LLM pandémie Portugal psychanalyse robotisation Royaume-Uni Russie réchauffement climatique Réfugiés Singularité spéculation Thomas Piketty Ukraine Vladimir Poutine zone euro « Le dernier qui s'en va éteint la lumière »
Répondre à Maxfriend Annuler la réponse