Link Search Menu Expand Document
Prog Lang & Comp

Axioms of Peano Arithmetic

  • (Ax1)    \(\forall x.\ \neg(0 = x+1)\)
  • (Ax2)    \(\forall x.\ \forall y.\ (x+1 = y+1 \Rightarrow x = y)\)
  • (Ax3)    \(\forall x.\ x+0 = x\)
  • (Ax4)    \(\forall x.\ \forall y.\ x + (y + 1) = (x + y) + 1\)
  • (Ax5)    \(\forall x.\ x * 0 = 0\)
  • (Ax6)    \(\forall x.\ \forall y.\ x * (y + 1) = (x * y) + x\)
  • (Ax7)    \(A(0) \wedge (\forall x.\ A(x) \Rightarrow A(x+1)) \Rightarrow (\forall x.\ A(x))\)