Axiomes de Peano

vignette|Giuseppe Peano En mathématiques, les axiomes de Peano sont des axiomes pour l'arithmétique proposés initialement à la fin du par Giuseppe Peano, et qui connaissent aujourd'hui plusieurs présentations qui ne sont pas équivalentes, suivant la théorie sous-jacente, théorie des ensembles, logique du second ordre ou d'ordre supérieur, ou logique du premier ordre. Richard Dedekind avait proposé une formalisation assez proche, sous une forme non axiomatique. La définition axiomatique des entiers naturels de Peano peut être décrite par les cinq axiomes : L'élément appelé zéro et noté 0 est un entier naturel. Tout entier naturel n a un unique successeur, noté s(n) ou Sn qui est un entier naturel. Aucun entier naturel n'a 0 pour successeur. Deux entiers naturels ayant le même successeur sont égaux. Si un ensemble d'entiers naturels contient 0 et contient le successeur de chacun de ses éléments, alors cet ensemble est N. Le premier axiome permet de poser que l'ensemble N des entiers naturels n'est pas vide, le troisième qu'il possède un premier élément et le cinquième qu'il vérifie le principe de récurrence. De façon plus formelle, dire de (E, c, f) qu'il satisfait les axiomes de Peano, c'est dire qu'il satisfait les propriétés suivantes : E est un ensemble ayant c pour élément, f est une fonction de E dans lui-même, c ∉ , f est injective, Toute partie F de E contenant c et stable par f (c'est-à-dire telle que ⊂ F) est égale à E. La formulation de la propriété 5 contient une quantification sur les parties de E : une telle propriété est dite du second ordre. Une telle structure est un modèle des axiomes de Peano, vu comme axiomes en logique du second ordre. La formulation originale de Peano contenait d'autres axiomes, par exemple sur l'égalité, que l'on considère aujourd'hui comme faisant partie de la logique sous-jacente. L'arithmétique de Peano désigne souvent la « restriction » des axiomes de Peano au langage de l'arithmétique du premier ordre, c'est-à-dire le calcul des prédicats égalitaire avec pour signature {0, s, + , ∙}.