Qu'est ce qu'un mathématicien, (André Lichnerowicz)

L'intuitionnisme : où l'on construit une preuve

Le raisonnement par l'absurde n'est pas constructif ! La logique intuitionniste, au contraire, relie preuve construite et calcul.
par Alexandre 

À partir de la fin du XIXe siècle, le développement considérable des mathématiques conduit de nombreux chercheurs de cette discipline à s'interroger sur la nature du raisonnement mathématique. L'introduction de nouveaux objets toujours plus complexes et l'utilisation de méthodes de raisonnement toujours plus abstraites (comme l'axiome du choix, dont l'introduction par Ernst Zermelo fut suivie de débats houleux) nécessite bien plus qu'une simple remise à plat des principes mathématiques.
Il ne suffit pas de spécifier les axiomes que l'on se donne et les règles de raisonnement que l'on s'autorise, encore faut-il savoir pourquoi on considère tel ou tel axiome, et pourquoi on raisonne de telle ou telle manière.
Dans ce contexte, le jeune mathématicien hollandais Luitzen Brouwer bâtit à partir de 1907 une critique philosophique originale du raisonnement mathématique classique, auquel il reproche ses méthodes non constructives (on démontre qu'un être mathématique existe, mais on n'en construit pas d'exemple). En remplacement, il propose une méthode de raisonnement centrée sur la notion de « construction intuitive », qu'il dénomme finalement « intuitionnisme ».
De cette démarche, la plupart des contemporains de Brouwer – et encore aujourd'hui la majorité des mathématiciens – ont retenu qu'elle consistait à rejeter des principes logiques élémentaires, tels que le principe du tiers exclu (« ou A ou non-A ») et, ce qui revient au même, le raisonnement par l'absurde. Pourtant, loin d'amputer les mathématiques, l'intuitionnisme donne au contraire un caractère plus tangible aux objets mathématiques et renforce la notion de preuve.
Exclu, le tiers exclu !
Pour saisir la démarche de Brouwer, examinons pourquoi la logique classique n'est pas constructive : du point de vue de la prouvabilité, le comportement des connecteurs logiques tels que la conjonction « et », notée ∧, et la disjonction « ou », notée ~, est révélateur.
Traitons d'abord la conjonction. À partir d'une preuve d'une proposition A et d'une preuve d'une autre proposition B, il est possible, par simple assemblage, de constituer une preuve de la proposition A ∧ B (A et B sont vraies) : c'est la signification même de la conjonction. Réciproquement, à partir de toute preuve de la proposition A ∧ B, on peut déduire une preuve de A (puisque A est une conséquence logique de A ∧ B), ainsi qu'une preuve de B (par le raisonnement symétrique). En d'autres termes, la proposition A ∧ B est prouvable si et seulement si A est prouvable et B est prouvable.
Cette propriété est loin d'être anecdotique : elle exprime que les règles de démonstration qui régissent le comportement du connecteur ∧ se conforment à l'utilisation qu'on souhaite en faire. Il semble qu'une logique qui ne vérifierait pas cette propriété serait bonne à jeter.
Passons à la disjonction. À partir d'une preuve de la proposition A, on démontre la proposition A ~ B (A ou B est vraie), puisque A ~ B est une conséquence logique de A. De même on démontre la proposition A ~ B à partir d'une preuve de la proposition B. Le simple fait de disposer ou bien d'une preuve de A ou bien d'une preuve de B suffit à construire une preuve de A ~ B.
Qu'en est-il de la réciproque ? Est-il possible, à partir d'une preuve de la proposition A ~ B, de retrouver ou bien une preuve de A, ou bien une preuve de B ?
Étonnamment la réciproque est fausse en logique classique. Le principe du tiers exclu permet en effet de prouver certaines propositions de la forme A ~ B sans pour autant prouver ni A ni B. Pour nous en convaincre, examinons une proposition A qui est indécidable dans le formalisme, c'est-à-dire telle que ni A ni sa négation ¬A ne sont prouvables dans le système considéré (le théorème de Gödel permet de construire une telle proposition dans n'importe quelle théorie contenant l'arithmétique). Bien qu'aucune des deux propositions A et ¬A ne soit prouvable, leur disjonction A ~ ¬A est néanmoins prouvable… d'après le principe du tiers exclu ! L'encadré A fournit un exemple d'une telle preuve.
Le même problème surgit avec la quantification existentielle, notée ∃. Considérons une proposition de la forme « Il existe un objet x qui possède la propriété A », ce que l'on écrit en logique formelle ∃x A(x). S'il existe un terme t, dit « témoin », pour lequel la proposition A(t) est prouvable, alors on détient une preuve de la proposition ∃x A(x).
Réciproquement, on serait en droit d'attendre que pour chaque proposition prouvable de la forme ∃x A(x), il soit possible de trouver un terme t pour lequel la proposition A(t) est prouvable. Hélas il n'en est rien, car le tiers exclu permet de construire des formules A(x) pour lesquelles la proposition ∃x A(x) est prouvable, sans pour autant qu'il soit possible d'exhiber un objet t pour lequel la proposition A(t) est prouvable : l'encadré B en donne un exemple.
Ce comportement surprenant, en logique classique, de la disjonction et de la quantification existentielle incite les mathématiciens intuitionnistes à rejeter le tiers exclu. Pour les intuitionnistes, non seulement les objets mathématiques doivent conserver un caractère concret, mais aussi et surtout toute preuve de A ~ B doit contenir, au moins implicitement, une preuve de A ou une preuve de B, de même que toute preuve de ∃x A(x) doit contenir, au moins implicitement, un témoin t de cette existence accompagné d'une preuve de la proposition A(t).
Avec une telle exigence sur le contenu des preuves, l'intuitionnisme est loin...
Pour la science

Alain Connes - Espace-temps, nombres premiers, deux défis pour la géométrie