Arithmétique des fonctions élémentaires - Elementary function arithmetic

« Arithmétique récursive élémentaire » réexpédie ici. Pour la classe de complexité de calcul, voir ELEMENTARY .

En théorie de la preuve , une branche de la logique mathématique , l'arithmétique des fonctions élémentaires ( EFA ), également appelée arithmétique élémentaire et arithmétique des fonctions exponentielles , est le système d'arithmétique avec les propriétés élémentaires habituelles de 0, 1, +, ×,  x y , ainsi que induction pour les formules avec quantificateurs bornés .

L'EFA est un système logique très faible, dont l'ordinal théorique de preuve est ω 3 , mais semble encore capable de prouver une grande partie des mathématiques ordinaires qui peuvent être énoncées dans le langage de l' arithmétique du premier ordre .

Définition

EFA est un système en logique du premier ordre (avec égalité). Sa langue contient :

  • deux constantes 0, 1,
  • trois opérations binaires +, ×, exp, avec exp( x , y ) généralement écrite sous la forme x y ,
  • un symbole de relation binaire < (Ceci n'est pas vraiment nécessaire car il peut être écrit en fonction des autres opérations et est parfois omis, mais est pratique pour définir des quantificateurs bornés).

Les quantificateurs bornés sont ceux de la forme ∀(x<y) et ∃ (x<y) qui sont des abréviations pour ∀ x (x<y)→... et ∃x (x<y)∧... manière.

Les axiomes de l'EPT sont

  • Les axiomes de l' arithmétique de Robinson pour 0, 1, +, ×, <
  • Les axiomes pour l'exponentiation : x 0 = 1, x y +1 = x y × x .
  • Induction pour les formules dont tous les quantificateurs sont bornés (mais qui peuvent contenir des variables libres).

La grande conjecture de Friedman

La grande conjecture de Harvey Friedman implique que de nombreux théorèmes mathématiques, tels que le dernier théorème de Fermat , peuvent être prouvés dans des systèmes très faibles tels que l'EFA.

L'énoncé original de la conjecture de Friedman (1999) est :

"Chaque théorème publié dans les Annals of Mathematics dont l'énoncé n'implique que des objets mathématiques finiaires (c'est-à-dire ce que les logiciens appellent un énoncé arithmétique) peut être prouvé dans EFA. EFA est le fragment faible de Peano Arithmetic basé sur les axiomes sans quantificateur habituels pour 0 , 1, +, ×, exp, ainsi que le schéma d' induction pour toutes les formules du langage dont tous les quantificateurs sont bornés."

Alors qu'il est facile de construire des déclarations arithmétiques artificielles qui sont vraies mais non prouvables en EFA, le point de la conjecture de Friedman est que les exemples naturels de telles déclarations en mathématiques semblent être rares. Quelques exemples naturels incluent des déclarations de cohérence de la logique, plusieurs déclarations liées à la théorie de Ramsey telles que le lemme de régularité de Szemerédi et le théorème mineur du graphe .

Systèmes associés

Plusieurs classes de complexité de calcul apparentées ont des propriétés similaires à celles de l'EFA :

  • On peut omettre le symbole de fonction binaire exp du langage, en prenant l'arithmétique de Robinson avec l'induction pour toutes les formules avec des quantificateurs bornés et un axiome énonçant grossièrement que l'exponentiation est une fonction définie partout. Ceci est similaire à l'EFA et a la même force théorique de preuve, mais est plus lourd à utiliser.
  • Il existe des fragments faibles d'arithmétique du second ordre appelés RCA*
    0     et WKL*
    0     qui ont la même force de cohérence que l'EFA et sont prudents par rapport à celui-ci pour Π0
    2    phrases, qui sont parfois étudiées en mathématiques inversées ( Simpson 2009 ).
  • L'arithmétique récursive élémentaire ( ERA ) est un sous-système de l'arithmétique récursive primitive (ARP) dans laquelle la récursivité est limitée aux sommes et aux produits bornés . Cela a aussi le même0
    2    phrases comme EFA, dans le sens où chaque fois que EFA prouve ∀x∃y P ( x , y ), avec P sans quantificateur, ERA prouve la formule ouverte P ( x , T ( x )), avec T un terme définissable dans ERA . Comme PRA, ERA peut être défini d'une manière entièrement sans logique, avec juste les règles de substitution et d'induction, et en définissant des équations pour toutes les fonctions récursives élémentaires. Contrairement à PRA, cependant, les fonctions récursives élémentaires peuvent être caractérisées par la fermeture sous composition et la projection d'un nombre fini de fonctions de base, et donc seul un nombre fini d'équations de définition est nécessaire.

Voir également

Les références

  • Avigad, Jeremy (2003), "Théorie des nombres et arithmétique élémentaire", Philosophia Mathematica , Série III, 11 (3) : 257-284, doi : 10.1093/philmat/11.3.257 , ISSN  0031-8019 , MR  2006194
  • Friedman, Harvey (1999), grandes conjectures
  • Simpson, Stephen G. (2009), Sous - systèmes d'arithmétique de second ordre , Perspectives in Logic (2e éd.), Cambridge University Press , ISBN 978-0-521-88439-6, MR  1723993