% Autor: MB
% Datum: 10.02.2016
% A naive axiomatization of Peano Arithmetic, involving the definitions of natural number and successor

:- dynamic naturalNumber/1.        % Zwischenergebenisse werden in den Arbeitsspeicher geladen
:- dynamic successor/2.
:- dynamic successor/1.
:- dynamic addition/3.
:- dynamic equal/2.
:- dynamic multiplication/3.

% Axiom 1, introducing the constant [0]
naturalNumber(0).

% Axiom 2
naturalNumber(Y):- successor(Y),
                   asserta(naturalNumber(Y)).

% Axiom 3, definition of [successor]-relation
successor(X,Y):- naturalNumber(X),
                 Y is X + 1,
                 asserta(successor(X,Y)),
                 asserta(naturalNumber(Y)).

successor(Y):- naturalNumber(X),
               Y is X + 1,
               asserta(successor(X,Y)),
               asserta(naturalNumber(Y)).
               
% Axiom 4
equal(X,Y):-
             successor(X,Z),
             successor(Y,Z),
             asserta(equal(X,Y)), !.

% Axioms 5 and 6, recursive definition of addition
addition(X,0,X):- naturalNumber(X), !.
addition(X,Ys,Z):-
                          naturalNumber(X),
                          successor(Y,Ys),
                          addition(X,Y,Z1),
                          successor(Z1,Z), !,
                          asserta(addition(X,Ys,Z)).

% Axioms 7 and 8, recursive defition of multiplication
multiplication(X,0,0):- naturalNumber(X), !.
multiplication(X,Ys,Z):-
                        naturalNumber(X),
                        successor(Y,Ys),
                        multiplication(X,Y,Z1),
                        addition(Z1,X,Z),  !,
                        asserta(multiplication(X,Ys,Z)).