Peano Arithmetic

Peano Arithmetic is a particular set of axioms and rules which allow you to prove theorems about the natural numbers.

These rules were formulated by the Italian mathematician Giuseppe Peano in 1889. They can be expressed as follows:

Let our language consist of the symbols $\left\{\right(,),\wedge ,\vee ,\neg ,\to ,\leftrightarrow ,\in ,\forall ,\exists ,=,+,\cdot ,O,S,N\}$ and an infinite set of variable symbols, which we will denote as $x,y,z,\dots$ (since three symbols is usually enough to denote infinitely many symbols).

We would like to interpret these symbols as representing our intuitive notions of logical and arithmetical operators, interpreting $O$ as the number 0, $S$ as the successor operation (thus $SO$ represents 1, $SSO$ represents 2, etc), and $N$ as the set of natural numbers.

We would furthermore like to create some formal rules such that we can derive certain true statements of arithmetic, like $SO+SO=SSO$ or $\forall x\in NSx\cdot Sx=x\cdot x+SSO\cdot x+SO$, but not derive false statements like $\exists x\in NSSO\cdot x=SSSO$.