logique (suite)

À la base de la conception hilbertienne, on trouve la conviction que les symboles et les opérations sur ces symboles constituent le noyau central irréductible des mathématiques. La réalisabilité d’un système axiomatique ne peut être établie dans tous les cas par la méthode qui consiste à en exhiber une réalisation. D’où la nécessité de recourir à une démonstration de consistance, c’est-à-dire à une démonstration du fait qu’aucune contradiction ne peut être déduite des axiomes. Tel est le problème qui deviendra chez Hilbert le problème central et auquel s’identifiera en quelque sorte le problème dit « du fondement des mathématiques » : donner, pour chaque branche des mathématiques, une démonstration du fait que les procédés de démonstration qui y sont admis ne produiront jamais à la fois comme théorèmes une proposition et sa négation. Pour réaliser ce programme. Hilbert constitue ce qu’il appelle une « théorie de la démonstration ». Le principe en est le suivant : toute théorie mathématique peut être mise aujourd’hui sous la forme d’un système rigoureusement formalisé, c’est-à-dire d’un ensemble de formules qui ne se distinguent des formules mathématiques habituelles que par le fait qu’en plus des symboles ordinaires elles comportent certains symboles logiques. Une démonstration est une suite de formules symboliques dont chacune ou bien est un axiome, ou bien est obtenue à partir de formules précédentes à l’aide de règles d’inférence préalablement spécifiées. D’où la possibilité de faire des démonstrations elles-mêmes l’objet d’une étude mathématique : à la mathématique ordinaire, ainsi formalisée, vient s’ajouter une métamathématique, dans laquelle les démarches de la première sont considérées uniquement en tant qu’elles représentent des opérations sur des formes écrites. Il est bien spécifié qu’à la différence de la mathématique formelle, dont elle doit examiner et justifier les démonstrations, la métamathématique ne doit utiliser pour sa part que des méthodes de démonstration ayant un caractère intuitif et rigoureusement finitaire.

Pour certains systèmes élémentaires, la démonstration de consistance a pu être obtenue sans trop de difficulté. Mais pour tous les systèmes d’une certaine puissance, comme par exemple l’arithmétique des entiers naturels, une démonstration de consistance n’est possible que si l’on renonce à user de moyens strictement finitaires. C’est ainsi que G. Gentzen a pu donner en 1936 une démonstration de non-contradiction pour l’arithmétique en utilisant la méthode dite « d’induction transfinie ».

Alors que, si l’on excepte W. van Orman Quine (Mathematical Logic, 1940) et, dans une certaine mesure, J. Bardey Rosser, l’entreprise logiciste des Principia mathematika n’a pas eu de grands continuateurs directs, le formalisme est devenu, sous une forme implicite ou explicite, une tendance dominante en mathématiques et en philosophie des mathématiques. Dans les Éléments de mathématiques de Bourbaki*, qui représentent en un certain sens l’aboutissement et le point culminant de cette tendance, le problème du fondement des mathématiques est conçu comme devant être résolu par une combinaison appropriée de la logique symbolique et de la théorie des ensembles axiomatiques.

L’intuitionnisme

L’école intuitionniste a été fondée par Luitzen Egbertus Jan Brouwer (1881-1966), mais on peut lui rattacher également comme précurseurs directs des mathématiciens tels que H. Poincaré et Leopold Kronecker (1823-1891). Sur le problème du fondement des mathématiques, les intuitionnistes soutiennent un certain nombre de thèses qui sont directement opposées aux idées des formalistes. Pour eux, la mathématique est avant tout une création mentale qui se fonde sur l’intuition, en particulier l’intuition originaire de la suite des nombres naturels. En tant que telle, contrairement à ce qu’affirme le formalisme, elle est fondamentalement indépendante de tout langage, naturel ou symbolique, le langage ne pouvant lui servir en fin de compte que comme auxiliaire ou comme moyen de communication. L’existence mathématique ne se confond pas avec la simple non-contradiction logique : un objet mathématique ne peut être considéré comme existant que si nous avons le moyen de le construire effectivement par une procédure spécifiquement mathématique. Les intuitionnistes sont résolument hostiles à toute utilisation de l’infini actuel en mathématiques et ne donnent pas de sens à des expressions comme l’« ensemble de tous les nombres réels compris entre 0 et 1 ». Les mathématiques, qui ne dérivent pas de l’expérience, ne sont pas non plus, selon eux, sous la dépendance de la logique : c’est au contraire la logique qui constitue une spécification des mathématiques et doit être considérée en un certain sens comme de la mathématique appliquée. La logique classique, qui peut être utilisée en toute sécurité aussi longtemps qu’on se meut dans le fini, cesse d’être entièrement valide lorsqu’on considère des univers infinis. C’est ainsi, par exemple, que le principe du tiers exclu est valide dans le cas d’un ensemble fini : si E est un ensemble fini de nombres naturels, on peut décider en un nombre fini d’étapes intuitivement évidentes s’il contient ou non un nombre premier. Mais, si E contient un nombre infini de nombres naturels, l’assertion du fait que E contient un nombre premier ou n’en contient pas ne peut être considérée comme vraie que si l’on peut soit exhiber (ou donner le moyen de construire) un nombre premier qui soit élément de E, soit déduire une impossibilité de l’hypothèse qu’il en existe un. Arend Heyting (né en 1898) a donné en 1930 une axiomatisation de la logique intuitionniste, qui se distingue de la logique dite « classique » par le fait que certaines lois comme celle du tiers exclu et celle de la double négation n’y sont pas reçues comme universellement valides.

Lewis

Les « paradoxes » de l’implication matérielle ont amené Clarence Irving Lewis (1883-1964) à rechercher une conception de l’implication qui se rapporte davantage de ce que l’on veut dire lorsqu’on dit qu’une formule A « implique » une formule B. L’implication stricte de Lewis (désignée par le symbole «  ≺  ») correspond à peu près à la relation de déductibilité logique, en ce sens que, si A et B sont des expressions bien formées, A ≺ B sera vrai si, et seulement si, B est une conséquence logique de A. La première formulation satisfaisante du calcul propositionnel avec implication stricte a été donnée en 1920. Le livre écrit par Lewis en collaboration avec C. H. Langford, Symbolic Logic (1932), qui traite la question en détail, est devenu un ouvrage de référence sur la logique modale et le point de départ de la plupart des travaux ultérieurs sur cette question.