Peano's Axioms

Then you might want to read Douglas Hofstadter's famous "Gödel, Escher, Bach" which draws analogies between mathematics and music and in one of its playful dialogues does in fact feature things called "Piano Postulates".

(The conceit is that one of the characters in the dialogue interprets mathematical notation as music, and claims to have an immediate sense of whether any given melody is "beautiful" that in every case seems to correspond to the truth or falsehood of the proposition expressed -- but denies all awareness of any connection between these melodies and anything mathematical. He mentions in particular five short but elegant pieces called the "Piano Postulates", which are of course Peano's axioms[1]. It eventually becomes clear, though it's not stated directly, that the character in question knows perfectly well what the notation really means and is trying to pull a hoax on his interlocutor, but his bluff gets called.)

[1] Though I'm only now realising that the notation they're using isn't actually expressive enough for it to be possible to write down the induction axiom in it.

Theorem providers should be treated as interactive. I don't know how Lean works but I know how Isabelle works. Reading Isabelle proofs in plain text (e.g. in the seL4 verification repository on GitHub) is completely useless. However, when you open one in Isabelle's IDE, you can click on any point in the proof and show the internal state of the verifier - what the current statement being proved is, so you can see how the last tactic modified it. You can also search for names of theorems and axioms by matching templates (e.g. "?a*(?b+?c)=?d" will match the law of distributivity and maybe some other stuff)

> Gödel's incompleteness theorems have given mathematicians an identity crisis for nearly a century now.

I don't think this is at all true.

Another one is Presburger Arithmetic, which is Peano Arithmetic minus the multiplication. What makes it interesting (and useful) is that this removal makes the theory decidable.

https://en.wikipedia.org/wiki/Presburger_arithmetic

https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_t...

Maybe a roundabout answer to your question, but Peano's axioms are equiconsistent with many finite set theories (even ZFC without axiom of infinity), and I do think philosophically it makes more sense to say weak axiomatic set theory + predicate calculus forms building blocks of arithmetic[1]. The idea of "number" as conceived by Frege is an equivalence class on finite sets: A ~ B <-> there is a bijection, which is in fact a good way of explaining "counting with fingers" as an especially primitive building block of arithmetic:

  {index, middle, ring} ~ 
  {apple, other apple, other other apple} ~
  {1, 2, 3}

[1] In my view Peano axioms are the Platonic ideal of arithmetic, after the cruft of bijections and whatnot are tossed away. I agree this is splitting hairs.

Conway's Surreal Numbers https://en.wikipedia.org/wiki/Surreal_number#Arithmetic

There are many axiom systems for natural numbers. My favorites are 1. Heyting Arithmetic, and 2. In category theory, one can characterise the natural numbers and the initial algebra of the X |–> X+1. functor.