###############################################################################
#                         Formal Arithmetic                                   #
#                   originally introduced by Elliott Mendelson                #
#                                   Introduction to Mathematical Logic        #
#                                   D. VAN NOSTRAND COMPANY, INC              #
#                                   PRINCETON NEW JERSEY                      #
#                                   TORONTO NEW YORK LONDON                   #
#                                   1964                                      #
#                                                                             #
#                   ForTheL translation: Piter Protsyk                        #
#                                        Kiev National State University       #
#                                        faculty of Cybernetics               #
#                               started: Ternopil, 1 April 2005               #
#                         last modified: Kiev, 22 April 2005                  #
###############################################################################
[none]

[a number / numbers]
[x is natural]

[the zero]
[0 @ the zero]

[the successor of x]
[the multiplication of x and y]
[the mul of x and y @ the multiplication of x and y]
[the sum of x and y]

[x' @ the successor of x]
[x * y @ the multiplication of x and y]
[x+y @ the sum of x and y]

#Now, we are ready to formulate some basic axioms of
#natural numbers

Axiom P0. 0 is natural number.
Axiom P1. The successor of every natural number is natural number.
Axiom P2. The sum of every natural number and every natural number is natural number.
Axiom P3. The mul of every natural number and every natural number is natural number.
Axiom P4. For every natural number N N = 0 or there exists a natural number M such that N = M'.

# In first-order logic we cannot give a finite axiomatization of well-foundness.
# Therefore ForTheL provides a preintroduced predicate symbol -<- wich is used
# as an abstract well-founded relation in induction arguments. 
# To simulate the induction on natural numbers we define following axioms:
 
Axiom IndOrdering. For every natural number N  N -<- N'.

# The following axioms discribes our theory:

Axiom S1. For all natural number A,B,C           A = B => (A = C => B = C).
Axiom S2. For all natural number A,B,C           A = B => A' = B'.
Axiom S3. For all natural number A               A'!=0.
Axiom S4. For all natural number A,B,C           A' = B' => A = B.
Axiom S5. For all natural number A               A + 0 = A.
Axiom S6. For all natural number A,B,C           A + (B') = (A+B)'.
Axiom S7. For all natural number A               A * 0 = 0.
Axiom S8. For all natural number A,B             A *(B')= (A*B) + A.

#Axiom S9. A(0) => (all x A(x) => A(x')) => all x A(x) , where A is any formula of the theory
# We don't need this axiom because it's implemented as induction principle of SAD, 
# see ForTheL language reference for details.

[a term/terms @ natural number]
################################################################################
#Every arithmetic term represent some natural number.                          #
#So we can say that every term is a representation of some natural number.     #
#Also we define three functions on natural numbers. They are the sucessor,     #
#the sum of two numbers and the multiplication.                                #
################################################################################

# Propostions L1-L8 directly derived from axioms S1-S8:

Proposition L1. For all terms t,r,s    t=r => (t=s => r=s) (by S1).
Proposition L2. For all terms t,r      t=r => t' = r' (by S2).
Proposition L3. For all term  t        0 != t' (by S3).
Proposition L4. For all terms t,r      t'= r' => t = r (by S4).
Proposition L5. For all term  t        t+0 = t (by S5).
Proposition L6. For all terms t,r      t+(r')=(t+r)' (by S6).
Proposition L7. For all term  t        t*0 = 0 (by S7).
Proposition L8. For all terms t,r      t*(r')=(t*r)+t (by S8).

# Some basic properties of natural number terms:

Proposition P_a. For all term  t        t=t.
Proposition P_b. For all terms t,r      t=r => t'=r'.
Proposition P_c. For all terms t,r,s    t=r => (r=s => t=s).
Proposition P_d. For all terms t,r,s    r=t => (s=t => r=s).
Proposition P_e. For all terms t,r,s    (t=r) => (t+s = r+s).

Proposition P_f. For all term  t        t=0+t.
Proof by induction on t.
  Let t be a term.

  Case t = 0.
    0+0 = 0 (by L5).
  end.

  Case t!=0.
    Take a term x such that x' = t.
     x = 0 + x.                                                 # Hypothesis!
    (0+(x')) = (0+x)' (by L6,P0,P1,P2,P3).
    x' = (0+x)' (by L2,P0,P1,P2,P3).
    x' = 0 + (x') (by P_d).
    x = 0 + x => x' = 0 + (x').
  end.
end.

Proposition P_g. For all terms t,r      (t')+r = (t+r)'.
Proof by induction on r.
  Let t,r be terms.

  Case r = 0.
   (t') + 0 = t'  (by L5, P0,P1,P2,P3).
    t + 0 = t (by L5,P0,P1,P2,P3).
    (t + 0)' = t' (by L2,P0,P1,P2,P3).
    (t') + 0 = (t + 0)' (by P_d).
  end.

 Case r!=0.
   Take a term x such that x' = r.
   (t') + x = (t + x)'.   # Hypothesis!
   (t') + (x') = ((t') + x)' (by L6,  P0,P1,P2,P3).
   ((t') + x)' = (t+x)'' (by L2, P0,P1,P2,P3).
   ((t') + (x')) = (t+x)'' (by P_c).
   (t+(x')) = (t+x)' (by L6,P0,P1,P2,P3).
   (t+(x'))' = (t+x)'' (by L2,P0,P1,P2,P3).
   (t')+(x') = (t+(x'))' (by P_d).
   Hence ((t')+x) = (t+x)' => (t') + (x') = (t+(x'))'.
 end.
end.

Proposition P_h. For all terms t,r      t+r=r+t.
Proof  by induction on r.
  Let t,r be terms.

  Case r = 0.
   r + 0 = r (by L5, P0,P1,P2,P3).
   r = 0 + r (by P_f).
   r+0 = 0+r (by P_c).
  end.

  Case r!=0.
   Take a term x such that x' = r.
   t + x = x + t.   #By induction hypothesis!
   t + (x') = (t + x)' (by L6,P0,P1,P2,P3).
   (x')+t = (x + t)' (by P_g).
   (t+x)' = (x+t)' (by L2,P0,P1,P2,P3).
   t+(x') = (x + t)' (by P_c).
   t+(x') = (x') + t (by P_d).
   Hence t+x = x+t => t + (x') = (x') + t. 
  end.
end.

Proposition P_i. For all terms t,r,s    t=r=>s+t=s+r.

Proposition P_j. For all terms t,r,s    (t+r)+s=t+(r+s).
Proof by induction on s.
 Let t,r,s be terms.

 Case s=0.
   (t+r) + 0 = t+r (by L5,P0,P1,P2,P3).
   r+0 = r (by L5,P0,P1,P2,P3).
   t+(r+0) = t+r (by P_i).
   (t+r)+0 = t+(r+0).
 end.

 Case s!=0.
   Take a term z such that z' = s.
    (t+r)+z = t+(r+z). #By induction hypothesis
    (t+r)+(z') = ((t+r)+z)' (by L6,P0,P1,P2,P3).
    ((t+r)+z)' = (t+(r+z))' (by L2,P0,P1,P2,P3).
    (t+r)+(z') = (t+(r+z))' (by P_c).
    r+z' = (r+z)' (by L6,P0,P1,P2,P3).
    t+(r+(z')) = t+(r+z)' (by P_i).
    t+(r+z)' = (t+(r+z))' (by L6,P0,P1,P2,P3).
    t+(r+(z')) = (t+(r+z))' (by P_d).
    (t+r)+(z') = t+(r+(z')) (by P_d).
    Hence (t+r)+z = t+(r+z) => (t+r)+(z') = t+(r+(z')).
  end.
end.

Proposition P_k. For all terms t,r,s    t=r=>t*s=r*s.

Proposition P_l. For all term  t        0*t=0.
Proof by induction on t.
 Let t be a term.

 Case t=0.
  0*0 = 0 (by L7,P0,P1,P2,P3).
 end.

 Case t!=0.
  Take a term x such that x' = t.
  0*x = 0.   #By induction hypothesis.
  0*(x') = (0*x) + 0 (by L8,P0,P1,P2,P3).
  (0*x)+0 = 0 (by L5,P0,P1,P2,P3).
  Hence 0*x = 0 => 0*(x') = 0.
 end.
end.

Proposition P_m. For all terms t,r      (t')*r=(t*r)+r.
Proof by induction on r.
 Let t,r be terms.

 Case r = 0.
  (t')*0 = 0 (by L7,P0,P1,P2,P3).
 end.

 Case r!=0.
  Take a term x such that x' = r.
   (t')*x = (t*x)+x. #By hypothesis
   (t')*(x') = ((t')*x)+(t') (by L8,P0,P1,P2,P3).
   ((t')*x)+(t') = ((t*x)+x)+(t') (by P_d).
   ((t*x)+x)+(t') = (t*x) + (x+(t')) .
   (t*x) + (x+(t')) = (t*x) + ((x+t)').
   ((t*x)+(x+t))' = (t*x) + ((x')+t).
   (t*x)+((x')+t) = (t*x)+(t+(x')).
   (t*x)+(t+(x')) = ((t*x)+t)+(x').
   ((t*x)+t)+(x') = (t*(x')) + (x') (by L8, P0,P1,P2,P3).
   Hence (t')*x = (t*x)+x => (t')*(x') =(t*(x'))+(x').
 end.
end.

Proposition P_n. For all terms t,r      t*r=r*t.
Proof by induction on r.
 Let t,r be terms.

 Case r = 0.
  t*0 = 0 (by L7, P0,P1,P2,P3).
  0*t = 0 (by P_l).
 end.

 Case r!=0.
  Take a term x such that x' = r.
   t*x = x*t. #By hypothesis.
   t*(x') = (t*x)+t (by L8, P0,P1,P2,P3).
   (t*x)+t = (x*t)+t.
   (x*t)+t = (x')*t (by P_m).
   Hence t*x = x*t => t*(x') = (x')*t.
 end.
end.

Proposition P_o. For all terms t,r,s    t=r => s*t = s*r.

# A number of important properties of addition and multiplication are given
# in following propositions:

Proposition P_p. For all terms r,s       (s=0 and r+s =r) 
                                              or 
                     there exists term x such that (x'=s)  and ((r+s) = (r+x')).

 
Proposition P_3_4_a. For all terms t,r,s  t*(r+s) = (t*r) + (t*s).
Proof by induction on s.
  Let t,r,s be terms.

   Case s = 0. 
      r+0 = r (by L5).
      t*(r+0) = t*r.
      t*r = t*r + 0.
      0 = t*0 (by L7).
      t*r = t*r + t*0.
      t*(r+0) = t*r + t*s.
    end.

   Case s!=0.
      Take a term x such that x' = s.
      Then t*(r+s) = t*(r+x') (by P_p).
       r+x' = (r+x)' (by L6).
       t*(r+x') = t*((r+x)') (by P_g,P_h).
       t*((r+x)') = (t*(r+x))+t.      
       t*(r+x)  = (t*r) + (t*x).
       (t*(r+x))+t = ((t*r)+(t*x))+t.
       ((t*r)+(t*x))+t = (t*r)+((t*x)+t) (by P_j,P2,P3).
       (t*x)+t = t*(x') (by L8).
      Hence t*(r+x') = (t*r) + (t*x').
    end.
end.

Proposition P_3_4_b. For all terms t,r,s  (r+s)*t = (r*t) + (s*t).

Proposition P_3_4_c. For all terms t,r,s  (t*r)*s = t*(r*s).
Proof by induction on s.
   Let t,r,s be terms.
 
   Case s = 0.
     (t*r)*0 = 0 (by L7,P0,P1,P2,P3,P4).
     r*0 = 0 (by L7,P0,P1,P2,P3,P4).
     t*(r*0) = 0 (by L7,P0,P1,P2,P3,P4).
   end.
   
  Case s!=0.
   Take a term x such that x' = s.
    (t*r)*x = t*(r*x). #By induction hypothesis
    (t*r)*(x')=((t*r)*x) + (t*r) (by L8,P0,P1,P2,P3,P4).
    ((t*r)*x)+(t*r) = (t*(r*x)) + (t*r).
    (t*(r*x))+(t*r) = t*((r*x)+r) (by P_3_4_a,P0,P1,P2,P3,P4).
    Hence t*((r*x)+r) = t*(r*(x')) (by L8,P0,P1,P2,P3,P4).
  end.
end.

Proposition P_3_4_d. For all terms t,r,s t+s = r+s => t = r.
Proof by induction on s.
 Let t,r,s be terms.
  
 Case s = 0.
  t+0 = t.
  r+0 = r.
  Hence t+0 = r+0 => t=r.
 end.

 Case s!=0.
  Take a term x such that x' = s.
   t+x = r+x => t = r.
   t+x' = (t+x)'.
   r+x' = (r+x)'.
   (t+x)' = (r+x)' => t+x =r+x => t = r.
   Hence t+(x')=r+(x') => t = r. 
 end.
end.

[the one @ 0'] [1 @ the one]
[the two @ 1'] [2 @ the two]
[the three @ 2'] [3 @ the three]
[the four @ 3'] [4 @ the four]
[the five @ 4'] [5 @ the five]
[the six @ 5'] [6 @ the six]
[the seven @ 6'] [7 @ the seven]
[the eight @ 7'] [8 @ the eight]
[the nine @ 8'] [9 @ the nine]
[the ten @ 9'] [10 @ the ten]

Proposition P_3_5_a. For all term t t + 1 = t'.
Proposition P_3_5_b. For all term t t * 1 = t.
Proposition P_3_5_c. For all term t t * 2 = t+t.

[none]
# Proving of this example is based on induction principle.
# But we cannot write the proofs because induction provides on formula.
# In current release induction is based only on terms

Proposition P_3_5_d. For all term t,s t +s = 0 => (t = 0) and (s = 0).
Proposition P_3_5_e. For all term t,s t != 0 => (s*t = 0 => s = 0).
Proposition P_3_5_f. For all term t,s  (t+s = 1) => (t = 0 and s = 1) or (t=1 and s=0) .
Proposition P_3_5_g. For all term t,s  (t*s = 1) => (t = 1 and s = 1).
Proposition P_3_5_h. For all term t  if (t!=0) then there exists term y such that t = y'.
Proposition P_3_5_i. For all term t,s,r  s!=0 => (t*s = r*s => t = r).
Proposition P_3_5_j. For all term t if (t!=0) then t is not equal to one and 
                      there exists term y such that t is equal to y''.
#[full]

[x is less then y]
[x is less or equal y]
[x is greater then y @ y is less then x]
[x is greater or equal  y @ y is less or equal y]

[x < y @ x is less then y]
[x=< y @ x is less or equal y]
[x > y  @ x is greater then y]
[x>= y @ x is greater or equal y]

Definition DefLess.
 Let t,s be terms.
 t is less then s iff there exists a term w such that w is not equal to zero and t+w = s.

Definition DefLessOrEqual.
 Let t,s be terms.
 t is less or equal s iff t < s or t =s.

Proposition  P_3_7_a.  For every term t t is not less then t.
Proposition  P_3_7_b.  For every terms t,s,r  t<s => (s<r => t<r).
Proof.
 Let t,s,r be terms.
 Suppose t<s and s<r.
 Then (there exists a term w such that w!=0 and t+w = s) and
          (there exists a term v such that v!=0 and s+v = r) (by DefLess).
 Take a term w such that t+w = s.
 Take a term v such that s+v =r.

 (t+w)+v = r.
 t+(w+v) = r.
 w!=0 and v!=0.
 w+v!=0.
 w+v!=0 and t+(w+v) = r.
 Then there exists  a term u such that u!=0 and t+u = r.
 Hence t<r.
 Then t<s => (s<r => t<r).
end.

Proposition  P_3_7_c. For every terms t,s t<s => not s<t.
Proposition  P_3_7_d. For every terms t,s,r  t<s <=> t+r < s+r.
Proposition  P_3_7_e. For every term t t is less or equal t.
Proposition  P_3_7_f. For every terms t,s,r t=<s => (s =< r => t =< r).
Proposition  P_3_7_g. For every terms t,s,r t=<s => (t+r =< s+r).
Proposition  P_3_7_h. For every terms t,s,r t=<s => (s < r => t < r).
Proposition  P_3_7_i. For every term t  0=<t.
Proposition  P_3_7_j. For every term t 0<t'.
Proposition  P_3_7_k. For every terms t,r t<r <=> t' =< r.
Proposition  P_3_7_l. For every terms t,s,r t=<r <=> t< r'.
Proposition  P_3_7_m. For every term t t<t'.
Proposition  P_3_7_n. (0 < 1) and (1 < 2) and  (2 < 3) and  (3 < 4) and  (4 < 5) and  (5 < 6) and (6 < 7) and  (7 < 8) and  (8 < 9 ) and  (9 < 10).
Proposition  P_3_7_o. For every terms t,r  t!=r => (t < r or r < t).
Proposition  P_3_7_oo.For every terms t,r  (t = r) or (t < r) or (r < t).
Proposition  P_3_7_p. For every terms t,r  (t=<r) or (r =< t).
Proposition  P_3_7_q. For every terms t,r t+r >= t.
Proposition  P_3_7_r. For every terms t,r  if r!=0 then t+r > 0.
Proposition  P_3_7_s. For every terms t,r if r!=0 then t*r >= t.
Proposition  P_3_7_t. For every terms r  if r!=0 then r>0.
Proposition  P_3_7_u. For every terms t,r r>0 => (t>0 => r*t >0).
Proposition  P_3_7_v. For every terms t,r r!=0 => (t>1 => t*r > r).
Proposition  P_3_7_w. For every terms t,s,r r!=0 => (t<s <=> t*r < s*r).
Proposition  P_3_7_x. For every terms t,s,r r!=0 => (t=<s <=> t*r =< s*r).
Proposition  P_3_7_y. For every terms t it is wrong that t < 0.
Proposition  P_3_7_z. For every terms t,r if (t=<r) and (r =< t) then t = r.

[x divide y]
[x | y @ x divide y]

Definition DefDivide.
 Let t,s be terms.
 t divide s iff there exists a term z such that s = t*z.

Proposition P_3_10_a. For all term t  t | t.
Proposition P_3_10_b. For all term t  1 | t.
Proposition P_3_10_c. For all term t  t | 0.
Proposition P_3_10_d. For all terms t,s,r  If t | s and s | r then t | r.
Proposition P_3_10_e. For all terms t,s  If s!=0 and t | s then t =< s.
Proposition P_3_10_f. For all terms t,s if t|s and s|t then s = t.
Proposition P_3_10_g. For all terms t,s,r  If t | s then  t | r*s.
Proposition P_3_10_h. For all term t,s,r  If t|s and t|r then t | s + r.

#Please try to write formal proofs of this exercises.

Proposition Exercise_1. For all term t If t | 1 then t = 1.
Proposition Exercise_2. For all terms t,s (t | s => t | s') => t = 1.

[none]
# Proving of this example is based on induction principle.
# But we cannot write the proofs because induction provides on formula.
# In current release induction is based only on terms
 Axiom P_3_11. For all term x,y If y!=0 then there exists terms u,v such that (( x = y*u + v and v < y) and 
                                   there exists terms m,n such that if ( x = y*m + n and n < y) then (u = m and n = v)).
#[full]