Defining a substraction in the standart signature of arithmetic

Question

I am answering the question, where I need to Formalize a claim: We are given the standart signature of arithmetic {0, s, +, *, <}, where I need to formalize a claim with "difference of (n+1)^2 - n", but I don't know how to define substraction. Any suggestions? I have tried with one negative number, but they have to be sequential.

Answer 1

You could try to define substraction ($-$) with: \begin{array}{rll} a-0 &= a \\ s(a)-s(b) & = a-b \\ 0-s(b) &\text{is undefined}\\ \end{array}

Answer 2

If you are working with the natural numbers, and thus cannot have negative numbers, you can define $x -y = 0$ for any $x <y$. To formalise this with one definitional axiom:

$$\forall x \forall y \forall z (z = x -y \leftrightarrow ((x < y \land z =0) \lor x = y +z))$$

But if this is just a one time formula to express '$y$ is the difference $(n+1)^2-n$', then you can use

$$y + n = (n + s(0))\cdot (n +s(0))$$

since for any $n$, $n < (n+1)^2$