Peano's Axioms in Prolog

peano.pl

% Peano's Axioms
:- module(peano, [
  is_zero/1,
  is_natural/1,
  equal/2,
  pred/2
]).

/** 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).

pred(succ(X), X) :- is_natural(X).

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