Peano Arithmetic is that branch of Mathematics having to do with the non-negative integers, the function of addition, and the less than relation.
Peano Arithmetic is more complicated than Modular Arithmetic in that we have infinitely many objects to consider, viz. the integers 0, 1, 2, 3, ... Since there are infinitely many such numbers, we need infinitely many terms to describe them in our language.
One way to get infinitely many terms is by expanding our vocabulary to include infinitely many symbols. Unfortunately, this would make the job of defining arithmetic impossible, as we would have to write out infinitely many sentences.
Fortunately, there is a better way. In particular, we can represent numbers using a single symbol (e.g. 0) and a single unary constructor (e.g. s). In this approach, we represent the number 0 with the symbol 0, and we represent every other natural number n by applying the constructor s exactly n times. For example, in this encoding, s(0) represents 1; s(s(0)) represents 2; s(s(s(0))) represents 3; and so forth. With this encoding, we automatically get an infinite set of ground terms.
Unfortunately, even with this representation, defining Peano Arithmetic is more challenging than defining Modular Arithmetic. We cannot write all of the facts to characterize addition and multiplication and so forth, because there are infinitely many cases to consider. For Peano Arithmetic, we must rely on view definitions, not just because they are more economical but because they are the only way we can characterize these concepts in finite space.
Let's look at the number predicate first. The rules shown here define the number relation in terms of 0 and s.
|number(s(X)) :- number(X)|
The next predicate holds of any natural number and the number that follows it. For example, we have next(0,s(0)) and next(s(0),s(s(0))) and so forth. We can define next in general as shown below.
|next(X,s(X)) :- number(X)|
Once we have number and next, we can define the usual arithmetic relations. For example, the following sentences define the add relation. Adding 0 to any number results in that number. If adding a number X to a number Y produces a number Z, then adding the successor of X to Y produces the successor of Z.
|add(0,Y,Y) :- number(Y)|
|add(s(X),Y,s(Z)) :- add(X,Y,Z)|
Using next, we can also define the less than relation in an analogous manner. A number X is less than a number Z if next holds of X and Z or if there is a number Y such that Y is the number after X and Y is less than Z.
|less(X,Z) :- next(X,Z)|
|less(X,Z) :- next(X,Y) & less(Y,Z)|
Before we leave our discussion of arithmetic, it is instructive to look at the concept of Diophantine equations. A polynomial equation is a sentence composed using only addition, multiplication, and exponentiation with fixed exponents (that is numbers not variables). For example, the expression shown below in traditional math notation is a polynomial equation.
x2 + 2y = 4z
A natural Diophantine equation is a polynomial equation in which the variables are restricted to the non-negative integers. For example, the polynomial equation here is also a Diophantine equation and happens to have a solution in the non-negative numbers, viz. x=4 and y=8 and z=8.
Diophantine equations can be readily expressed as sentences in Peano Arithmetic. For example, we can represent the Diophantine equation above with the rule shown below.
This is a little messy, but it is doable. And we can always clean things up by adding a little syntactic sugar to our notation to make it look like traditional math notation.