param (PROP prop.ghi () "") param (PREDICATE ../predicate/all.ghi (PROP) "") tvar (wff ph ps ch) tvar (nat A B C D) var (nat x y z) # Properties of numbers: Peano axioms term (nat (0)) term (nat (S A)) term (nat (+ A B)) term (nat (* A B)) # Equality axiom for addition ## Addition of Equal Numbers Axiom ## ## When two equal numbers are added, their sums are equal. ## ## stmt (addeq12 () () (-> (/\ (= A B) (= C D)) (= (+ A C) (+ B D)))) ## Multiplication of Equal Numbers Axiom ## ## When two equal numbers are added, their products are equal. ## ## stmt (muleq12 () () (-> (/\ (= A B) (= C D)) (= (* A C) (* B D)))) ## Peano Axiom 1: 0 is the first natural number ## ## One of the Peano axioms ## for arithmetic. 0 is the first natural number. It has no predecessor. ## It is not a successor to anything. ## ## stmt (pa_ax1 () () (-. (= (0) (S A)))) ## Peano Axiom 2: Succession Equality ## ## Two natural numbers are equal iff their successors are equal. ## One of the Peano axioms ## for arithmetic. Note that the biconditional captures equality properties of ## successor just as well as the traditional Peano axiom 2. ## ## ## (<-> (= A B) (= (S A) (S B))) ##
## stmt (pa_ax2 () () (<-> (= A B) (= (S A) (S B)))) ## Peano Axiom 3: Additive Identity Axiom ## ## One of the Peano axioms ## for arithmetic. ## ## auto-right('Simplify', '0') ## stmt (pa_ax3 () () (= (+ A (0)) A)) ## Peano Axiom 4: Addition ## ## One of the Peano axioms ## for arithmetic. ## ## left('Equivalence', 'R') ## stmt (pa_ax4 () () (= (+ A (S B)) (S (+ A B)))) ## Peano Axiom 5: Multiply by 0 ## ## One of the Peano axioms ## for arithmetic. ## ## right('Simplify','0') ## stmt (pa_ax5 () () (= (* A (0)) (0))) ## Peano Axiom 6: Multiplication ## ## One of the Peano axioms ## for arithmetic. ## ## right('Distribute','+') ## stmt (pa_ax6 () () (= (* A (S B)) (+ (* A B) A))) ## Peano Induction Axiom ## ## One of the Peano axioms. ## The more traditional statement of mathematical induction is derived ## from this axiom in the finds ## and induction ## theorems. ## ## stmt (pa_ind ((ph y)) () (-> (/\ (A. x (-> (= x (0)) ph)) (A. y (-> (A. x (-> (= x y) ph)) (A. x (-> (= x (S y)) ph))))) (A. x ph)))