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\).