Mathématiques à rebours

Un article de Wikipédia, l'encyclopédie libre.

Cet article est une ébauche à compléter concernant les mathématiques, vous pouvez partager vos connaissances en le modifiant.

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.

Le domaine a été créé par Harvey Friedman dans son article “Some systems of second order arithmetic and their use” (Proceedings of the International Congress of Mathematicians (Vancouver, B.C., 1974), Vol. 1, pp. 235–242. Canad. Math. Congress, Montreal, Que., 1975).

Le sujet fut poursuivi entre autres par Stephen G. Simpson et ses étudiants. Simpson a écrit l'ouvrage de référence sur le sujet, Subsystems of Second Order Arithmetic (Perspectives in Mathematical Logic, Springer-Verlag, Berlin, 1999, ISBN 3-540-64882-8); dont l'introduction a très fortement inspiré cet article.

[modifier] Principes

[modifier] Généralités

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 consideré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 soit 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 suffir à 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.