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 ».
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, dont l'introduction a très fortement inspiré cet article.
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.
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.
Discrete mathematics is a discipline with applications to almost all areas of study. It provides a set of indispensable tools to computer science in particular. This course reviews (familiar) topics a
Set Theory as a foundational system for mathematics. ZF, ZFC and ZF with atoms. Relative consistency of the Axiom of Choice, the Continuum Hypothesis, the reals as a countable union of countable sets,
This course covers the statistical physics approach to computer science problems, with an emphasis on heuristic & rigorous mathematical technics, ranging from graph theory and constraint satisfaction
En logique mathématique, l'arithmétique du second ordre est une théorie des entiers naturels et des ensembles d'entiers naturels. Elle a été introduite par David Hilbert et Paul Bernays dans leur livre Grundlagen der Mathematik. L'axiomatisation usuelle de l'arithmétique du second ordre est notée Z2. L'arithmétique de second ordre a pour conséquence les théorèmes de l'arithmétique de Peano (du premier ordre), mais elle est à la fois plus forte et plus expressive que celle-ci.
In proof theory, ordinal analysis assigns ordinals (often large countable ordinals) to mathematical theories as a measure of their strength. If theories have the same proof-theoretic ordinal they are often equiconsistent, and if one theory has a larger proof-theoretic ordinal than another it can often prove the consistency of the second theory. The field of ordinal analysis was formed when Gerhard Gentzen in 1934 used cut elimination to prove, in modern terms, that the proof-theoretic ordinal of Peano arithmetic is ε0.
Primitive recursive arithmetic (PRA) is a quantifier-free formalization of the natural numbers. It was first proposed by Norwegian mathematician , as a formalization of his finitistic conception of the foundations of arithmetic, and it is widely agreed that all reasoning of PRA is finitistic. Many also believe that all of finitism is captured by PRA, but others believe finitism can be extended to forms of recursion beyond primitive recursion, up to ε0, which is the proof-theoretic ordinal of Peano arithmetic.
Katznelson's Question is a long-standing open question concerning recurrence in topological dynamics with strong historical and mathematical ties to open problems in combinatorics and harmonic analysis. In this article, we give a positive answer to Katznel ...
At the core of the contribution of this dissertation there is an augmented reality (AR) environment, StaticAR, that supports the process of learning the fundamentals of statics in vocational classrooms, particularly in carpentry ones. Vocational apprentice ...
Grigorchuk and Medynets recently announced that the topological full group of a minimal Cantor Z-action is amenable. They asked whether the statement holds for all minimal Cantor actions of general amenable groups as well. We answer in the negative by prod ...