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.
[^] # Re: Alerte crackpots
Posté par kantien . En réponse au lien Il est mathématiquement prouvé que nous ne vivons pas dans une simulation informatique. Évalué à 3.
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.