PA⁻
PA⁻
定義
Ax1 $ (\forall x,y,z)[(x + y) + z = x + (y + z)]
Ax2 $ (\forall x, y)[x + y = y + x]
Ax3 $ (\forall x,y,x)[(x \cdot y) \cdot z = x \cdot (y \cdot z)]
Ax4 $ (\forall x,y)[x \cdot y = y \cdot x]
Ax5 $ (\forall x, y, z)[x \cdot (y + z) = x \cdot y + x \cdot z]
Ax6.1 $ (\forall x)[x + 0 = x]
Ax6.2 $ (\forall x)[x \cdot 0 = 0]
Ax7$ (\forall x)[x \cdot 1 = x]
Ax8 $ (\forall x,y,z)[x < y \to y < z \to x < z]
Ax9 $ (\forall x)[\lnot x < x]
Ax10 $ (\forall x,y)[x < y \lor x = y \lor y < x]
$ +, \cdotと順序の関係
Ax11 $ (\forall x, y, z)[x < y \to x + z < y + z]
Ax12 $ (\forall x, y, z)[x < y \to z \ne 0 \to x \cdot z < y \cdot z]
Ax13 $ (\forall x, y)[x < y \to (\exists z)[x + z = y]]
$ <はdiscrete, また$ 0は$ <最小元
Ax14.1 $ 0 < 1
Ax14.2 $ (\forall x)[0 < x \to 1 \le x]
Ax15 $ (\forall x)[0 \le x]