Peano Arithmetic

Peano Arith­metic is a par­tic­u­lar set of ax­ioms and rules which al­low you to prove the­o­rems about the nat­u­ral num­bers.

Th­ese rules were for­mu­lated by the Ital­ian math­e­mat­i­cian Giuseppe Peano in 1889. They can be ex­pressed as fol­lows:

Let our lan­guage con­sist of the sym­bols $$\left\{(,),\wedge,\vee,\neg,\to,\leftrightarrow,\in,\forall,\exists,=,+,\cdot,O,S,N \right\}$$ and an in­finite set of vari­able sym­bols, which we will de­note as $$x, y, z, \dots$$ (since three sym­bols is usu­ally enough to de­note in­finitely many sym­bols).

We would like to in­ter­pret these sym­bols as rep­re­sent­ing our in­tu­itive no­tions of log­i­cal and ar­ith­meti­cal op­er­a­tors, in­ter­pret­ing $$O$$ as the num­ber 0, $$S$$ as the suc­ces­sor op­er­a­tion (thus $$SO$$ rep­re­sents 1, $$SSO$$ rep­re­sents 2, etc), and $$N$$ as the set of nat­u­ral num­bers.

We would fur­ther­more like to cre­ate some for­mal rules such that we can de­rive cer­tain true state­ments of ar­ith­metic, like $$SO+SO=SSO$$ or $$\forall x \in N\; Sx \cdot Sx = x\cdot x + SSO \cdot x + SO$$, but not de­rive false state­ments like $$\exists x\in N \; SSO\cdot x = SSSO$$.