Et si le programme de Hilbert tenait toujours ?
(Et si Gödel, Church, Turing, Kleene avaient été de mauvaise foi ?)
Partager :
11 réflexions sur « Vidéo – P vs NP – Deuxième épisode »
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 !
(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.)
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.
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 :
https://www.jesuismort.com/tombe/david-hilbert#citation
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):
http://r6.ca/Goedel/goedel1.html
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.