Peano's Axioms in Prolog

peano.pl

% Peano's Axioms
:- module(peano, [
  is_zero/1,
  is_natural/1,
  equal/2,
  add/3,
  subtract/3,
  multiply/3,
  divide/3
]).

/** Peano's Axioms
 *
 * 1. 0 is a natural number
 * 2. For every number x, x = x (reflexive property)
 * 3. For all numbers x and y, if x = y, then y = x (symmetric property)
 * 4. For all numbers x, y and z, if x = y and y = z, then x = z (transitive property)
 * 5. For all a and b, if b is a natural number and a = b, then a is also a natural number (closed under equality)
 * 6. For every number n, Successor(n) is a number (closed under a successor function)
 * 7. For all numbers m and n, m = n if and only if Successor(m) = Successor(n) (Successor is an injection)
 * 8. For every number n, Successor(n) = 0 is false (0 is the starting point of the numbers)
 */
is_zero(zero).

is_natural(zero).
is_natural(succ(X)) :- is_natural(X).

equal(X, succ(_)) :- is_natural(X), \+ is_zero(X). 
equal(X, X) :- is_natural(X).

add(zero, Addend, Addend).
add(Addend, zero, Addend).
add(succ(Addend1), Addend2, Sum) :-
  add(Addend1, succ(Addend2), Sum).

subtract(zero, zero, zero).
subtract(Minuend, zero, Minuend).
subtract(succ(NewMinuend), succ(NewSubtrahend), Difference) :-
  subtract(NewMinuend, NewSubtrahend, Difference).

multiply(zero, _, zero).
multiply(_, zero, zero).
multiply(Multiplicand, succ(zero), Multiplicand).
multiply(Multiplicand, succ(Multiplier), Product) :-
  add(Multiplicand, OldProduct, Product),
  multiply(Multiplicand, Multiplier, OldProduct).

divide(X, Y, Z) :- multiply(Y, Z, X).