Notes sur l'intuitionnisme

Qu’est ce que l’intuitionnisme ?

L’intuitionnisme est une philosophie des mathématiques, née dans les années 1890, sous l’impulsion de Brouwer. L’intuitionnisme est un kantisme radical appliqué aux mathématiques. Il se caractérise par le refus du principe du tiers-exclus et affirme que tant que l’on n’a pas construit la vérité d’un fait, celui-ci n’existe pas. Il s’oppose en cela à la conception platonisante des idéalités mathématiques. Platon considérait que le monde mathématique est parfait : étant donné p, si p porte sur un objet mathématique, p est soit vrai soit faux, indépendamment du fait qu’on puisse le savoir ou non. Le mathématicien est alors perçu un découvreur de vérités. Pour l’intuitionnisme, au contraire, il est un constructeur de vérités.

Pour Brouwer, la philosophie platonisante des mathématiques est anachronique. Les mathématiques, selon lui, ne sont qu’une création humaine. Il se peut donc que des propositions mathématiques ne soient ni vraies ni fausses, puisqu’on ne les connaît pas encore. Tant qu’on n’y a pas accès par une preuve, on ne peut pas dire d’une proposition qu’elle est vraie ou fausse.

Donc si on montre qu’une chose est impossible, on n’a pas montré que l’inverse est vrai pour autant. Tout dépend des axiomes : il peut y avoir de l’indéterminé. Donc A∨¬A n’est pas un théorème. Les affirmations de Socrate selon lesquelles si on a montré qu’il impossible que l’homme ne soit pas libre, alors on a montré qu’il est libre, contiennent donc, dans la perspective intuitionniste, un biais logique grave.

Brouwer remplace en effet la dichotomie vrai/faux (qui suppose qu’on peut passer de la contradiction d’une proposition à l’affirmation de sa négation) par la dichotomie cohérent/contradictoire. Il se trouve que le cohérent est souvent vrai mais il n’y a pas coïncidence entre les deux pour autant.

Un élève de Brouwer, Heyting, a formalisé ces propositions philosophiques en logique. Gödel et Kolmogorov l’ont développé au XXème siècle. Curry, Howard et Gentzen ont montré que la logique intuitionniste et l’informatique sont très proches. Dans la même lignée, Jean-Yves Girard (logicien français, vivant) affirme que la logique intuitionniste est une logique à part entière.

Selon eux, Brouwer a découvert une logique structurellement féconde, qui colle plus au processus de découverte et de compréhension humain (cf. cours sur les différences entre la logique classique et les modes d’argumentation habituels).


Les différences d’interprétations

Comment interpréter A→B ?

Selon la logique classique, on a : (A→B)↔(¬A∨B). Mais, pour Brouwer, ce n’est pas acceptable. En effet, dire « A→B » c’est, selon lui, dire qu’on a une méthode qui transforme une preuve de A en une preuve de B. Dire « ¬A∨B » c’est dire qu’on dispose d’une preuve de ¬A ou d’une preuve de B. Il faut donc avoir au moins une preuve de ¬A ou de B pour affirmer leur disjonction. Or « A→B » affirme qu’on a une méthode de transformation des preuves, pas qu’on a effectivement une preuve de ¬A ou une preuve de B. L’équivalence retenue par la logique classique ne peut donc pas être acceptée.

Comment interpréter A∨¬A ?

Selon Brouwer, l’équivalence A∨¬A n’est pas acceptable non plus. En effet, comme on l’a vu avec l’exemple de Socrate, ou comme on le constate dans le cas des conjectures mathématiques qui ne sont démontrées qu’au fil du temps, avoir une preuve de ¬A n’équivaut pas à avoir un preuve de A, et inversement.

Comment interpréter ¬∀xPx→∃x¬Px ?

En logique classique on peut déduire de ¬∀xPx que ∃x¬Px. Or, selon Brouwer, ce n’est pas parce qu’on a démontré qu’il est impossible que tous soient P, qu’on a exhibé celui qui ne l’est pas. L’intuitionniste ne se permet pas de considérer un individu sans le voir : s’il ne voit, il ne croit pas. A l’inverse, le platoniste croit même s’il ne voit pas. Différemment, quand il a découvert les transfinis, Cantor a écrit à Dedekind : je le vois mais ne le crois pas.

Comment interpréter ¬(A∧B)↔(¬A∨¬B) ?

Pour Brouwer, ¬A∨¬B→¬(A∧B) est acceptable, mais pas l’inverse (comme le suppose le signe d’équivalence) : on peut conclure le négatif du positif mais pas l’inverse.

Un "paradoxe" (au sens intuitif) de la logique classique : ∃x(Px→∀yPy)

Dans la logique classique, on a le point de vue de Dieu : tous les faits sont décidés. Donc, dans cet exemple, on a :

- Ou bien ∀yPy, ou bien ¬∀yPy (par application du principe du tiers-exclu)
- Si on a ∀yPy, le conséquent est vrai, et l’implication aussi
- Si on ¬∀yPy, alors on a ∃y¬Py. Donc, en considérant ce y, l’antécédent est faux, et l’implication vraie.

C’est un résultat contre-intuitif mais conforme aux principes de la logique classique. Pour les intuitionnistes, on ne peut pas déduire une affirmation d’existence du néant de l’incohérence.

Reste A→¬¬A, qui est quand même acceptable selon Brouwer.

Gödel, en 1931, démontre que la perfection d'un "monde" mathématique n'est pas accessible par les méthodes formelles "dédiées à" (i.e. axomatisant) ce monde. Il est platonisant à sa manière : il pense que le monde mathématique est parfait, mais que l’homme ne peut pas totalement y accéder par des méthodes formelles fixées (ce qui rejoint un peu la critique intuitionniste). Gödel montre qu’on peut trouver des vérités auxquelles on ne peut accéder par des axiomes fixés (il faut étendre d’autant, à chaque fois, les axiomes). Il apporte la preuve que dans un système arithmétique, on ne peut pas accéder à toutes les vérités arithmétiques. Le geste intuitionniste a donc eu un caractère "prophétique", annonçant ce décalage. Gödel a aussi montré qu’on pouvait coder la logique classique dans la logique intuitionniste.