*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.
L’utilisation compulsive des écrans n’est elle pas plutôt un symptôme de mal être qu’il conviendrait de déceler et éventuellement de…
@un lecteur N’est-ce pas justement cette simplicité et transparence de la personnalité de TRUMP qui en fait son attrait, ces…
ON Y EST ! https://www.huffingtonpost.fr/international/article/israel-frappe-l-iran-ce-que-l-on-sait-des-frappes-sur-des-sites-militaires-et-nucleaires_251298.html https://www.huffingtonpost.fr/international/video/aux-etats-unis-ce-senateur-democrate-expulse-de-force-d-une-conference-de-presse-du-gouvernement-trump_251293.html
Cher Pierre-Yves, Emmanuel Macron a été élu grâce à l’influence de quelques entreprises parmi les 6000 GE et ETI qui…
Depuis la numérotation, quand je recharge la page d’accueil, les 10 commentaires les plus récents apparaissent tantôt à droite comme…
Il faut remplacer une addiction par une autre. C’est parfois ainsi que cela se passe. L’addiction aux écrans est aussi…
alvin, https://www.slate.fr/story/79512/guerre-mondes-welles-panique J’avais vu il y a quelques années cette « légende urbaine » reprise par Arte (à qui se fier !).…
Pierre-Yves, Interdire les RS au moins de 15 ans, d’accord, ça fera pas de mal, le temps que les gamins…
Comment appelle-t-on déjà un état qui arrête un sénateur d’opposition, le brutalise et le menotte, uniquement parce qu’il souhaitait poser…
Y’a peut être des parts de marché à prendre dans le secteur « économique » de la vérité peu valorisé par Publicis…
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 »
Laisser un commentaire