Fondements des mathématiques

Les fondements des mathématiques sont les principes de la philosophie des mathématiques sur lesquels est établie cette science.

Les Principia Mathematica d'Alfred North Whitehead et Bertrand Russell : une tentative de fonder les mathématiques dans la perspective logiciste, qui a joué un rôle important dans l'histoire des fondements des mathématiques.

Les points de vue sur la nature des mathématiques

Le logicisme

Le logicisme a été prôné notamment par Gottlob Frege et Bertrand Russell. La mathématique pure présente deux caractéristiques : la généralité de son discours — la considération des particuliers existants est exclue — et la déductibilité du discours mathématique — les inférences qui structurent le discours mathématique sont des implications formelles (elles affirment non pas les propositions elles-mêmes, mais la nécessité de leur connexion). En ce que le discours mathématique ne prétend qu’à une vérité formelle, il est possible de réduire les mathématiques à la logique, les lois logiques étant les lois du « vrai ». Par exemple, la définition logique du nombre, loin d’être réduite à l’opération concrète de dénombrement d’objets, consiste en la référence à l’égalité numérique de deux classes (deux classes ont le même nombre s’il est possible d’instaurer entre leurs éléments respectifs une relation bijective). Le logicisme a rencontré néanmoins, à ses débuts, de réelles difficultés en tant qu’il s'engage ontologiquement par rapport aux classes. La théorie des classes avait conduit à des paradoxes logiques maintenant résolus mais qui avaient mis au jour la nécessité de clarifier les axiomes.

Le formalisme

Le formalisme est soutenu par David Hilbert : les mathématiques se présentent comme une pure construction de l’esprit. La tâche des mathématiciens est de déduire des théorèmes à partir d’axiomes qui ne sont ni vrais ni faux. La validité ne repose plus que sur la structure des énoncés, et non sur la nature de ce dont ils parlent. La vérité des mathématiques est réduite à leur cohérence interne, la non-contradiction des propositions. Le débat sur cette conception formaliste a été relancé par le théorème d'incomplétude de Gödel qui affirme que tout système formel cohérent et récursif contenant l'arithmétique, possède une proposition qui n’est ni démontrable, ni réfutable ; de plus, cette proposition est cependant « vraie » au sens intuitif du terme : elle formalise en effet l'affirmation selon laquelle la théorie est cohérente, ce qu'on a supposé dès le départ.

L'intuitionnisme

L’intuitionnisme est défendu de manière paradigmatique par Brouwer : les mathématiques ont un fondement intuitif, c'est-à-dire que tous les objets des mathématiques sont des constructions de l'esprit humain. Selon la conception intuitionniste un nombre réel peut être représenté comme une suite infinie de décimales à condition de disposer d'un algorithme qui peut calculer chacune de ces décimales. Cette position a des conséquences importantes notamment sur le plan logique. En logique intuitionniste, on ne peut pas éliminer la double négation (alors que cela est possible en logique classique) : « non non p » ne se réduit pas à « p » ; sinon on pourrait démontrer l'existence d'objets sans pour autant construire ceux-ci. Il s’ensuit que « non p ou p » n'est pas un théorème. Brouwer concevait l'intuitionnisme comme un positionnement philosophique sur les mathématiques et a accueilli avec scepticisme sa formalisation donnée ultérieurement par Arend Heyting^{[réf. nécessaire]}.

Les fondements de la géométrie

L’œuvre de Hilbert est très représentative de la crise des fondements qui s’est produite en mathématiques pendant le XIX^e et au début du XX^e siècle.

Hilbert, comme d’autres logiciens et mathématiciens de son temps, s’est rendu compte que la géométrie euclidienne était incomplète, pas au sens où l’axiome des parallèles n’y est pas déductible, mais parce que tous les géomètres depuis Euclide se servent dans leurs preuves d’axiomes qui n’avaient jamais été explicités. À la suite des travaux de Pasch, Hilbert a donné une formulation presque complète de la géométrie euclidienne, dans son livre Les Fondements de la géométrie, pour laquelle aucun axiome géométrique n’était laissé dans l’ombre.

Ce programme de fondation de la géométrie n’était cependant pas achevé pour deux raisons. D’une part, les règles de raisonnement admises étaient encore laissées dans l’ombre.^{[réf. nécessaire]} D’autre part, un des axiomes de la géométrie, relatif à la continuité de l’espace, posait des problèmes d’interprétation associés à ceux de la définition des nombres réels et de la théorie des ensembles de Cantor.

Les fondements de l’analyse et la théorie des ensembles

L’analyse, que l’on peut aussi appeler calcul infinitésimal, ou calcul différentiel et intégral, repose maintenant sur la définition de l’ensemble des nombres réels. Depuis les découvertes de Newton et Leibniz, il avait fallu sortir du cadre des Éléments d'Euclide.

Les mathématiciens du XIX^e siècle, notamment Cauchy et Weierstrass, pour l'analyse proprement dite, puis Dedekind et Cantor ont donné une formulation précise de principes qui permettent de raisonner avec rigueur et exactitude sur les nombres réels. Ceux-ci sont définis par Dedekind comme des couples d'ensembles de nombres rationnels, les coupures de Dedekind. Peano a donné des axiomes et des méthodes formelles pour développer d’une façon logiquement rigoureuse l’arithmétique et celle-ci suffit pour fonder la théorie des nombres rationnels.

La théorie des ensembles de Cantor, qui n'était pas vraiment formalisée, semblait cependant le cadre idéal, paradisiaque selon l’expression de Hilbert, pour fonder l’analyse et plus généralement les mathématiques. Frege, de son côté avait donné des règles formelles précises et explicites pour une théorie logique qui devait permettre de fonder les mathématiques. On pouvait espérer une base solide.

Mais cette base n'a pas tardé à montrer ses faiblesses. La découverte du paradoxe de Burali-Forti (l'ensemble de tous les ordinaux est bien ordonné, ce bon ordre est supérieur à tous les ordinaux, donc à son propre ordinal), puis celle du paradoxe de Russell, proche sur le principe mais nettement plus simple (l'ensemble des ensembles qui n'appartiennent pas à eux-mêmes est un ensemble, il ne peut ni s'appartenir, ni ne pas s'appartenir à lui-même), montrent l'incohérence de ces deux théories. (Russell a donné son paradoxe initialement pour la théorie de Frege).

Des solutions pour éviter ces paradoxes furent rapidement trouvées. L'une, initiée par Russell, et développée dans les Principia Mathematica, stratifie les prédicats grâce à la notion de type : on ne peut plus écrire qu'un ensemble n’appartient pas à lui-même. L'autre, initiée par Zermelo, restreint la définition des ensembles par compréhension, c'est-à-dire par une propriété de ses éléments : la propriété de ne pas appartenir à soi-même ne définit plus un ensemble.

Mais pouvait-on s'assurer que l'on ne puisse pas dériver de nouveaux paradoxes dans ces théories ?

Le programme de Hilbert

Pour répondre à la crise des fondements des mathématiques, David Hilbert avait conçu un programme dont il établit les prémices en 1900 dans l'introduction à sa célèbre liste de problèmes, le second problème étant justement celui de la cohérence de l'arithmétique. Il développe ce programme avec ses collaborateurs, parmi lesquels Paul Bernays et Wilhelm Ackermann, essentiellement dans les années 1920. L'idée est grossièrement la suivante.

Tant que l'on manipule le fini, les mathématiques sont sûres. L'arithmétique élémentaire (en un sens qui doit se préciser) est sûre. Pour justifier l'utilisation d'objets abstraits ou idéaux, en particulier infinis, il suffit de montrer que la théorie qui les utilise est cohérente, mais bien sûr cette cohérence doit elle-même être démontrée par des moyens finitaires. On peut alors affirmer l'existence de ces objets. C'est la position formaliste (à ne pas confondre avec le finitisme qui considère que seules les constructions directement finitaires ont un sens).

Le système dans lequel on pourrait formaliser les mathématiques finitaires n'est pas clair. À l'époque, il semble que Hilbert pensait, sans l'avoir explicitement formalisé, à un système plus faible que l'arithmétique de Peano, l'arithmétique primitive récursive : toutes les définitions de fonctions récursives primitives sont dans le langage, la récurrence est restreinte aux formules sans quantificateurs (disons aux égalités pour faire simple), donc très immédiate. Peu importe en fait : le second théorème d'incomplétude de Gödel, montre que l'on ne pourra même pas prouver dans la théorie arithmétique en question sa propre cohérence, et donc certainement pas celle de théories plus fortes qui assureraient la fondation des mathématiques.

Le programme de Hilbert n'est donc pas réalisable, en tout cas pas sans une révision drastique. Des logiciens comme Gentzen, et Gödel lui-même, ont pensé à rétablir ce programme en étendant la notion de méthodes finitaires, celles-ci ne pouvant cependant pas être définies une fois pour toutes par une théorie toujours à cause du second théorème d'incomplétude. Ainsi, Gentzen a donné en 1936 une preuve de cohérence de l'arithmétique de Peano dans un système forcément plus fort, où l'on raisonne par induction sur un ordre bien fondé (dénombrable mais plus grand que l'ordre des entiers), mais où l'induction est cependant restreinte à des formules sans quantificateurs, donc plus « immédiate ». Si l'intérêt mathématique des méthodes mises en œuvre par Gentzen ne fait aucun doute, l'interprétation de ses preuves de cohérence, en tant que preuves « absolues » (ce sont bien sûr indubitablement des preuves de cohérence relative) reste très discutable.

Il reste que, malgré son échec, le programme de Hilbert a joué un rôle décisif dans le développement de la logique mathématique moderne.

La méthode formelle

Il ne faudrait pas confondre formalisme, et méthode formelle ^[pas clair]. La méthode formelle est essentielle pour comprendre les mathématiques contemporaines ^{[réf. souhaitée]}.

Définir une théorie formelle, c'est ^{[réf. souhaitée]}:

• se donner des symboles (a, b, c, =, +, ≥, <, etc.)  ;
• se donner une syntaxe pour construire des « phrases ». Par exemple on peut écrire a≥b mais pas a b ≥ ;
• se donner une méthode pour déduire des phrases à partir d'autres phrases. Par exemple, si on a a≥b et b≥c alors on a aussi la « phrase » a≥c.

Définir une théorie de façon formelle est essentiel pour en donner des propriétés ^{[réf. nécessaire]}: cohérence ou incohérence, complétude ou incomplétude etc. Tant qu’on n'a pas formalisé une théorie, on ne sait pas exactement si une formule appartient ou non à la théorie ^{[réf. nécessaire]}.

Les règles de déduction de la logique traditionnelle sont désormais complètement connues et formalisées au sein de la logique mathématique ^{[réf. nécessaire]}. Toutes les connaissances mathématiques peuvent être prouvées avec ces règles et des axiomes convenablement choisis ^{[réf. nécessaire]}.

C'est probablement dans cette catégorie que l'on ^[Qui ?] doit classer les mathématiques à rebours d'Harvey Friedman.

Les théories des ensembles

Les mathématiques actuelles sont fondées sur la notion d' ensemble. En fait, tout objet mathématique ou presque peut être défini comme un ensemble. Par exemple, le nombre 23 peut être défini comme un certain ensemble.
De même, $\mathbb {N}$ peut être construit à partir d'ensembles comme suit :

• $0=\varnothing$
• $\forall n(n+1=n\cup \{n\})$

(voir à ce sujet l'article sur la construction des entiers naturels).

Avec de telles définitions, ou d’autres semblables, toutes les connaissances mathématiques peuvent être prouvées à l’intérieur d’une théorie des ensembles. Leurs axiomes peuvent être considérés comme les principaux fondements des mathématiques (avec les règles de déduction du calcul des prédicats au premier ordre).

Plusieurs systèmes d’axiomes ont été proposés :

• La théorie axiomatique des ensembles « standard » comporte neuf axiomes. Ces axiomes ont été énoncés par Zermelo (1908) et complétés dans les années 1920 par Fraenkel et Skolem. Ils sont dits de Zermelo-Fraenkel et comprennent l'axiome du choix, d'où le sigle ZFC souvent employé pour désigner cette théorie. L'œuvre de l'association Bourbaki a été développée dans ce cadre axiomatique.
• La théorie des classes, de von Neumann, Gödel et Bernays (NGB). C’est une extension de ZFC qui lui est presque équivalente. Tous les théorèmes de ZFC sont des théorèmes de NGB. Inversement, tous les théorèmes de NGB qui ne mentionnent que les notions fondamentales de ZFC (c’est-à-dire les ensembles et non les classes) sont des théorèmes de ZFC. NGB convient mieux que ZFC pour formuler la théorie des catégories.
• La théorie du zigzag interdit de Quine. Elle n'est pas très utilisée mais pourrait l’être davantage^{[réf. nécessaire]}. Elle montre en particulier qu’on peut développer une théorie des ensembles sans exclure l’ensemble de tous les ensembles.
• D’autres théories, qui sont soit moins puissantes que les précédentes, parce qu’elles refusent les constructions ensemblistes trop audacieuses (théories constructivistes, intuitionnistes, finitaires, ...), soit plus puissantes parce qu’elles les complètent avec d’autres axiomes (axiome de constructibilité, axiomes des grands cardinaux, ...)

Parmi les mathématiciens, certains se contentent des axiomes ZF, et refusent l'axiome du choix (C), car ils considèrent que certaines de ses implications sont contre-intuitives. Certains mathématiciens refusent même ZF et la logique classique qui en est la base, car ils considèrent que tout doit être construit explicitement; c'est la raison pour laquelle on les appelle constructivistes ou intuitionnistes.

D'autres formalismes

• Diverses théories des types telles que
  • La théorie des types de Whitehead et Russell, exposée principalement dans les Principia Mathematica. Son formalisme est lourd (des dizaines de pages pour prouver des propositions qui peuvent paraître évidentes) et ses principes imposent beaucoup d’interdits entre les divers types dans le souci de ne pas reproduire l'équivalent du paradoxe de Russell. Outre sa grande importance historique parce qu’elle est la première formulation axiomatique, rigoureuse et cohérente des principes généraux des mathématiques, elle a, grâce à l'informatique, repris de la vigueur à la fin du XXe siècle et au début du XXIe et devient une discipline phare de la logique mathématique contemporaine et un fondement solide des mathématiques.
  • La théorie des types d'Alonzo Church qui invente le lambda calcul
  • La théorie des types intuitionniste de Per Martin-Löf
  • Le calcul des constructions ((en) CoC)
  • La théorie des types homotopiques ((en) HoTT)

• La théorie des catégories : depuis les années 1960, certains auteurs, à la suite de Francis William Lawvere, défendent l'usage de la théorie des catégories en lieu et place de la théorie des ensembles comme fondement des mathématiques.

• Les fondements univalents : une théorie constructiviste qui emprunte à la fois à la théorie des types homotopiques et à la théorie des catégories.

Bibliographie

• Introduction to Metamathematics, Amsterdam, North-Holland, 1952, x+550 (SUDOC 005505526, présentation en ligne) — Nombreuses réimpressions, en 1957, 1959, 1962, 1964, 1967, 1971, 1974, 1980, 1988, 1991, 1996, 2000, 2009 notamment par Wolters-Noordhoff (Groningen) (ISBN 0720421039), d'après la notice Sudoc. Nombreuses traductions.
• Mathematical logic, Dover, 1967 — Réimpression Dover reprint, 2001, (ISBN 0-486-42533-9). Traduction française par Jean Largeault, Logique mathématique, Armand Colin, 1971 ou Gabay 1987 (ISBN 2-87647-005-5).
• Jean Cavaillès, Méthode axiomatique et formalisme - Essai sur le problème du fondement des mathématiques, Paris, Hermann, 1938.
• Logique et fondements des mathématiques. Anthologie (1850 − 1914), recueil d'articles traduits en français et rassemblés sous la direction de François Rivenc, Payot, octobre 1992, (ISBN 2228884839).
• (en) Stewart Shapiro (dir.), The Oxford Handbook of Philosophy of Mathematics and Logic, Oxford ; New York, Oxford University Press, 2005 (réimpression 2007) (OCLC 949190300), (ISBN 9780195325928).

Voir aussi

Articles connexes

• Logique mathématique
• Crise des fondements
• Grundlagen der Mathematik
• Introduction à la philosophie mathématique

Lien externe

Conférence sur les fondements des mathématiques, par Jean-Yves Girard, 17 juin 2002, Université de tous les savoirs.