First-order logic task with limited clauses

Question

I have the following axioms

1. The sum of a natural number x and 0 is equal to x.
2. The sum of a natural number x and the successor of a natural number y is equal to the successor of the sum of x and y.
3. The product of 0 and a natural number x equals 0.
4. The product of the successor of a natural number x and a natural number y is equal to the sum of (a) the product of x and y and (b) the natural number y itself.

I am trying to represent these in first-order logic. Easy, but here comes the problem: I am only allowed to use

• predicate with 3 arguments
• another predicate with 3 arguments
• one function with 1 argument
• one function with 0 arguments (= constant)

My first predicate is

Sumequal(x, y, z)

which returns true if x + y = z. I then would use the function with 1 argument as

successor(x)

which returns the result of x + 1. Finally my constant n would just be 0.

For Axiom (1) I can then say:

Sumequal(x, n, x)

Axiom (2) asks me to first calculate the sum of two integers and then calculate the successor. With the limitation of what I am allowed to use I can't find a formula for this one.

Are my defined predicates and functions even useful?

How could I solve the task?

Thanks!

Answer 1

Your choices for the predicates and functions are useful, and the problem is solvable yet not trivial.

For 2, your first approach would presumably be something like

$$sumequal(x,succ(y),s(sumequal(x,y,..????))$$

with the obvious problem that 1. you can't nest the predicate $sumequal$ into the function symbol $s$ and 2. you don't now how to refer to that thing meant by "???". What you want to express is something like "$succ(z)$ such that $z$ is the sum of $x$ and $y$", which already leads you to the solution.

The trick here - which, by the way, is a very central trick when it comes to writing logic programs in a relational programming language like Prolog, should you ever get in contact with that - is to "source out" the computation of the sum to a a separate statement, introduce a variable that represents the result of this computation, then use the same variable as the term for the function you wanted to embed the other computation in, and finally conjoin the formulas:

$$sumequal(x,succ(y),s(z)) ∧ sumequal(x,y,z)$$

Since you use the same variable $z$ in $s(z)$ and $sumequal(x,y,z)$, they refer to the same thing, and since the sum is, though now represented as merely a relation, still a function in the extensional sense that there will be only one unique value $z$ that satisfies the three-place predicate, and the two formulas are and-ed, i.e. potential candidates for $z$ must satisfy both requirements, $s(z)$ will be precisely the successor of that term which also the sum of $x$ and $y$.

4 works completely analogously.