Re: Le cerveau n'est pas logique

La logique peut aussi vérifier la cohérence interne des connaissances des experts sur leur sujet. [...] Mais du point de vue de la cohérence, ça peut lever des lièvres.

Oui car telle est son affaire, elle peut montrer l'incohérence d'une formalisation. Pour ce qui est de prouver la cohérence, par contre...

Ça me rappelle ce passage humoristique dans la partie remerciements de la thèse de Perthmâd (qui, s'y j'en crois les notes de publication de la toute récente dernière version de Coq, a fait un gros travail de nettoyage et d'optimisation du langage des tactiques) :

— Un thésard demanda à Hugo Herbelin : « Coq est-il cohérent ? »
— Anomaly: Uncaught exception Mu.

Par malheur, l’histoire omet de raconter si l’étudiant fut illuminé ou bien s’il l’était déjà à l’instant même où il songea à passer un doctorat d’informatique fondamentale 5 [1].

[1]Par contre, l’histoire précise bien que le rapport de bug qui s’en suivit fut marqué WontFix par un certain kgoedel. Ce n’est pas dans le privé qu’on verrait ça.

Dans une démarche également historique, le passage que j'ai cité de la Critique de la Raison Pure est extrait du paragraphe sur la question « Qu'est-ce que la vérité ? » qui commence ainsi :

La vielle est célèbre question, par laquelle on se figurait pousser les logiciens dans leur retranchement et on cherchait à les amener, ou à devoir se laisser surprendre dans un pitoyable diallèle, ou bien à devoir avouer leur ignorance, et par la suite la vanité de tout leur art, est celle-ci : Qu'est-ce que la vérité ? La définition nominale de la vérité, qui en fait la conformité de la connaissance avec son objet, est ici accordée et supposée; mais on veut savoir quel est le critère universel et sûr de la vérité de toute connaissance.

C'est déjà une grande et nécessaire preuve de sagesse et de pénétration que de savoir ce que l'on doit raisonnablement demander. En effet, si la question est absurde en soi et si elle appelle parfois, outre la confusion de celui qui la soulève, l'inconvénient de porter à des réponses absurdes l'auditeur qui n'est pas sur ses gardes, et de donner ainsi le ridicule spectacle de deux personnes, dont l'un trait le bouc (comme disaient les anciens), tandis que l'autre tend un tamis.

Si la vérité consiste dans l'accord d'une connaissance avec son objet, cet objet doit être par là distinguer des autres; car une connaissance est fausse, si elle ne s'accorde pas avec lequel elle est rapportée, alors même qu'elle pourrait bien valoir pour d'autres objets. Or, un critère universel de la vérité serait celui qui vaudrait pour toutes les connaissances, sans distinction de leurs objets. Mais il est clair, puisqu'on y fait abstraction de tout contenu de la connaissance (du rapport à son objet), et que la vérité à trait justement à ce contenu, qu'il est tout à fait impossible et absurde de demander une marque de la vérité de ce contenu des connaissances, et qu'on ne peut donc proposer une caractéristique suffisante et en même temps universelle de la vérité. Comme nous avons déjà nommé plus haut le contenu de la connaissance sa matière, on devra dire : On ne peut demander aucune caractéristique universelle de la vérité quant à sa matière, parce que c'est en soi contradictoire.

Kant, Critique de la Raison Pure.

On trouve des considérations identiques dans le traité qu'il consacra à la logique. Premièrement, ce qu'il appelle la définition nominale de la vérité est celle que l'on utilise toujours de nos jours sous le nom de définition tarskienne de la vérité à la base de la sémantique tarskienne (utilisée en théorie des modèles). Ensuite, si l'on combine le théorème de Gödel auquel Perthmâd fait allusion (le théorème d'incomplétude) à une autre théorème fondamentale de Gödel (son théorème de complétude : une théorie est cohérente si et seulement si elle a un modèle), on aboutit à la conclusion du texte kantien cité ci-dessus. Une théorie (disons ZF, la théorie axiomatique des ensembles) qui fournirait un critère matérielle de sa vérité serait en mesure d'engendrer son propre contenu (fournirait un modèle d'elle-même), serait donc cohérente (en vertu du théorème de complétude) ce qui contredirait le théorème d'incomplétude.

Le théorème d'incomplétude clos une période historique au cours de laquelle la thèse centrale de la Critique de la Raison Pure fut attaqué de toute part par des logiciens, et Gödel finit par donner raison à Kant. :-)

On gagne déjà beaucoup à pouvoir faire tenir une foule de recherche sous la formule d'un seul problème. Par là, en effet, on ne facilite pas seulement pour soi-même son propre travail, en se le déterminant avec précision, mais on rend aussi plus facile à quiconque veut l'examiner de juger si nous avons ou non satisfait à notre dessein. Le problème propre de la raison pur est donc contenu dans la question suivante : Comment des jugements synthétiques a priori sont-ils possibles ? [...]

Dans la solution du problème précèdent est engagée en même temps la possibilité du pur usage de la raison pour fonder est développer toutes les sciences qui contiennent une connaissance théorique a priori des objets, c'est-à-dire la réponse à ces questions :

• Comment la mathématique pure est-elle possible ?
• Comment la physique pure est-elle possible ?

Kant, ibid.

À cette subdivision de la question, précède le texte suivant :

Les jugements mathématiques sont tous synthétiques. Cette proposition semble avoir échappé jusqu'ici aux observations des analystes de la raison humaine, et même être exactement opposée à toutes leurs conjectures, bien qu'elle soit incontestablement certaine et très importantes dans ses conséquences. En effet, comme on trouvait que tous les raisonnements mathématiques procédaient tous d'après le principe de contradiction (ce qu'exige la nature de toute certitude apodictique) on se persuada que les principes étaient connu aussi étaient connus à partir du principe de contradiction : en quoi ces analystes; car une proposition synthétique peut bien être saisie d'après le principe de contradiction, mais seulement de telle sorte qu'une autre proposition synthétique soit supposée, d'où elle puisse être déduite, mais jamais en elle-même.

Kant, ibid.

Ce qu'a prouvé Gödel, c'est que la logique formelle (et donc le principe de contradiction) ne peut légitimer à elle seule le raisonnement par récurrence : le principe du raisonnement par récurrence est un pur jugement synthétique a priori.

Il y a un membre de linuxfr qui a pour signature quelque chose du style : «BeOS le faisait déjà il y a vingt ans ». Pour ma part, d'une manière générale, je dirais : ce que font les théories des types contemporaines, Kant le faisait déjà il y a plus de 200 ans. Par exemple, la logique de Hoare utilisée par frama-c, c'est dans la Critique de la Raison Pure; ou bien la programmation par contrat, la gestion de propriété des espaces mémoires par Rust ou Mezzo, c'est dans la Doctrine du Droit (que l'on peut voir comme une théorie de typage du droit romain). :-)

Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.