Voir la source de Fondements des mathématiques

{{Confusion|Grundlagen der Mathematik}}[[Image:Russell, Whitehead - Principia Mathematica to 56.jpg|200px|right|thumb|Les ''[[Principia Mathematica]]'' d'[[Alfred North Whitehead]] et [[Bertrand Russell]] : une tentative de fonder les mathématiques dans la perspective [[logicisme|logiciste]], qui a joué un rôle important dans l'histoire des 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 points de vue sur la nature des mathématiques ==

=== Le logicisme ===
Le [[logicisme]] a été prôné notamment par [[Gottlob Frege]] et [[Bertrand Russell]]<ref>{{Ouvrage |langue=fr |prénom1=Vernant, Denis, |nom1=1948- |lien auteur1=Denis Vernant |titre=La philosophie mathématique de Bertrand Russell |éditeur=Vrin |lieu=Paris |année=1993 |pages totales=512 |isbn=2-7116-1141-8 |isbn2=9782711611416 |oclc=413557229 |lire en ligne=https://www.worldcat.org/oclc/413557229 |consulté le=2019-02-06}}</ref>. La [[Mathématiques pures|mathématique pure]] présente deux caractéristiques : ''la généralité de son discours'' {{incise|la considération des particuliers existants est exclue}} et ''la déductibilité'' du discours mathématique {{incise|les [[Inférence (logique)|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 [[Classe (mathématiques)|classes]] (deux classes ont le même nombre s’il est possible d’instaurer entre leurs éléments respectifs une relation [[bijection|bijective]]). Le logicisme a rencontré néanmoins, à ses débuts, de réelles difficultés en tant qu’il s'engage [[Ontologie (philosophie)|ontologiquement]] par rapport aux classes. La théorie des classes avait conduit à des [[Paradoxe de Russell|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 [[Théorie axiomatique#Théorie récursivement axiomatisable|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 [[Luitzen Egbertus Jan Brouwer|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<ref>On suppose par exemple qu'il n'existe pas de nombre réel satisfaisant une certaine propriété, on en déduit une contradiction et on conclut par réduction à l'absurde qu'un tel réel doit exister ; une démonstration de cette forme ne donne aucune indication sur la façon dont on peut calculer un tel réel. Pour un intuitionniste on a juste démontré que l'existence d'un tel réel n'était pas contradictoire, mais on n'a pas démontré l'existence proprement dite.</ref>. 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 {{refnec|et a accueilli avec scepticisme sa formalisation donnée ultérieurement par [[Arend Heyting]]}}<ref>{{Ouvrage |langue=fr |prénom1=Largeault, |nom1=Jean. |lien auteur1=Jean Largeault |titre=Intuition et intuitionisme |éditeur=J. Vrin |lieu=Paris |année=1993 |pages totales=240 |isbn=2-7116-1155-8 |isbn2=9782711611553 |oclc=29897047 |lire en ligne=https://www.worldcat.org/oclc/29897047 |consulté le=2019-02-06}}</ref>.

== Les fondements de la géométrie ==
L’œuvre de [[David Hilbert|Hilbert]] est très représentative de la [[crise des fondements]] qui s’est produite en mathématiques pendant le [[XIXe siècle|XIX{{e}}]] et au début du {{XXe 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, non pas au sens où l’[[Axiome d'Euclide|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’[[axiome]]s qui n’avaient jamais été explicités. À la suite des travaux de [[Moritz Pasch|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, {{refnec|les règles de raisonnement admises étaient encore laissées dans l’ombre.}} D’autre part, un des axiomes de la géométrie, relatif à la [[Continuité (mathématiques)|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 [[Georg Cantor|Cantor]].

== Les fondements de l’analyse et la théorie des ensembles ==
L’[[analyse (mathématiques)|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 [[nombre réel|nombres réels]]. Depuis les découvertes de [[Isaac Newton|Newton]] et [[Leibniz]], il avait fallu dépasser le cadre des ''[[Éléments d'Euclide]]''.

Les mathématiciens du {{s-|XIX}}, notamment [[Augustin Louis Cauchy|Cauchy]] et [[Karl Weierstrass|Weierstrass]], pour l'analyse proprement dite, puis [[Richard Dedekind|Dedekind]] et [[Georg Cantor|Cantor]] ont donné une formulation précise de principes qui permettent de raisonner avec rigueur et exactitude sur les [[Nombre réel|nombres réels]]. Ceux-ci sont définis par Dedekind comme des couples d'ensembles de [[Nombre rationnel|nombres rationnels]], les [[coupure de Dedekind|coupures de Dedekind]]. [[Giuseppe Peano|Peano]] a établi des axiomes et des méthodes formelles pour développer  l’[[arithmétique]] de manière logiquement rigoureuse, suffisante pour fonder la [[théorie des nombres]] rationnels.

La théorie des ensembles de Cantor, bien que non formalisée, semblait constituer cependant le cadre idéal, paradisiaque selon l’expression de Hilbert, pour fonder l’analyse et plus généralement les mathématiques. De son côté, [[Gottlob Frege|Frege]] avait formulé des règles formelles précises et explicites pour une théorie logique destinée à fonder les mathématiques, offrant l'espoir d'une base solide.

Cependant, cette base a rapidement montré 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), a révélé l'incohérence de ces deux théories.
([[Bertrand Russell|Russell]] a initialement donné son paradoxe dans le cadre de la théorie de [[Gottlob Frege|Frege]]<ref>{{Ouvrage |langue=en |prénom1=Giaquinto, M. |nom1=(Marcus) |titre=The search for certainty |sous-titre=a philosophical account of foundations of mathematics |éditeur=Clarendon Press |lieu=Oxford |année=2002 |pages totales=304 |isbn=0-19-875244-X |isbn2=9780198752448 |isbn3=9781280914287 |oclc=48053880 |lire en ligne=https://www.worldcat.org/oclc/48053880 |consulté le=2019-02-06}}</ref>).

Des solutions pour éviter ces paradoxes furent rapidement élaborées. Russell, dans les ''[[Principia Mathematica]]'', a introduit la notion de ''types'' pour stratifier les [[Prédicat (logique mathématique)|prédicat]]s, empêchant ainsi l’écriture d'ensembles s’appartenant à eux-mêmes. [[ZFC|Zermelo]], quant à lui, a restreint la définition des ensembles par ''compréhension'',  excluant ainsi les ensembles définis par la propriété de ne pas s'appartenir à eux-mêmes.

La question restait de savoir si ces nouvelles théories pouvaient éviter de générer d'autres paradoxes.

== Le programme de Hilbert ==
{{article détaillé|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 [[problèmes de Hilbert|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 de base est la suivante : tant que l'on manipule des entités finies, les mathématiques sont sûres. L'arithmétique élémentaire (dans un sens à préciser) est également sûre. Pour justifier l'utilisation d'objets abstraits ou idéaux, notamment infinis, il suffit de démontrer que la théorie qui les utilise est cohérente. Toutefois, cette cohérence doit être prouvée par des moyens finitaires. Cela permet d'affirmer l'existence de ces objets. C'est la position formaliste, à ne pas confondre avec le [[finitisme]], pour lequel 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 [[fonction récursive primitive|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 [[Kurt Gödel|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 ==
{{À recycler|date=mai 2020|thème=mathématiques}}
Il ne faudrait pas confondre [[formalisme]], et méthode formelle {{pas clair}}. 
La méthode formelle est essentielle pour comprendre les mathématiques contemporaines {{refsou}}.

Définir une théorie formelle, c'est {{refsou}}:
* 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  {{refnec}}: 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 {{refnec}}.

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 {{refnec}}. Toutes les connaissances mathématiques peuvent être prouvées avec ces règles et des [[axiome]]s convenablement choisis {{refnec}}.

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. <br />
De même, <math>\mathbb N </math> peut être construit à partir d'ensembles comme suit : 
* <math> 0 = \varnothing </math> 
* <math> \forall n  (n + 1 = n \cup \{ n \})</math> 
(voir à ce sujet l'article sur la [[construction entiers naturels|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 '''[[ZFC|théorie axiomatique des ensembles]] « standard »''' comporte neuf ''axiomes''. Ces axiomes ont été énoncés par [[Ernst Zermelo|Zermelo]] (1908) et complétés dans les années 1920 par [[Abraham Adolf Fraenkel|Fraenkel]] et [[Thoralf Skolem|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'[[Nicolas Bourbaki|association Bourbaki]] a été développée dans ce cadre axiomatique.
* La '''[[théorie des classes]]''', de [[John von Neumann|von Neumann]], [[Kurt Gödel|Gödel]] et [[Paul Bernays|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 [[Willard van Orman Quine|Quine]]. {{refnec|Elle n'est pas très utilisée mais pourrait l’être davantage}}. 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é]], [[grand cardinal|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 [[constructivisme (mathématiques)|constructivistes]] ou  [[intuitionnisme|intuitionnistes]].

== D'autres formalismes ==
* Diverses '''[[théorie des types|théories des types]]''' telles que
** la [[théorie des types]] de [[Alfred North Whitehead|Whitehead]] et [[Bertrand Russell|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 homotopique des types]] ({{en}} '''HoTT''')<ref>{{Lien web|1=LP18|langue=en|format=pdf|url=http://philsci-archive.pitt.edu/11081/1/Does_HTT_Provide_a_Foundation_public.pdf|titre=Does Homotopy Type Theory Provide a Foundation for Mathematics?|auteur=James Ladyman, Stuart Presnell|année=2018}}</ref>.

* La '''[[théorie des catégories]]''' : depuis les années 1960, certains auteurs, à la suite de [[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 [[constructivisme (mathématiques)|constructiviste]] qui emprunte à la fois à la théorie homotopique des types et à la théorie des catégories.

== Bibliographie ==
* {{Ouvrage |titre=Introduction to Metamathematics |éditeur=North-Holland |lieu=Amsterdam |année=1952 |pages totales=x+550 p.|sudoc=005505526 |présentation en ligne=https://books.google.com/books?id=HZAjPwAACAAJ}} {{commentaire biblio SRL|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}}.
* {{Ouvrage | titre=Mathematical logic | éditeur=Dover | année première édition=1967|année=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, {{date-|octobre 1992}}, {{ISBN|2228884839}}.
* {{Ouvrage |langue=en |auteur1=Stewart Shapiro (dir.) |titre=The Oxford Handbook of Philosophy of Mathematics and Logic |éditeur=Oxford University Press |lieu=Oxford ; New York |année=2005 (Réimpression 2007) |isbn= |oclc=949190300}}, {{ISBN|9780195325928}}.

== Références ==
{{Références|colonnes=}}

== Voir aussi ==
{{autres projets
  | wikiversity = Fondements des mathématiques
  | wikiversity titre = Fondements des mathématiques
}}
=== Articles connexes ===
* [[Logique mathématique]]
* [[Crise des fondements]]
* ''[[Grundlagen der Mathematik]]''
* ''[[Introduction à la philosophie mathématique]]''

=== Lien externe ===
[http://www.canal-u.tv/index.php/canalu/producteurs/universite_de_tous_les_savoirs/dossier_programmes/les_conferences_de_l_annee_2000/perspectives_sur_les_mathematiques_actuelles/les_fondements_des_mathematiques/ Conférence sur les fondements des mathématiques], par [[Jean-Yves Girard]], {{date-|17 juin 2002}}, [[Université de tous les savoirs]].

{{Portail|logique|mathématiques}}

[[Catégorie:Philosophie des mathématiques]]
[[Catégorie:Fondements des mathématiques]]
[[Catégorie:Logique]]