Re: Le cerveau n'est pas logique

Il y a quand même une légère différence dans les détails :)

Pas spécialement, le principe que je décris est celui qu'a utilisé Gödel pour démontrer son fameux théorème d'incomplétude : une théorie assez riche (au pouvoir expressif suffisant) pour parler d'elle même a toujours des énoncés indécidables (qu'elle ne peut ni prouver ni réfuter) et parmi ceux-ci figurent toujours sa propre cohérence (sa non contradiction). Ce que je dis c'est que si une théorie est assez riche (comme l'est ZF) pour exprimer les principes de la théorie des modèles et donc parler de la relation entre la forme et le contenu (ce en quoi consiste la vérité) alors elle ne peut engendrer son propre contenu (elle ne peut construire un modèle d'elle même) et fournir un critère matériel et universelle de la vérité, sous peine d'être incohérente d'après le théorème d'incomplétude. Dans ce cas, comme elle peut prouver tout et n'importe, on ne peut nullement avoir confiance dans ce qu'elle prétend affirmer.

Cette démarche consiste à réfléchir la métathéorie dans la théorie elle même, c'est le même genre d'argument qu'a utilisé Turing pour prouver l'impossibilité de résoudre le problème de l'arrêt pour sa machine universelle. D'un point de vue programmation, cela revient à dire qu'un langage ne peut se compiler lui-même sans une phase de bootstrap : il faut un coup de pouce extérieur au langage de programmation.

J’ai l’impression que tu décris une sorte de « principe de réflexion » de la pensée abstraite dans la logique formelle, comme dans l’univers constructible de Gôdel ( http://www.madore.org/~david/weblog/d.2013年03月19日.2124.constructible.html ) ou les ensembles et leur structure décrit par un rang inférieur se reflètent dans les rangs supérieurs de différentes manières.

L'univers des constructibles de Gödel sert à prouver des théorèmes de consistance relative : si ZF est non contradictoire alors il en est de même de ZF augmentée de l'axiome du choix, ce dernier axiome n'introduit pas de contradiction dans la théorie. C'est du même ordre que les théorèmes de consistance relative que Poincaré a effectués au XIXème entre les géométries euclidienne et non euclidiennes. Le cercle de Poincaré, construit dans un espace euclidien, permet d'interpréter les axiomes de la géométrie hyperbolique. Autrement dit, si la géométrie euclidienne est cohérente alors il en est de même de l'hyperbolique.

En revanche aux questions : l'arithmétique est-elle cohérente ? la géométrie est-elle cohérente ? ZF est-elle cohérente ? la logique et son principe de contradiction est incapable d'y répondre. La seule chose qu'elle peut faire c'est prouver la cohérence d'une théorie en admettant la cohérence d'une autre. Par exemple, on peut prouver la cohérence de l'arithmétique à partir de ZF, mais reste la question : ZF est elle cohérente ? On peut continuer en ajoutant des axiomes de grands cardinaux qui prouvent la consistance de ZF (ils fournissent un modèle de celle-ci), mais reviens alors la question : ses nouveaux axiomes sont-ils cohérents ? Et cette approche turtles all the way down la logique formelle ne peut en sortir, pour la simple raison que, laissée à elle même, elle n'engendre que des tautologies (l'art de M. de La Palice) et est incapable de répondre à la question : comment des jugements synthétiques a priori sont-ils possibles ?

Les principes abstraits en langage naturel de Kant se reflètent dans les méthodes formelles modernes. Mais enrichis :)

Ça se discute, ils ne sont nullement enrichis, ce sont les mêmes mais exprimés dans une langue différente. Un principe ne deviendrait ni plus vrai, ni plus clair, ni plus riche sous prétexte qu'il serait exprimés en français plutôt qu'en anglais (ou vice versa). La méthode kantienne est on ne peut plus formelle (il n'y a pas plus formaliste qu'un kantien), et les langues naturelles sont tout à fait adaptées pour exprimer de tels principes. Il n'est pas nécessaire de recourir à des symbolismes compréhensibles par une machine (ce qui n'est d'ailleurs adapté qu'à la formalisation de la pensée mathématique mais nullement à la pensée philosophique, comme les problèmes de philosophie du droit) pour formaliser sa pensée : je préfère de loin l'usage du français à Coq, par exemple. Les langues naturelles ont, en leur sein, un système à type dépendant mais une grammaire plus complexe que les grammaires régulières des langages de programmation (il suffit de voir la difficulté que rencontre l'auteur de grammalecte, ou tous ceux qui travaillent sur le traitement automatique des langues).

Prenons, un principe de base de la logique de Hoare utilisée pour la formalisation des langages impératifs, celui de la composition des instructions :

{ P } S { Q } { Q } T { R }
----------------------------
 { P } S ; T { R }

une expression de la forme { P } S { Q } se lit : l'instruction S fait passer le système de l'état P à l'état Q. Une telle règle ce lit alors : si l'instruction S fait passer la machine de l'état P à l'état Q et que l'instruction T fait passer de l'état Q à l'état R, alors la série d'instructions S ; T fait passer de l'état P à l'état R.

Il se trouve que c'est l'analogue dans le paradigme de la programmation fonctionnelle pure de la composition des fonctions :

fun f g x -> g (f x);;
- : ('a -> 'b) -> ('b -> 'c) -> 'a -> 'c = <fun>

A --> B B --> C
------------------
 A --> C

Autrement dit, des deux prémisses si A alors B et si B alors C, on conclue à si A alors C. Cela résulte d'une double application de la règle dite du modus ponens :

• si A alors B, or A donc B (modus ponens utilisant la première prémisse et l'hypothèse A)
• si B alors C, or B donc C (modus ponens utilisant la seconde prémisse et la conclusion du syllogisme hypothétique précédent)

ainsi en supposant A on conclue à C, c'est à dire que l'on a prouvé si A alors C. Ce genre de preuve, quelque peu pédante, est ce que nous oblige à écrire Coq (il offre quand même des techniques pour éviter de rentrer autant dans les détails).

Ce que Kant a prouvé, par exemple, dans la Critique de la Raison Pure c'est que le concept de cause (qui sert à expliquer les changements d'états des choses réelles dans le monde physique) n'est pas un concept d'origine empirique, mais un concept que nous imposons nous même à la nature en vertu de la structure formelle de notre esprit et qu'il a pour type (là j'emploie une terminologie contemporaine) la forme logique des jugements hypothétiques (si A alors B).

On pourrait exprimer le principe fondamentale de la dynamique de Newton ainsi dans un tel symbolisme : { p } F { p + F * dt}. Autrement dit, un corps dans l'état de mouvement p et soumis à une force F se retrouve dans l'état { p + F * dt } au bout d'un temps infiniment petit dt. L'on retrouverait ainsi les considérations entre les sémantiques petit pas (small step) ou grands pas (big step), auxquelles gasche faisait allusion dans ce commentaire, et la distinction entre les lois différentielles et les lois intégrales en physique théorique. La première étant une approche discrète (sémantique des langages de programmation), là où la seconde est continue (physique théorique).

Et c'est ce lien formel entre le principe de causalité et la forme des jugements hypothétiques qui explique que l'on peut construire des machines qui « exécutent » les calculs automatiquement.

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