J'ai l'impression que toutes ces démonstrations sont avec au moins un infini dans le lot. Je n'ai pas l'impression que c'est indécidable si le tout est fini et discret.
Posté par Ltrlg .
Évalué à 10 (+11/-0).
Dernière modification le 31 octobre 2025 à 18:01.
Si je lis bien, ils ont démontré qu’une simulation algorithmique n’est pas possible pour un modèle donné de notre réalité. Modèle par essence imparfait. Et, dans ces hypothèses hyper-spéculatives de méta-monde, la possibilité d’une simulation non-algorithmique ne peut pas vraiment être écartée (quoi que cela veuille dire). Bon, apparemment ils ne sont pas d’accord sur ce deuxième point (« Any simulation is inherently algorithmic »), mais leur formulation exclue l’usage de systèmes analogues du champ des simulations, ce qui me semble discutable.
Ce qu’ils ont démontré, c’est donc surtout notre incapacité à simuler ledit modèle notre réalité, ce qui est en soi un résultat important, mais aurait probablement fait un moins bon titre ?
Je viens de lire l'article (https://arxiv.org/pdf/2507.22950). Il se trouve que les théorèmes de Gödel font partie des bases de mon propre domaine de recherche (je suis en thèse). Je n'ai pas le temps de développer mais disons simplement que cet article est du vent. Il ne dit strictement rien d'intéressant et ne prouve certainement pas que nous ne vivons pas dans une simulation.
Posté par kantien .
Évalué à 4 (+3/-1).
Dernière modification le 31 octobre 2025 à 23:12.
Quand je vois ce genre de titre, je n'ai même pas envie de lire l'article. Ce n'est pas la première fois, ni la dernière, que l'on fera dire n'importe quoi aux théorèmes de Gödel. Mais même si les physiciens s'y mettent, on n'est pas sorti de l'auberge.
De toute façon, comme je suis kantien, la question n'a même pas de sens pour moi : comme dit le petit enfant boudhiste dans le premier Matrix, « la cuillère n'existe pas ». :-P
Tu fais une thèse en théorie de la démonstration ? ou en calculabilité ? C'est là où j'y vois trois résultats fondamentaux :
théorème de complétude de Gödel
théorème d'incomplétude de Gödel
correspondance de Curry-Howard (logique intuitionniste et classique)
Théorèmes qui ne font que confirmer le cœur de la philosophie kantienne, et l'inexistence de la cuillère.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
« Quand je vois ce genre de titre, je n'ai même pas envie de lire l'article. Ce n'est pas la première fois, ni la dernière, que l'on fera dire n'importe quoi aux théorèmes de Gödel. Mais même si les physiciens s'y mettent, on n'est pas sorti de l'auberge. »
Idem, pas envie de lire un blougui-blouga dénué de tout sens. Le titre seul pourrait quasiment convaincre d'un article écrit par un LLM. Mais après tout, peut-être peut-on trouver des gens assez naïfs pour écrire de telles âneries, et d'autres assez peu scrupuleux pour les publier. Ça a au moins l'intérêt de montrer certaines limites des systèmes de publications.
Juste deux petits exemples pour contextualiser ce jugement à l'emporte pièce sur la seule base du titre :
Dans les années 90, les meilleurs physiciens appliqués, spécialisés en traitement du signal, armés de solides théorèmes mathématiques nous démontraient irréfragablement les limites théoriques en matière de signal transporté sur du câble en cuivre (les fameux xx kbauds). Puis quelqu'un inventa l'ADSL…
Quand on écoute les collègues cosmologistes, ils vous disent qu'il n'est pas exclu que ~95% (estimation au doigt mouillée évidemment) de la nature de l'univers échappe actuellement à notre connaissance — les hypothétiques matières noires et énergies noires. Moi qui ait souvent du mal à résoudre un casse-tête que je puisse connaître entièrement, je conçois mal la niveau d'hubris qu'il faudrait avoir, pour prétendre décider du niveau de connaissance impliqué par le titre à partir de si peu (~5%).
Et n'évoquons même pas la pertinence de la question prétendument résolue…
Juste deux petits exemples pour contextualiser ce jugement à l'emporte pièce sur la seule base du titre
Ce jugement semble ne pas avoir été apprécié par un membre du site, à en juger par ma note.
Dans les années 90, les meilleurs physiciens appliqués, spécialisés en traitement du signal, armés de solides théorèmes mathématiques nous démontraient irréfragablement les limites théoriques en matière de signal transporté sur du câble en cuivre (les fameux xx kbauds). Puis quelqu'un inventa l'ADSL…
À la même époque, d'autres physiciens (Sokal et Bricmont) reprochaient à certains philosophes français leur usage saugrenu de l'incomplétude de Gödel.
Quand on écoute les collègues cosmologistes, ils vous disent qu'il n'est pas exclu que ~95% (estimation au doigt mouillée évidemment) de la nature de l'univers échappe actuellement à notre connaissance — les hypothétiques matières noires et énergies noires. Moi qui ait souvent du mal à résoudre un casse-tête que je puisse connaître entièrement, je conçois mal la niveau d'hubris qu'il faudrait avoir, pour prétendre décider du niveau de connaissance impliqué par le titre à partir de si peu (~5%).
L'un n'empêche pas l'autre. Notre connaissance peut être bornée quant aux contenu du monde (bornée par ce qu'il reste encore à découvrir) mais nous pouvons être en mesure de déterminer les limites du savoir humain (ce que font les méthodes formelles). Kant avait une belle image pour illustrer cela : je peux ignorer le contenu effectif de la surface du globe (il faudrait pour cela en avoir parcouru la totalité) tout en sachant qu'il est circonscrit dans des limites données que je peux déterminer (je n'ai pas besoin de le parcours pour connaître sa circonférence).
Cela étant j'ai fini par lire l'article est je suis moins catégorique que Jeanas sur son contenu : ce n'est pas du Régis Debray. La thèse principale n'est pas tant que nous ne vivons pas dans une simulation, mais qu'une théorie du tout qui unifierait la relativité générale et la physique quantique n'est pas axiomatisable. En résumé : la physique n'est pas axiomatisable. Ce qui a pour corrolaire que l'univers n'est pas une simulation d'ordinateur.
Dans l'ensemble, bien que je souscrives personnellement à ces thèses métaphysiques, leur argumentaire ne me convainc que moyennement. D'une part parce que je doute que la méthode mathématique soit la seule à même de traiter ces questions. D'autre part, parce que l'article consiste à formaliser la thèse de Roger Penrose d'entendement non algorithmique (non algorithmic understanding), thèse qu'il développe par exemple dans son livre Les deux infinis et l'esprit humain. Cette thèse me semblait pas très claire à l'issue de ma lecture du livre, et l'article ne change pas la donne dessus.
Ils font effectivement usage des deux théorèmes de Gödel que j'ai évoqué dans mon premier commentaire. Tout commence à la troisième page de l'article, lorsqu'il suppose une axiomatisation de la physique en supposant l'existence d'un système formel , dont la signification doit vouloir dire : Formalisation of Quantic Gravitation. Il font sur le système des hypothèses raisonnables : logique du premier ordre, ensemble d'axiomes récursivement énumérables, système complet de règles d'inférence. À dire vrai, ces derniers hypothèses n'en sont pas, c'est la définition même de la proposition « la physique est axiomatisable ».
À cela ils ajoutent deux contraintes :
l'arithmétique de Peano est dérivable dans ce système axiomatique ;
tout les phénomènes observables sont prévisibles par la théorie (conséquence du système d'axiomes par les règles de déduction)
On peut bien leur accorder la première, la physique théorique ayant besoin de l'arithmétique. C'est celle-ci qui leur permet de faire usage du théorème d'incomplétude : le système axiomatique étant une extension de l'arithmétique de Péano, il est déductivement incomplet.
Mais ensuite, je dois avouer avoir du mal à les suivre dans leur pensée. Ils semblent jongler entre syntaxe et sémantique : il y aurait des énoncés observables, et donc vrais (théorie de la vérité correspondance, sémantique de Tarski), dans l'univers (cf. deuxième contrainte), mais qui ne seraient pas conséquences déductives du système d'axiomes (que l'on pourrait obtenir à partir des axiomes de l'ensemble Sigma et des règles R). Peut être bien, mais lesquelles ? C'est à partir de là qu'ils introduisent leur méta-théorie non algorithmique, leur entendement non algorithmique à la Penrose et qu'ils me perdent. Non que ce genre de méta-théorie ne soient pas considérées par les logiciens mathématiciens (en théorie des modèles, on étudie bien les modèles non standard de l'arithmétique, des théories non récursivement énumérables voir même non dénombrables), mais je ne comprends pas selon quels principes ils l'introduisent ni la justifient.
Ça a au moins l'intérêt de montrer certaines limites des systèmes de publications.
Cela me rappelle une blague de notre professeur de théorie des modèles, lorsque j'étais étudiant en DEA de logique mathématique et fondements de l'informatique. Il faut faire attention, ici, que le mot modèle est un homonyme de celui utilisé en physique (bien qu'il y ait des rapports entre les deux). Pour un théoricien des modèles, à la question qu'est-ce qu'un groupe ? Il répond : un modèle de la théorie des groupes, c'est à dire une structure qui satisfait à l'axiomatique de la théorie.
Trève de digression et revenons à sa blague. Un jour, en début du cours, il nous tint à peu près ce discours : « je lisais ce matin dans le Monde que la pape Jean Paul II avait sanctifié plus de personnes que tous ces prédécesseurs réunis. Sachant que, durant ces 20 dernières années, on a publié plus d'écrits mathématiques que durant toute la période de l'humanité qui précède, si un jour vous publiez un article insignifiant, vous pourrez vous considérer en bijection avec un sanctifié du pape ! ».
Je dois admettre, après lecture de l'article, que je ne sais quoi dire sur le statut de sanctifiés de ses auteurs.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Posté par mahikeulbody .
Évalué à 3 (+1/-0).
Dernière modification le 02 novembre 2025 à 09:34.
Alors je vais sûrement passer pour l'ignare de service qui s’immisce dans un débat qui le dépasse mais j'assume : c'est comme ça qu'on apprend :-)
une axiomatisation de la physique.
Je ne comprends pas ce point. Naïvement, pour moi, on a deux choses complètement différentes
1) La théorie mathématique (je dirais plutôt "Le système formel"), basée sur des axiomes arbitraires (mais qui doivent avoir certaines caractéristiques pour que la théorie soit intéressante) ; il n'y a rien à prouver (à part les théorèmes issus de la théorie elle-même)
2) La théorie scientifique, basée sur des postulats qui semblent permettre une bonne formalisation du réel (et donc non arbitraires) ; on cherche à prouver vérifier que les résultats fournis mathématiquement par la formalisation de la théorie sont cohérents avec les observations et, ainsi, conforter les postulats.
Du coup, ça veut dire quoi, une axiomatisation de la physique ?
PS. C'est d'ailleurs pour ça que j'ai du mal à qualifier les mathématiques de "science" au sens habituel du terme.
Posté par kantien .
Évalué à 6 (+4/-0).
Dernière modification le 02 novembre 2025 à 22:05.
Alors je vais sûrement passer pour l'ignare de service qui s’immisce dans un débat qui le dépasse mais j'assume : c'est comme ça qu'on apprend :-)
Si je peux te donner conseil : conserve précieusement cette maxime, et ne cesse jamais d'en faire usage.
Le même prof qui avait plaisanté sur les sanctifiés du Pape nous avait donné ce principe dès les premières minutes de son premier cours :
Si vous ne comprenez pas quelque chose, n'hésitez pas à m'interrompre. Je m'arrêterais pour expliquer. Autrement, je continuerais partant du principe que vous avez compris.
Je n'ai jamais hésité à l'interrompre, et il a toujours satisfait à ma requête. Néanmoins, dans le cadre d'une salle de classe, j'ai pu constaté que nombreux sont ceux n'ayant jamais osé (bien qu'il ne comprenait pas), sans doute de peur de passer pour des idiots. Le problème de la peur du regard des autres…
Du coup, ça veut dire quoi, une axiomatisation de la physique ?
Il faut voir cela avec David Hilbert, c'est son sixième problème.
Le sujet étant long et complexe, j'ai trouvé ce texte en ligne : la portée epistémique de l'axiomatisation de la physique chez Hilbert. Cela reste tout de même un texte très technique qui revient tout d'abord sur l'utilité et la raison d'être de l'axiomatisation pour les mathématiques, avant de traiter de la volonté d'Hilbert d'étendre la méthode à la physique.
Mais sinon, en version plus simple et courte : c'est ce que font tous les programmeurs du monde. Lorsqu'une équipe de programmeurs établit un cahier des charges puis écrit les spécifications du logiciel qu'ils doivent écrire, ils axiomatisent leur domaine métier. Ensuite charge à eux de réifier cette axiomatique, c'est à dire implémenter les spécifications.
C'est là qu'intervient l'utilité pour les programmeurs du domaine de recherche de Jeanas, la théorie des types et la correspondance preuve-programme. Un système de type est un langage dans lequel on peut exprimer ses spécifications, le type checker vérifiant que le code est conforme aux types. Plus le systèmes de types est évolué, plus on peut exprimer finement ses spécifications, et moins il y a de bug (de code non conforme aux spécifications). Et c'est ce qu'on toujours fait les mathématiciens : la preuve d'un théorème est un programme dont l'énoncé est la spécification. Prenons l'exemple du théorème affirmant qu'il existe un nombre infini de nombres premiers. Celui-ci affirme que « pour tout entier n, il existe un entier p premier et strictement plus grand que n ». Toute preuve de ce théorème est un programme qui prend en entrée un entier n, et renvoie en sortie un entier p premier et plus grand que l'entrée. C'est cela la correspondance de Curry-Howard ou correspondance preuve-programme (toute preuve mathématique a un contenu algorithmique, est un programme). Vérifier qu'une preuve est logiquement valide (elle respecte bien les règles de déduction et les axiomes de la théories) ou vérifier qu'un programme est bien typé, c'est tout un ! Un vérificateur de preuves ou un type checker, c'est le même logiciel.
Sur le sujet, il y a ce texte bien plus abordable à lire et comprendre que le premier (je te le conseille pour commencer): À propos de la théorie des démonstrations (du programme de Hilbert aux programmes tout court). L'auteur est aussi un de mes anciens professeurs, celui qui m'initia à ce domaine de la logique. Il est l'auteur d'une machine abstraite La machine de Krivine dont le but était d'interpréter les preuves de théorèmes comme des programmes. Elle est proche, dans son fonctionnement, à la première machine abstraite qui interprétait le bytecode du langage OCaml (la ZINC).
Sinon, pour revenir à de la programmation de tous les jours : utiliser un types primitif d'un langage, c'est poser une axiomatique (tout ce que le langage fournit sur ce type est une axiomatique); programmer contre une classe abstraite, c'est poser une axiomatique (celle décrite par l'interface de la classe); utiliser des interfaces en golang, c'est faire de l'axiomatique (celle décrite par l'interface); utiliser des traits en Rust idem, des types classes en Haskell idem, des foncteurs en OCaml idem… Je n'ai jamais croisé un développeur de ma vie qui ne faisait pas de l'axiomatique sans le savoir (à la manière de monsieur Jourdain).
Enfin, c'est pour cela que je suis sur un site dédié aux logiciels libres : de même qu'une preuve mathématique se doit d'être publique, un code doit l'être; conceptuellement ce ne sont pas deux types d'objets distincts, mais les deux faces d'une seule et même pièce.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
j'ai trouvé ce texte en ligne : la portée épistémique de l'axiomatisation de la physique chez Hilbert.
Texte très intéressant, merci. En ce qui concerne la discussion en cours, le passage suivant m'a éclairé sur la différence entre l'axiomatique pour les systèmes formels et l'axiomatique pour la physique :
La méthode axiomatique ne consiste pas en une activité a priori à partir de laquelle il serait possible de dériver un éventail de connaissances [NDLR comme c'est le cas en mathématiques]. Au contraire, la méthode axiomatique ne sert pas à créer des théories mais se veut plutôt un outil qui permet d'examiner la structure logique des théories existantes.
Si je comprends bien, il ne s'agit pas ici de créer un "univers" (un système formel) sans contrainte a priori par rapport à la réalité physique mais de reformuler (donc a posteriori) sous forme d'axiomes les postulats d'une théorie physique sur le réel pour s'assurer de leur "validité", "objectivité", consistance, …
Par exemple, reformuler les six postulats de la mécanique quantique sous forme d'axiomes, ç’a été tenté ?
Pour en revenir à l'objet du lien, utiliser le concept d'axiomatisation de la physique malgré sa nature très différente de l'axiomatisation des systèmes formels pour y faire des "démonstrations" basées sur ce qui a été démontré dans le cadre d'un système formel (les théorèmes de Gödel, notamment) me paraît douteux mais je n'ai largement pas le niveau pour aller au delà de ce doute "naïf". Je note cependant que tu n'es pas davantage convaincu.
Si je comprends bien, il ne s'agit pas ici de créer un "univers" (un système formel) sans contrainte a priori par rapport à la réalité physique mais de reformuler (donc a posteriori) sous forme d'axiomes les postulats d'une théorie physique sur le réel pour s'assurer de leur "validité", "objectivité", consistance, …
Oui, on ne va tout de même pas prétendre pouvoir faire sortir, comme par magie, de notre esprit, des lois de la nature qui ne peuvent être connus que par expérience.
Comme je l'ai dit par analogie avec la programmation, les spécifications, bien que formalisées et constituant une axiomatique du domaine métier, ne peuvent être formulées que par la connaissance expérimentale du dit domaine. Et l'on y retrouve les deux classes de bugs dans les logiciels : non conformité du code avec les spécifications (c'est là que les systèmes de types jouent un rôle), non conformité des spécifications avec le domaine (cela, aucune méthode formelle ne peut les résoudre).
Cela étant, il reste toujours un part d'a priori dans les théories physiques, que l'on ne peut totalement éliminer pour tout ramener à l'expérience. C'est cela que Kant avait formidablement remarqué (on le retrouve dans Curry-Howard) et que Hilbert espérait résoudre via l'axiomatisation de la physique. On le retrouve dans ce passage de l'article :
Autrement dit, l'axiomatisation de la physique nous permet de nous dégager de la géométrie euclidienne, qui, provenant de notre intuition spatiale, était jusqu'à présent un présupposé
anthropomorphique implicite à notre conception de la structure du monde empirique. Or, en axiomatisant la physique, il devient possible de se dégager de ce présupposé et ainsi atteindre une connaissance plus objective.
Pour un kantien, il restera toujours un fond a priori dans les sciences de la nature. Voir par exemple l'exemple des lois de l'electricité par Ampère, décrite dans cette article : La déraisonnable efficacité des mathématiques. Comme dit dans l'article, c'est lié à ce que Kant appelait sa théorie du schématisme, ce qu'exprime à sa façon la correspondance preuve-programme : les preuves sont des programmes, c'est-à-dire des schèmes (en terme kantien), et l'on ne peut s'en passer pour appréhender le réel. J'aime beaucoup les deux citations de Paul Valéry qui sont si kantienne dans l'esprit :
La mathématique est la science des actes sans les choses et par là des choses que l'on peut définir par des actes.
Quand les contenus sont créés par les opérations mêmes, c'est-à-dire quand quand des opérations remarquées sont désignées, isolées et qu'on en forme des combinaisons, alors on est en mathématiques
Paul Valéry.
On le retrouve dans la conférence donnée par Stéphane Mallat lors du colloque de rentrée au Collège de France sur l'intelligence artificielle : Mystères mathématiques d’intelligences pas si artificielles. À partir de la quatrième minute, il aborde la théorie de la connaissance et les deux tendances qui s'opposent depuis l'antiquité : rationalisme contre empirisme (Platon contre Aristote). Il évoque plus particulièrement David Hume (empiriste) qui mit en doute la notion même de causalité, et Kant qui vint développer la troisième voie : la méthode critique entre le dogmatisme rationaliste et le scepticisme empirique. Il soutient que l'approche des réseaux neurones tient du kantisme mais ne développe pas trop ses raisons, si ce n'est qu'il y a, aussi, une dimension d'a priori dans les réseaux de neurones.
Mais je veux surtout rebondir sur Hume, la causalité et son rapport à Kant. C'est Hume qui fit sortir Kant de son sommeil dogmatique (l'expression est de Kant lui-même) par son attaque contre le principe de causalité. Et la réponse de Kant fut ce qu'il est convenu d'appeler sa théorie des catégories qui est une correspondance preuve-programme bien avant l'heure : la Critique de la Raison Pure date de 1781 et la dite correspondance de la fin des années 1960. La réponse de Kant à Hume fut celle-ci : le principe de causalité n'est pas d'origine empirique, mais nous l'imposons a priori au réel en conformité avec la forme logique des jugements hypothétiques.
Que voulait-il dire par là ? Faisons un détour par la théorie de la démonstration. Parmi les règles de déduction employées par les mathématiciens, il y en a une bien connue sous le nom de modus ponens : si A alors B, or A donc B. Et cette règle est celle qui sert à typer l'application de fonction dans les langages fonctionnels (c'est la base de la correspondance de Curry-Howard). Mais cette règle de typage a un principe analogue dans l'analyse formelle des langages impératifs, c'est le cœur de logique de Hoare avec ses triplets de Hoare {P} C {Q} : un programme C a pour résultat de passer de P à Q. Autrement si ma machine est dans l'état P alors en éxécutant le programme C, elle sera dans l'état Q. Et c'est explicitement ce que Kant avait exposé dans sa table des catégories, via la correspondance entre la table des jugement et la table des catégories. Où l'on voit la correspondance entre les jugements hyptothétiques (si A alors B) et la causalité. Correspondance qu'exprime à leur manière Curry-Howard et Hoare : les programmeurs fonctionnels composent les fonctions, comme les programmeurs impératifs composent les instructions. Et c'est ce lien entre ces deux logiques qui expliquent pourquoi l'on peut automatiser (c'est à dire construire des machines soumises à la causalité) l'exécution des algorithmes et non les exécuter seulement à la main.
On retrouve cette correspondance de la logique dans la confrontation même des théories physiques avec l'expérience. La physique pose une loi causale (en arrière plan, il y a la forme logique si A alors B), constate un état A et observe non B : il y a contradiction entre le réel et la théorie. Conséquence : soit la loi est fausse, soit l'état A était mal déterminé. Deux exemples issu de de la cosmologie :
les perturbations orbitales de Mercure ne correpondent pas aux observations : on prédit B mais on observe non B, on émet l'hypothèse de l'existence d'une autre planète (on pose non A), à savoir Pluton, sans changer la loi ;
le périhélie de Mercure ou la déviation des rayons lumineux par le Soleil, on change la loi (le si A alors B) et on passe à la relativité générale.
Là tu te dis peut être : mais what the fuck !? De quel droit peut-on imposer totalement a priori des lois à la nature (non selon le contenu mais selon la forme) sans même les emprunter à l'expérience ? C'est là que Kant et les kantiens répondent en cœur avec l'enfant bouddhiste de Matrix : la cuillière n'existe pas ! :-P Derrière cette boutade, il y a le principe que si l'on voit partout de l'espace et du temps dans l'expérience, c'est parce qu'on les y met nous mêmes. Donc, d'un point de vue expérimentale, la cuillère existe bien, certes, comme objet spatio-temporellement déterminable. Mais si l'on fait abstraction de son rapport à un observateur, et que l'on se demande : cette chose qui nous apparaît sous la forme d'une cuillière, est-elle en elle même dans l'espace et dans le temps, soumise à la causalité… À cela nous répondons : non ! En tant qu'objet d'expérience possible elle l'est, mais abstraction faite du rapport à l'expérience elle ne l'est pas. Il n'y a pas de réalité absolument indépendante de l'esprit humain qui serait objet d'étude de cette science que l'on nomme physique.
Par exemple, reformuler les six postulats de la mécanique quantique sous forme d'axiomes, ça a été tenté ?
Je ne sais pas. Je ne suis pas assez les travaux de physiciens théoriciens pour le savoir, mais il y a de très forte chance qu'il y ait eu des tentatives.
Pour en revenir à l'objet du lien, utiliser le concept d'axiomatisation de la physique malgré sa nature très différente de l'axiomatisation des systèmes formels pour y faire des "démonstrations" basées sur ce qui a été démontré dans le cadre d'un système formel (les théorèmes de Gödel, notamment) me paraît douteux mais je n'ai largement pas le niveau pour aller au delà de ce doute "naïf". Je note cependant que tu n'es pas davantage convaincu.
Leur usage du théorème d'incomplétude est parfaitement valide. Ce que je ne comprends pas c'est quand ils arguent l'existence de phénomènes observables, donc dont on peut déterminer la valeur de vérité, qui sont hors du champ de la déductibilité du système : il y a des formules non déductibles, le système étant déductivement incomplet, mais en quoi correspondent-elles à des phénomènes observables ? De mémoire, chez Penrose, c'est le phénomène de réduction de la fonction d'ondes ou réductions du vecteur d'états en mécanique quantique qui l'amène à développer sa notion d'entendement non algorithmique. Mais dans cet article, bien court et peu développé, les principes tombent un peu comme un cheveux sur la soupe. Donc je ne sais quoi en dire, d'autant que je suis loin d'être un spécialiste du sujet. Mais je doute qu'il puisse convaincre ceux qui s'occupent du sixième problème de Hilbert.
Pour finir, avec une remarque quelque peu hors-sujet. Kant ne s'est pas contenté de faire usage de son système pour justifier l'usage des mathématiques en physique et la légitimité de certains principes a priori. Il l'a même étendu à la doctrine du droit et à la philosophie politique. Question : pourquoi nos États sont-ils structurés autour de trois pouvoirs (législatif, exécutif et judiciaire). Réponse :
Tout État renferme en soi trois pouvoirs, c’est-à-dire que l’unité de la volonté générale s’y décompose en trois personnes (trias politica) : le souverain pouvoir (la souveraineté), qui réside dans la personne du législateur ; le pouvoir exécutif, dans la personne qui gouverne (conformément à la loi) ; et le pouvoir judiciaire (qui attribue à chacun le sien suivant la loi), dans la personne du juge (potestas legislatoria, rectoria et judiciaria). Ce sont comme les trois propositions d’un syllogisme pratique : la majeure, qui contient la loi d’une volonté ; la mineure, l’ordre de se conduire d’après la loi, c’est-à-dire le principe de la subsomption des actions sous cette loi ; enfin la conclusion (la sentence), qui décide ce qui est de droit dans le cas dont il s’agit.
Kant, Doctrine du droit.
Autrement dit : nous ne faisons que projeter dans la constitution de nos États la structure formelle de notre propre esprit : raison (législatif), entendement (exécutif) et faculté de juger (législatif).
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Quand on écoute les collègues cosmologistes, ils vous disent qu'il n'est pas exclu que ~95% (estimation au doigt mouillée évidemment) de la nature de l'univers échappe actuellement à notre connaissance — les hypothétiques matières noires et énergies noires. Moi qui ait souvent du mal à résoudre un casse-tête que je puisse connaître entièrement, je conçois mal la niveau d'hubris qu'il faudrait avoir, pour prétendre décider du niveau de connaissance impliqué par le titre à partir de si peu (~5%).
J'ai recherché le texte de Kant sur les limites de la connaissance humaine. Je le cite pour la clarté avec laquelle il expose le problème :
La conscience de mon ignorance (si cette ignorance n’est en même temps reconnue comme nécessaire), au lieu de terminer toutes mes recherches, est au contraire la véritable cause qui les provoque. Toute ignorance porte ou bien sur les choses, ou bien sur la détermination et les bornes de ma connaissance. Or, quand l’ignorance est accidentelle, elle doit me pousser, dans le premier cas, à soumettre les choses (les objets) à une investigation dogmatique, et, dans le second, à rechercher, au point de vue critique, les limites de ma connaissance possible. Mais que mon ignorance soit absolument nécessaire, et que par conséquent elle me dispense de toute recherche ultérieure, c’est ce que l’on ne peut prouver empiriquement par l’observation, mais seulement d’une manière critique, en sondant les sources premières de notre connaissance. La détermination des limites de notre raison ne peut donc se faire que suivant des principes à priori, mais nous pouvons connaître aussi à posteriori qu’elle est bornée, en remarquant ce qui, dans toute science, nous reste encore à savoir, bien que cette connaissance d’une ignorance à jamais invincible soit encore indéterminée pour nous. La première connaissance de l’ignorance de la raison, que peut seule nous donner la critique de la raison même, est donc une science ; mais la seconde connaissance n’est qu’une perception, aux suites de laquelle je ne puis assigner des limites. Quand je me représente (suivant l’apparence sensible) la surface de la terre comme un plateau rond, je ne puis savoir jusqu’où elle s’étend. Mais l’expérience m’apprend que, où que j’aille, je vois toujours devant moi un espace où je puis continuer de m’avancer, et je reconnais ainsi les bornes de ma connaissance réelle de la terre, mais non pas celles de toute description possible de la terre. Que si j’en suis venu au point de savoir que la terre est un globe et que sa surface est sphérique, je puis alors connaître d’une manière déterminée et suivant des principes à priori, même par une petite partie de cette surface, un degré par exemple, le diamètre de la terre, et, par ce diamètre, la complète circonscription de la terre, c’est-à-dire sa surface entière ; et, bien que je sois ignorant par rapport aux objets que cette surface peut contenir, je ne le suis pas quant à la circonscription qui les contient, à son étendue et à ses limites.
Comme c'est un problématique de ce genre que traite les auteurs :
Mais que mon ignorance soit absolument nécessaire, et que par conséquent elle me dispense de toute recherche ultérieure, c’est ce que l’on ne peut prouver empiriquement par l’observation, mais seulement d’une manière critique, en sondant les sources premières de notre connaissance.
afin de répondre par la négative au sixième problème de Hilbert, il n'ont pas grand choix sur la méthode. Je ne connais que trois résultats utilisables en la matière :
l'incomplétude de Gödel (limites de la déduction)
le problème de l'arrêt de Turing (limites du calcul)
la critique kantienne (limites de la raison théorique dans son usage philosophique)
Vu la question (existence d'un système axiomatique), il n'ont pas d'autres choix que de passer par l'incomplétude de Gödel. Il l'utilise correctement en l'appliquant à un système adéquate aux hypothèses du théorème (contrairement à Régis Debray. Mais une fois obtenue l'incomplétude déductive du système, le reste de l'argumentaire devient de plus en plus douteux.
D'ailleurs, les mathématiciens (toujours dans le cadre du programme de Hilbert) ont eux aussi cherché un système axiomatique unique dans lequel toutes les mathématiques connues pourraient se formaliser (un anneau pour les gouverner tous ;-). Rien ne disait que c'était faisable, et ce fût fait sous la forme de la théorie axiomatique des ensembles ZF. Elles est bien entendue incomplète, car soumise au théorème d'incomplétude, mais cela n'a jamais perturbé personne. On n'a nullement invoqué je ne sais quel entendement non algorithmique en conséquence. Bien au contraire, cela a ouvert un champ de recherche luxuriant : quels sont les énoncés ayant un sens mathématique important qui sont indécidables dans ZF ? On a au choix : toutes les formes de l'axiome du choix, l'hypothèse du continue de Cantor, l'existence ou non de partie des réels non mesurables au sens de Lebesgue, les axiomes sur les grands ordinaux… Cela a donné des résultats, dits de consistance relative, analogues à ceux obtenus par Poincaré sur la consistance relative des différentes géométries (euclidienne, hyperbolique et sphérique). Et toutes ces mathématiques sont algorithmiques de part en part, du moins on a pour l'instant ZF + Choix dépendant en logique classique interprété comme programmes via Curry-Howard, et ce système est suffisant pour développer tout l'outillage conceptuel actuellement utilisé par les physiciens théoriciens.
Et malgré cela, certains continuent, à bon droit, de chercher des théories concurrentes à ZF, à commencer par la théorie homotopique des types (HoTT) ou celle spéculative du sujet de thèse de Jeanas.
Après, que l'entendement humain soit non algorithmique, je n'en doute pas une seconde. Mais c'est parce qu'il ne sert pas qu'à faire des mathématiques, il sert aussi à philosopher. L'usage mathématique est algorithmique, pas son usage philosophique. Ça c'est Kant qui l'a prouvé.
Les mathématiques donnent le plus éclatant exemple d’une heureuse extension de la raison pure par elle-même et sans le secours de l’expérience. Les exemples sont contagieux, surtout pour cette faculté, qui se flatte naturellement d’avoir toujours le même bonheur qu’elle a eu dans un cas particulier. Aussi la raison pure espère-t-elle pouvoir s’étendre, dans son usage transcendental, avec autant de bonheur et de solidité qu’elle l’a fait dans son usage mathématique, surtout en appliquant ici cette même méthode qui lui a été là d’une si évidente utilité. Il nous importe donc beaucoup de savoir si la méthode qui conduit à la certitude apodictique, et que dans cette dernière science on appelle mathématique, est identique à celle qui sert à chercher cette même certitude dans la philosophie et qui y devrait être appelée dogmatique.
La connaissance philosophique est la connaissance rationnelle par concepts, et la connaissance mathématique la connaissance rationnelle par construction des concepts. Construire un concept, c’est représenter à priori l’intuition qui lui correspond. La construction d’un concept exige donc une intuition non empirique, qui par conséquent, comme intuition, soit un objet singulier, mais qui n’en exprime pas moins, comme construction d’un concept (d’une représentation générale), quelque chose d’universel qui s’applique à toutes les intuitions possibles appartenant au même concept. Ainsi je construis un triangle en représentant l’objet correspondant à ce concept soit par la simple imagination dans l’intuition pure, soit même, d’après celle-ci, sur le papier dans l’intuition empirique, mais dans les deux cas tout à fait à priori, sans en avoir tiré le modèle de quelque expérience. La figure particulière ici décrite est empirique, et pourtant elle sert à exprimer le concept sans nuire à son universalité, parce que, dans cette intuition empirique, on ne songe jamais qu’à l’acte de la construction du concept, auquel beaucoup de déterminations sont tout à fait indifférentes, comme celles de la grandeur, des côtés et des angles, et que l’on fait abstraction de ces différences qui ne changent pas le concept du triangle.
La connaissance philosophique considère le particulier uniquement dans le général, et la connaissance mathématique le général dans le particulier, même dans le singulier, mais à priori et au moyen de la raison, de telle sorte que, comme ce singulier est déterminé d’après certaines conditions générales de la construction, de même l’objet du concept auquel ce singulier ne correspond que comme son schème doit être conçu comme universellement déterminé. […]
Puisque nous nous sommes fait un devoir de déterminer exactement et avec certitude les limites de la raison pure dans l’usage transcendental, mais que cette faculté a ceci de particulier que, malgré les avertissements les plus pressants et les plus clairs, elle se laisse leurrer par l’espoir de parvenir, par de là les limites des expériences, dans les attrayantes contrées de l’intellectuel, il est nécessaire de lui enlever encore en quelque sorte la dernière ancre d’une espérance fantastique, en lui montrant que l’application de la méthode mathématique dans cette espèce de connaissance ne peut lui procurer le moindre avantage, si ce n’est peut-être celui de lui découvrir plus clairement ses propres défauts ; que la géométrie et la philosophie sont deux choses tout à fait différentes, bien qu’elles se donnent la main dans la science de la nature, et que par conséquent les procédés de l’une ne peuvent jamais être imités par l’autre.
La solidité des mathématiques repose sur des définitions, des axiomes et des démonstrations. Je me contenterai de montrer qu’aucun de ces éléments ne peut être ni fourni ni imité par la philosophie dans le sens où le mathématicien le prend ; que le géomètre, en transportant sa méthode, dans la philosophie, ne construit que des châteaux de cartes ; que le philosophe, en appliquant la sienne aux mathématiques, ne peut faire que du verbiage ; ce qui n’empêche pas que le rôle de la philosophie dans cette science ne soit d’en reconnaître les limites, et que le mathématicien lui-même, quand son talent n’est pas déjà circonscrit par la nature et restreint à sa sphère, ne soit obligé de tenir compte des avertissements de la philosophie et de ne pas se mettre au-dessus d’eux.
Et la physique a tout autant besoin de la philosophie que des mathématiques pour justifier ses premiers principes, à commencer par le principe de causalité, et pour se faire elle ne peut emprunter la méthode algorithmique des mathématiques.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Donc c'est plus en lien avec la théorie de la démonstration et la correspondance de Curry-Howard ou correspondance preuves-programmes. Tu es plus du côté informatique (systèmes de types pour les langages de programmation) ou mathématique (HoTT, interprétation des preuves comme programmes, logique classique ou intuitionniste) ?
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
# hum
Posté par Jean Gabes (site web personnel) . Évalué à 3 (+1/-0).
J'ai l'impression que toutes ces démonstrations sont avec au moins un infini dans le lot. Je n'ai pas l'impression que c'est indécidable si le tout est fini et discret.
# la matrice
Posté par bubar🦥 . Évalué à 10 (+13/-0). Dernière modification le 31 octobre 2025 à 17:58.
Ouhai, ça c'est que veut nous faire croire la matrice !
faisez vos propres recherches
# hum bis
Posté par Ltrlg . Évalué à 10 (+11/-0). Dernière modification le 31 octobre 2025 à 18:01.
Si je lis bien, ils ont démontré qu’une simulation algorithmique n’est pas possible pour un modèle donné de notre réalité. Modèle par essence imparfait. Et, dans ces hypothèses hyper-spéculatives de méta-monde, la possibilité d’une simulation non-algorithmique ne peut pas vraiment être écartée (quoi que cela veuille dire). Bon, apparemment ils ne sont pas d’accord sur ce deuxième point (« Any simulation is inherently algorithmic »), mais leur formulation exclue l’usage de systèmes analogues du champ des simulations, ce qui me semble discutable.
Ce qu’ils ont démontré, c’est donc surtout notre incapacité à simuler ledit modèle notre réalité, ce qui est en soi un résultat important, mais aurait probablement fait un moins bon titre ?
[^] # Re: hum bis
Posté par Maclag . Évalué à 4 (+1/-0).
On est vendredi. Il se fait tard. C'était vraiment pas le bon moment pour
essayer denous embrouiller!Donc moi je vais juste retenir qu'on a démonté la Matrice!
------> [ ]
# Alerte crackpots
Posté par jeanas (site web personnel, Mastodon) . Évalué à 7 (+5/-0).
Je viens de lire l'article (https://arxiv.org/pdf/2507.22950). Il se trouve que les théorèmes de Gödel font partie des bases de mon propre domaine de recherche (je suis en thèse). Je n'ai pas le temps de développer mais disons simplement que cet article est du vent. Il ne dit strictement rien d'intéressant et ne prouve certainement pas que nous ne vivons pas dans une simulation.
[^] # Re: Alerte crackpots
Posté par kantien . Évalué à 4 (+3/-1). Dernière modification le 31 octobre 2025 à 23:12.
Quand je vois ce genre de titre, je n'ai même pas envie de lire l'article. Ce n'est pas la première fois, ni la dernière, que l'on fera dire n'importe quoi aux théorèmes de Gödel. Mais même si les physiciens s'y mettent, on n'est pas sorti de l'auberge.
De toute façon, comme je suis kantien, la question n'a même pas de sens pour moi : comme dit le petit enfant boudhiste dans le premier Matrix, « la cuillère n'existe pas ». :-P
Tu fais une thèse en théorie de la démonstration ? ou en calculabilité ? C'est là où j'y vois trois résultats fondamentaux :
Théorèmes qui ne font que confirmer le cœur de la philosophie kantienne, et l'inexistence de la cuillère.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Alerte crackpots
Posté par ǝpɐןƃu∀ nǝıɥʇʇɐW-ǝɹɹǝıԀ (site web personnel) . Évalué à 6 (+4/-0).
Idem, pas envie de lire un blougui-blouga dénué de tout sens. Le titre seul pourrait quasiment convaincre d'un article écrit par un LLM. Mais après tout, peut-être peut-on trouver des gens assez naïfs pour écrire de telles âneries, et d'autres assez peu scrupuleux pour les publier. Ça a au moins l'intérêt de montrer certaines limites des systèmes de publications.
Juste deux petits exemples pour contextualiser ce jugement à l'emporte pièce sur la seule base du titre :
Et n'évoquons même pas la pertinence de la question prétendument résolue…
« IRAFURORBREVISESTANIMUMREGEQUINISIPARETIMPERAT » — Odes — Horace
[^] # Re: Alerte crackpots
Posté par kantien . Évalué à 3 (+1/-0).
Ce jugement semble ne pas avoir été apprécié par un membre du site, à en juger par ma note.
À la même époque, d'autres physiciens (Sokal et Bricmont) reprochaient à certains philosophes français leur usage saugrenu de l'incomplétude de Gödel.
L'un n'empêche pas l'autre. Notre connaissance peut être bornée quant aux contenu du monde (bornée par ce qu'il reste encore à découvrir) mais nous pouvons être en mesure de déterminer les limites du savoir humain (ce que font les méthodes formelles). Kant avait une belle image pour illustrer cela : je peux ignorer le contenu effectif de la surface du globe (il faudrait pour cela en avoir parcouru la totalité) tout en sachant qu'il est circonscrit dans des limites données que je peux déterminer (je n'ai pas besoin de le parcours pour connaître sa circonférence).
Cela étant j'ai fini par lire l'article est je suis moins catégorique que Jeanas sur son contenu : ce n'est pas du Régis Debray. La thèse principale n'est pas tant que nous ne vivons pas dans une simulation, mais qu'une théorie du tout qui unifierait la relativité générale et la physique quantique n'est pas axiomatisable. En résumé : la physique n'est pas axiomatisable. Ce qui a pour corrolaire que l'univers n'est pas une simulation d'ordinateur.
Dans l'ensemble, bien que je souscrives personnellement à ces thèses métaphysiques, leur argumentaire ne me convainc que moyennement. D'une part parce que je doute que la méthode mathématique soit la seule à même de traiter ces questions. D'autre part, parce que l'article consiste à formaliser la thèse de Roger Penrose d'entendement non algorithmique (non algorithmic understanding), thèse qu'il développe par exemple dans son livre Les deux infinis et l'esprit humain. Cette thèse me semblait pas très claire à l'issue de ma lecture du livre, et l'article ne change pas la donne dessus.
Ils font effectivement usage des deux théorèmes de Gödel que j'ai évoqué dans mon premier commentaire. Tout commence à la troisième page de l'article, lorsqu'il suppose une axiomatisation de la physique en supposant l'existence d'un système formel
, dont la signification doit vouloir dire : Formalisation of Quantic Gravitation. Il font sur le système des hypothèses raisonnables : logique du premier ordre, ensemble d'axiomes récursivement énumérables, système complet de règles d'inférence. À dire vrai, ces derniers hypothèses n'en sont pas, c'est la définition même de la proposition « la physique est axiomatisable ».
À cela ils ajoutent deux contraintes :
On peut bien leur accorder la première, la physique théorique ayant besoin de l'arithmétique. C'est celle-ci qui leur permet de faire usage du théorème d'incomplétude : le système axiomatique étant une extension de l'arithmétique de Péano, il est déductivement incomplet.
Mais ensuite, je dois avouer avoir du mal à les suivre dans leur pensée. Ils semblent jongler entre syntaxe et sémantique : il y aurait des énoncés observables, et donc vrais (théorie de la vérité correspondance, sémantique de Tarski), dans l'univers (cf. deuxième contrainte), mais qui ne seraient pas conséquences déductives du système d'axiomes (que l'on pourrait obtenir à partir des axiomes de l'ensemble Sigma et des règles R). Peut être bien, mais lesquelles ? C'est à partir de là qu'ils introduisent leur méta-théorie non algorithmique, leur entendement non algorithmique à la Penrose et qu'ils me perdent. Non que ce genre de méta-théorie ne soient pas considérées par les logiciens mathématiciens (en théorie des modèles, on étudie bien les modèles non standard de l'arithmétique, des théories non récursivement énumérables voir même non dénombrables), mais je ne comprends pas selon quels principes ils l'introduisent ni la justifient.
Cela me rappelle une blague de notre professeur de théorie des modèles, lorsque j'étais étudiant en DEA de logique mathématique et fondements de l'informatique. Il faut faire attention, ici, que le mot modèle est un homonyme de celui utilisé en physique (bien qu'il y ait des rapports entre les deux). Pour un théoricien des modèles, à la question qu'est-ce qu'un groupe ? Il répond : un modèle de la théorie des groupes, c'est à dire une structure qui satisfait à l'axiomatique de la théorie.
Trève de digression et revenons à sa blague. Un jour, en début du cours, il nous tint à peu près ce discours : « je lisais ce matin dans le Monde que la pape Jean Paul II avait sanctifié plus de personnes que tous ces prédécesseurs réunis. Sachant que, durant ces 20 dernières années, on a publié plus d'écrits mathématiques que durant toute la période de l'humanité qui précède, si un jour vous publiez un article insignifiant, vous pourrez vous considérer en bijection avec un sanctifié du pape ! ».
Je dois admettre, après lecture de l'article, que je ne sais quoi dire sur le statut de sanctifiés de ses auteurs.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Alerte crackpots
Posté par mahikeulbody . Évalué à 3 (+1/-0). Dernière modification le 02 novembre 2025 à 09:34.
Alors je vais sûrement passer pour l'ignare de service qui s’immisce dans un débat qui le dépasse mais j'assume : c'est comme ça qu'on apprend :-)
Je ne comprends pas ce point. Naïvement, pour moi, on a deux choses complètement différentes
1) La théorie mathématique (je dirais plutôt "Le système formel"), basée sur des axiomes arbitraires (mais qui doivent avoir certaines caractéristiques pour que la théorie soit intéressante) ; il n'y a rien à prouver (à part les théorèmes issus de la théorie elle-même)
2) La théorie scientifique, basée sur des postulats qui semblent permettre une bonne formalisation du réel (et donc non arbitraires) ; on cherche à
prouvervérifier que les résultats fournis mathématiquement par la formalisation de la théorie sont cohérents avec les observations et, ainsi, conforter les postulats.Du coup, ça veut dire quoi, une axiomatisation de la physique ?
PS. C'est d'ailleurs pour ça que j'ai du mal à qualifier les mathématiques de "science" au sens habituel du terme.
[^] # Re: Alerte crackpots
Posté par kantien . Évalué à 6 (+4/-0). Dernière modification le 02 novembre 2025 à 22:05.
Si je peux te donner conseil : conserve précieusement cette maxime, et ne cesse jamais d'en faire usage.
Le même prof qui avait plaisanté sur les sanctifiés du Pape nous avait donné ce principe dès les premières minutes de son premier cours :
Je n'ai jamais hésité à l'interrompre, et il a toujours satisfait à ma requête. Néanmoins, dans le cadre d'une salle de classe, j'ai pu constaté que nombreux sont ceux n'ayant jamais osé (bien qu'il ne comprenait pas), sans doute de peur de passer pour des idiots. Le problème de la peur du regard des autres…
Il faut voir cela avec David Hilbert, c'est son sixième problème.
Le sujet étant long et complexe, j'ai trouvé ce texte en ligne : la portée epistémique de l'axiomatisation de la physique chez Hilbert. Cela reste tout de même un texte très technique qui revient tout d'abord sur l'utilité et la raison d'être de l'axiomatisation pour les mathématiques, avant de traiter de la volonté d'Hilbert d'étendre la méthode à la physique.
Mais sinon, en version plus simple et courte : c'est ce que font tous les programmeurs du monde. Lorsqu'une équipe de programmeurs établit un cahier des charges puis écrit les spécifications du logiciel qu'ils doivent écrire, ils axiomatisent leur domaine métier. Ensuite charge à eux de réifier cette axiomatique, c'est à dire implémenter les spécifications.
C'est là qu'intervient l'utilité pour les programmeurs du domaine de recherche de Jeanas, la théorie des types et la correspondance preuve-programme. Un système de type est un langage dans lequel on peut exprimer ses spécifications, le type checker vérifiant que le code est conforme aux types. Plus le systèmes de types est évolué, plus on peut exprimer finement ses spécifications, et moins il y a de bug (de code non conforme aux spécifications). Et c'est ce qu'on toujours fait les mathématiciens : la preuve d'un théorème est un programme dont l'énoncé est la spécification. Prenons l'exemple du théorème affirmant qu'il existe un nombre infini de nombres premiers. Celui-ci affirme que « pour tout entier
n, il existe un entierppremier et strictement plus grand que n ». Toute preuve de ce théorème est un programme qui prend en entrée un entiern, et renvoie en sortie un entierppremier et plus grand que l'entrée. C'est cela la correspondance de Curry-Howard ou correspondance preuve-programme (toute preuve mathématique a un contenu algorithmique, est un programme). Vérifier qu'une preuve est logiquement valide (elle respecte bien les règles de déduction et les axiomes de la théories) ou vérifier qu'un programme est bien typé, c'est tout un ! Un vérificateur de preuves ou un type checker, c'est le même logiciel.Sur le sujet, il y a ce texte bien plus abordable à lire et comprendre que le premier (je te le conseille pour commencer): À propos de la théorie des démonstrations (du programme de Hilbert aux programmes tout court). L'auteur est aussi un de mes anciens professeurs, celui qui m'initia à ce domaine de la logique. Il est l'auteur d'une machine abstraite La machine de Krivine dont le but était d'interpréter les preuves de théorèmes comme des programmes. Elle est proche, dans son fonctionnement, à la première machine abstraite qui interprétait le bytecode du langage OCaml (la ZINC).
Sinon, pour revenir à de la programmation de tous les jours : utiliser un types primitif d'un langage, c'est poser une axiomatique (tout ce que le langage fournit sur ce type est une axiomatique); programmer contre une classe abstraite, c'est poser une axiomatique (celle décrite par l'interface de la classe); utiliser des interfaces en golang, c'est faire de l'axiomatique (celle décrite par l'interface); utiliser des traits en Rust idem, des types classes en Haskell idem, des foncteurs en OCaml idem… Je n'ai jamais croisé un développeur de ma vie qui ne faisait pas de l'axiomatique sans le savoir (à la manière de monsieur Jourdain).
Enfin, c'est pour cela que je suis sur un site dédié aux logiciels libres : de même qu'une preuve mathématique se doit d'être publique, un code doit l'être; conceptuellement ce ne sont pas deux types d'objets distincts, mais les deux faces d'une seule et même pièce.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Alerte crackpots
Posté par mahikeulbody . Évalué à 3 (+1/-0).
Texte très intéressant, merci. En ce qui concerne la discussion en cours, le passage suivant m'a éclairé sur la différence entre l'axiomatique pour les systèmes formels et l'axiomatique pour la physique :
La méthode axiomatique ne consiste pas en une activité a priori à partir de laquelle il serait possible de dériver un éventail de connaissances [NDLR comme c'est le cas en mathématiques]. Au contraire, la méthode axiomatique ne sert pas à créer des théories mais se veut plutôt un outil qui permet d'examiner la structure logique des théories existantes.
Si je comprends bien, il ne s'agit pas ici de créer un "univers" (un système formel) sans contrainte a priori par rapport à la réalité physique mais de reformuler (donc a posteriori) sous forme d'axiomes les postulats d'une théorie physique sur le réel pour s'assurer de leur "validité", "objectivité", consistance, …
Par exemple, reformuler les six postulats de la mécanique quantique sous forme d'axiomes, ç’a été tenté ?
Pour en revenir à l'objet du lien, utiliser le concept d'axiomatisation de la physique malgré sa nature très différente de l'axiomatisation des systèmes formels pour y faire des "démonstrations" basées sur ce qui a été démontré dans le cadre d'un système formel (les théorèmes de Gödel, notamment) me paraît douteux mais je n'ai largement pas le niveau pour aller au delà de ce doute "naïf". Je note cependant que tu n'es pas davantage convaincu.
[^] # Re: Alerte crackpots
Posté par kantien . Évalué à 3 (+1/-0).
Oui, on ne va tout de même pas prétendre pouvoir faire sortir, comme par magie, de notre esprit, des lois de la nature qui ne peuvent être connus que par expérience.
Comme je l'ai dit par analogie avec la programmation, les spécifications, bien que formalisées et constituant une axiomatique du domaine métier, ne peuvent être formulées que par la connaissance expérimentale du dit domaine. Et l'on y retrouve les deux classes de bugs dans les logiciels : non conformité du code avec les spécifications (c'est là que les systèmes de types jouent un rôle), non conformité des spécifications avec le domaine (cela, aucune méthode formelle ne peut les résoudre).
Cela étant, il reste toujours un part d'a priori dans les théories physiques, que l'on ne peut totalement éliminer pour tout ramener à l'expérience. C'est cela que Kant avait formidablement remarqué (on le retrouve dans Curry-Howard) et que Hilbert espérait résoudre via l'axiomatisation de la physique. On le retrouve dans ce passage de l'article :
Pour un kantien, il restera toujours un fond a priori dans les sciences de la nature. Voir par exemple l'exemple des lois de l'electricité par Ampère, décrite dans cette article : La déraisonnable efficacité des mathématiques. Comme dit dans l'article, c'est lié à ce que Kant appelait sa théorie du schématisme, ce qu'exprime à sa façon la correspondance preuve-programme : les preuves sont des programmes, c'est-à-dire des schèmes (en terme kantien), et l'on ne peut s'en passer pour appréhender le réel. J'aime beaucoup les deux citations de Paul Valéry qui sont si kantienne dans l'esprit :
On le retrouve dans la conférence donnée par Stéphane Mallat lors du colloque de rentrée au Collège de France sur l'intelligence artificielle : Mystères mathématiques d’intelligences pas si artificielles. À partir de la quatrième minute, il aborde la théorie de la connaissance et les deux tendances qui s'opposent depuis l'antiquité : rationalisme contre empirisme (Platon contre Aristote). Il évoque plus particulièrement David Hume (empiriste) qui mit en doute la notion même de causalité, et Kant qui vint développer la troisième voie : la méthode critique entre le dogmatisme rationaliste et le scepticisme empirique. Il soutient que l'approche des réseaux neurones tient du kantisme mais ne développe pas trop ses raisons, si ce n'est qu'il y a, aussi, une dimension d'a priori dans les réseaux de neurones.
Mais je veux surtout rebondir sur Hume, la causalité et son rapport à Kant. C'est Hume qui fit sortir Kant de son sommeil dogmatique (l'expression est de Kant lui-même) par son attaque contre le principe de causalité. Et la réponse de Kant fut ce qu'il est convenu d'appeler sa théorie des catégories qui est une correspondance preuve-programme bien avant l'heure : la Critique de la Raison Pure date de 1781 et la dite correspondance de la fin des années 1960. La réponse de Kant à Hume fut celle-ci : le principe de causalité n'est pas d'origine empirique, mais nous l'imposons a priori au réel en conformité avec la forme logique des jugements hypothétiques.
Que voulait-il dire par là ? Faisons un détour par la théorie de la démonstration. Parmi les règles de déduction employées par les mathématiciens, il y en a une bien connue sous le nom de modus ponens :
si A alors B, or A donc B. Et cette règle est celle qui sert à typer l'application de fonction dans les langages fonctionnels (c'est la base de la correspondance de Curry-Howard). Mais cette règle de typage a un principe analogue dans l'analyse formelle des langages impératifs, c'est le cœur de logique de Hoare avec ses triplets de Hoare{P} C {Q}: un programmeCa pour résultat de passer dePàQ. Autrement si ma machine est dans l'étatPalors en éxécutant le programmeC, elle sera dans l'étatQ. Et c'est explicitement ce que Kant avait exposé dans sa table des catégories, via la correspondance entre la table des jugement et la table des catégories. Où l'on voit la correspondance entre les jugements hyptothétiques (si A alors B) et la causalité. Correspondance qu'exprime à leur manière Curry-Howard et Hoare : les programmeurs fonctionnels composent les fonctions, comme les programmeurs impératifs composent les instructions. Et c'est ce lien entre ces deux logiques qui expliquent pourquoi l'on peut automatiser (c'est à dire construire des machines soumises à la causalité) l'exécution des algorithmes et non les exécuter seulement à la main.On retrouve cette correspondance de la logique dans la confrontation même des théories physiques avec l'expérience. La physique pose une loi causale (en arrière plan, il y a la forme logique
si A alors B), constate un étatAet observenon B: il y a contradiction entre le réel et la théorie. Conséquence : soit la loi est fausse, soit l'état A était mal déterminé. Deux exemples issu de de la cosmologie :Là tu te dis peut être : mais what the fuck !? De quel droit peut-on imposer totalement a priori des lois à la nature (non selon le contenu mais selon la forme) sans même les emprunter à l'expérience ? C'est là que Kant et les kantiens répondent en cœur avec l'enfant bouddhiste de Matrix : la cuillière n'existe pas ! :-P Derrière cette boutade, il y a le principe que si l'on voit partout de l'espace et du temps dans l'expérience, c'est parce qu'on les y met nous mêmes. Donc, d'un point de vue expérimentale, la cuillère existe bien, certes, comme objet spatio-temporellement déterminable. Mais si l'on fait abstraction de son rapport à un observateur, et que l'on se demande : cette chose qui nous apparaît sous la forme d'une cuillière, est-elle en elle même dans l'espace et dans le temps, soumise à la causalité… À cela nous répondons : non ! En tant qu'objet d'expérience possible elle l'est, mais abstraction faite du rapport à l'expérience elle ne l'est pas. Il n'y a pas de réalité absolument indépendante de l'esprit humain qui serait objet d'étude de cette science que l'on nomme physique.
Je ne sais pas. Je ne suis pas assez les travaux de physiciens théoriciens pour le savoir, mais il y a de très forte chance qu'il y ait eu des tentatives.
Leur usage du théorème d'incomplétude est parfaitement valide. Ce que je ne comprends pas c'est quand ils arguent l'existence de phénomènes observables, donc dont on peut déterminer la valeur de vérité, qui sont hors du champ de la déductibilité du système : il y a des formules non déductibles, le système étant déductivement incomplet, mais en quoi correspondent-elles à des phénomènes observables ? De mémoire, chez Penrose, c'est le phénomène de réduction de la fonction d'ondes ou réductions du vecteur d'états en mécanique quantique qui l'amène à développer sa notion d'entendement non algorithmique. Mais dans cet article, bien court et peu développé, les principes tombent un peu comme un cheveux sur la soupe. Donc je ne sais quoi en dire, d'autant que je suis loin d'être un spécialiste du sujet. Mais je doute qu'il puisse convaincre ceux qui s'occupent du sixième problème de Hilbert.
Pour finir, avec une remarque quelque peu hors-sujet. Kant ne s'est pas contenté de faire usage de son système pour justifier l'usage des mathématiques en physique et la légitimité de certains principes a priori. Il l'a même étendu à la doctrine du droit et à la philosophie politique. Question : pourquoi nos États sont-ils structurés autour de trois pouvoirs (législatif, exécutif et judiciaire). Réponse :
Autrement dit : nous ne faisons que projeter dans la constitution de nos États la structure formelle de notre propre esprit : raison (législatif), entendement (exécutif) et faculté de juger (législatif).
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Alerte crackpots
Posté par kantien . Évalué à 3 (+1/-0).
J'ai recherché le texte de Kant sur les limites de la connaissance humaine. Je le cite pour la clarté avec laquelle il expose le problème :
Comme c'est un problématique de ce genre que traite les auteurs :
afin de répondre par la négative au sixième problème de Hilbert, il n'ont pas grand choix sur la méthode. Je ne connais que trois résultats utilisables en la matière :
Vu la question (existence d'un système axiomatique), il n'ont pas d'autres choix que de passer par l'incomplétude de Gödel. Il l'utilise correctement en l'appliquant à un système adéquate aux hypothèses du théorème (contrairement à Régis Debray. Mais une fois obtenue l'incomplétude déductive du système, le reste de l'argumentaire devient de plus en plus douteux.
D'ailleurs, les mathématiciens (toujours dans le cadre du programme de Hilbert) ont eux aussi cherché un système axiomatique unique dans lequel toutes les mathématiques connues pourraient se formaliser (un anneau pour les gouverner tous ;-). Rien ne disait que c'était faisable, et ce fût fait sous la forme de la théorie axiomatique des ensembles ZF. Elles est bien entendue incomplète, car soumise au théorème d'incomplétude, mais cela n'a jamais perturbé personne. On n'a nullement invoqué je ne sais quel entendement non algorithmique en conséquence. Bien au contraire, cela a ouvert un champ de recherche luxuriant : quels sont les énoncés ayant un sens mathématique important qui sont indécidables dans ZF ? On a au choix : toutes les formes de l'axiome du choix, l'hypothèse du continue de Cantor, l'existence ou non de partie des réels non mesurables au sens de Lebesgue, les axiomes sur les grands ordinaux… Cela a donné des résultats, dits de consistance relative, analogues à ceux obtenus par Poincaré sur la consistance relative des différentes géométries (euclidienne, hyperbolique et sphérique). Et toutes ces mathématiques sont algorithmiques de part en part, du moins on a pour l'instant ZF + Choix dépendant en logique classique interprété comme programmes via Curry-Howard, et ce système est suffisant pour développer tout l'outillage conceptuel actuellement utilisé par les physiciens théoriciens.
Et malgré cela, certains continuent, à bon droit, de chercher des théories concurrentes à ZF, à commencer par la théorie homotopique des types (HoTT) ou celle spéculative du sujet de thèse de Jeanas.
Après, que l'entendement humain soit non algorithmique, je n'en doute pas une seconde. Mais c'est parce qu'il ne sert pas qu'à faire des mathématiques, il sert aussi à philosopher. L'usage mathématique est algorithmique, pas son usage philosophique. Ça c'est Kant qui l'a prouvé.
Et la physique a tout autant besoin de la philosophie que des mathématiques pour justifier ses premiers principes, à commencer par le principe de causalité, et pour se faire elle ne peut emprunter la méthode algorithmique des mathématiques.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Alerte crackpots
Posté par jeanas (site web personnel, Mastodon) . Évalué à 3 (+1/-0).
Théorie des types
[^] # Re: Alerte crackpots
Posté par kantien . Évalué à 4 (+2/-0).
Donc c'est plus en lien avec la théorie de la démonstration et la correspondance de Curry-Howard ou correspondance preuves-programmes. Tu es plus du côté informatique (systèmes de types pour les langages de programmation) ou mathématique (HoTT, interprétation des preuves comme programmes, logique classique ou intuitionniste) ?
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Alerte crackpots
Posté par jeanas (site web personnel, Mastodon) . Évalué à 4 (+2/-0).
Mon sujet principal est une variante spéculative de HoTT.
Envoyer un commentaire
Suivre le flux des commentaires
Note : les commentaires appartiennent à celles et ceux qui les ont postés. Nous n’en sommes pas responsables.