Peano: THEORY
%%%
%%% In this theory we "build" arithmetic from
%%% basic principles.  Addition (p) and multiplication
%%% (m) are defined in terms of a "successor" function
%%% (s) which is thought of as "add-one".
%%%
%%% In essence, We are defining the set N inductively,
%%% according to
%%%      1) Z [zero] is an element of N
%%%      2) if k is an element of N, then so is S(k) [1+k]
%%%      3) nothing else
%%%
%%% But a purely logical formulation does not allow
%%% inductive set definitions.
%%%
BEGIN
N: TYPE+              % Our model for the natural numbers
Z: N                  % the zero element
S: [N -> N]           % the constructor, think of S(k) as 1+k
i,j,k: VAR N

%%%
%%% Zero is no number's successor.
%%%

ZERO: AXIOM i = S(j) IMPLIES NOT i = Z

%%%
%%% S is one-to-one
%%%

S_is_one_to_one: AXIOM S(i) = S(j) IMPLIES i = j

%%%
%%% Axiomatize the induction principle as:
%%%

IND: AXIOM forall (H:[N -> bool]):(
      H(Z)
      AND
      (forall i: (H(i) IMPLIES H(S(i))))
      IMPLIES
      (forall i: H(i)))

%%% 
%%% Now, define addition and multiplication.
%%% The recursive defintions would be.
%%%
%%%    p(0, k) = k 
%%%    p(j+1, k) = 1 + p(j, k) 
%%%
%%%    m(0, k) = 0
%%%    m(j+1, k) = p(k, m(j, k))
%%%
%%% But, again, we don't have recursion.
%%% I'm cheating here by declaring "p" and "m" to have
%%% type "function".  It really should be
%%% proved that p and m are functions, not mere relations. 

p: [N, N -> N]
Pz: AXIOM p(Z, j) = j
Ps: AXIOM p(S(i), j) = S(p(i, j))

m: [N, N -> N]
Mz: AXIOM m(Z, j) = Z
Ms: AXIOM m(S(i), j) = p(j, m(i, j))

%%%
%%% If our model is valid, it should satisfy the laws of
%%% arithmetic, some of which are stated in the following
%%% theorems.
%%%

P_ide: THEOREM p(i, Z) = i                                  %%% x + 0 = x
P_lemma: LEMMA p(S(i), j) = p(i, S(j))                      %%% Sx + y = x + Sy
P_com: THEOREM p(i, j) = p(j, i)                            %%% + is commutative
P_assoc: THEOREM p(p(i, j), k) = p(i, p(j, k))              %%% + is associative
M_ide: THEOREM m(i, S(Z)) = i                               %%% x * 1 = x
M_com: THEOREM m(i, j) = m(j, i)                            %%% * is commutative
M_assoc: THEOREM m(m(i, j), k) = m(i, m(j, k))              %%% * is associative
M_distr_over_P: THEOREM m(i, p(j, k)) = p(m(i,j), m(i, k))  %%% distributivity

%%%
%%% Hint: Prove these first by hand, using infix notation, so you can
%%%       get a clear idea of what you need to do in the Prover.
%%%
END Peano