Mathématiques à rebours
| Image manquante Math.png | Cet article est une ébauche 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éfinit simplement par “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). Et 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.
Principes
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 moin pour le langage structuré et le système de base): un ensemble d'axiome plus réstreint ne pourrait pas suffir à prouver le théorème, et il ne pourrait pas en impliquer un plus large.