Un programme de recherche et une relation qui classent les théorèmes mathématiques en identifiant les plus faibles sous-systèmes de l'arithmétique du second ordre qui sont équivalents à ces théorèmes sur une théorie de base faible ; il étudie quels axiomes sont nécessaires et suffisants pour démontrer des résultats particuliers.

Principe

Le principe organisateur est l'équivalence sur une théorie de base (typiquement RCA_0) : pour un théorème donné T on trouve un sous-système S tel que T est démontrable à partir de S et S est démontrable à partir de T sur la base, renversant ainsi la direction habituelle de la preuve pour déterminer la force axiomatique minimale.

Démonstration

Une démonstration standard montre que de nombreux théorèmes ordinaires tombent dans une petite hiérarchie : par exemple, certains énoncés combinatoires ou analytiques sont équivalents sur la base à WKL_0 ou ACA_0, ce qui signifie que chaque principe se déduit de l'autre dans le cadre choisi.

Mauvaise application

Appliquer la classification de la reverse mathematics sans fixer clairement une théorie de base ou interpréter à tort l'équivalence comme valable dans tous les contextes (il s'agit d'équivalence sur la base choisie), ou supposer que le programme mesure des engagements ontologiques plutôt que la force proof-théorique ou axiomatique dans ce cadre formel.

Conséquence

La reverse mathematics fournit une taxonomie des théorèmes selon leurs exigences proof-théoriques, clarifie quels axiomes sont nécessaires pour des résultats standards, et éclaire les débats fondateurs en montrant que beaucoup de théorèmes n'exigent que des sous-systèmes faibles tandis que d'autres requièrent des principes plus forts de compréhension ou de choix.

Inversion

Inverser l'approche vers l'analyse fondationnelle habituelle revient au projet ordinaire de démontrer des théorèmes à partir d'axiomes choisis ; la reverse mathematics inverse cela en demandant quels axiomes découlent du théorème lui-même, faisant du théorème le point de départ pour la caractérisation axiomatique.

Limite

Opère dans le cadre de l'arithmétique du second ordre (ou variante choisie) relative à un système de base spécifié ; exclut des conclusions sur la nécessité en mathématiques informelles sans traduction dans le langage formel et dépend des choix de codage et de formulation.

Tension sémantique

La reverse mathematics entre en tension avec des programmes fondateurs qui privilégient des mesures différentes (axiomes d'existence d'ensembles, cadres catégoriques, interprétabilité modèle-théorique) : des tensions surgissent quant à savoir si les cinq sous-systèmes centraux rendent compte de l'import philosophique des théorèmes hors codages arithmétiques.

Synthèse

La reverse mathematics consiste à déterminer les axiomes formels minimaux pour des théorèmes en prouvant des équivalences bilatérales sur une théorie de base, produisant une hiérarchie structurée qui révèle la force axiomatique précise requise pour de larges classes de résultats mathématiques.