Mathématiques à rebours
Les mathématiques à rebours sont une branche des mathématiques qui pourrait être définie simplement par l'idée de « remonter aux axiomes à partir des théorèmes », contrairement au sens habituel (des axiomes vers les théorèmes). Un peu plus précisément, il s'agit d'évaluer la robustesse logique d'un ensemble de résultats mathématiques usuels en déterminant exactement quels axiomes sont nécessaires et suffisants pour les prouver.
Histoire
Le domaine a été créé par Harvey Friedman dans son article « Some systems of second order arithmetic and their use »[1].
Le sujet fut poursuivi entre autres par Stephen G. Simpson[2] et ses étudiants. Simpson a écrit l'ouvrage de référence sur le sujet, Subsystems of Second Order Arithmetic[3], dont l'introduction a très fortement inspiré cet article.
Principes
Le principe des mathématiques à rebours est le suivant : on considère un langage structuré et une théorie de base, trop faible pour prouver la plupart des théorèmes qui peuvent nous intéresser, mais quand même assez forte pour prouver l'équivalence de certaines assertions dont la différence est vraiment minime, ou pour établir certains faits considérés comme assez évidents (la commutativité de l'addition par exemple). Au-dessus de cette faible théorie de base, il existe une théorie complète (ensemble d'axiomes), assez forte pour prouver les théorèmes qui nous intéressent et dans laquelle l'intuition mathématique classique reste intacte.
Entre le système de base et le système complet, le mathématicien cherche les ensembles d'axiomes de robustesse intermédiaire, qui ne sont deux à deux probablement pas équivalent (dans le système de base) : chaque système ne doit pas seulement prouver tel ou tel théorème classique, mais doit aussi y être équivalent (dans le système de base). Cela assure que la robustesse logique du théorème a été précisément atteinte (au moins pour le langage structuré et le système de base) : un ensemble d'axiome plus restreint ne pourrait pas suffire à prouver le théorème, et il ne pourrait pas en impliquer un plus large.
Le principe part donc du système complet au système de base tout en relevant les axiomes ayant permis par le procédé réciproque l'obtention du système de base.
Notes et références
- (en) Proceedings of the International Congress of Mathematicians, Vancouver, B.C., 1974, vol. 1, p. 235–242. Canad. Math. Congress, Montreal, Que., 1975.
- (en) Page de S. G. Simpson à l'université d'État de Pennsylvanie.
- (en) Subsystems of Second Order Arithmetic, Perspectives in Mathematical Logic, Springer-Verlag, Berlin, 1999 (ISBN 3-540-64882-8).