## ## Naturals ../naturals/add_multiply_min.gh ## Integers ../integers/add_multiply_min.gh ## Rationals ../rationals/NaN_construction/division_NaN.gh ## Rationals2 ../rationals/division_min.gh ## Complex ../complex/add_multiply_min.gh ## # The basic properties common to natural, integer, rational, real, and complex arithmetic. # derived initially from the Peano axioms and subsequently during the construction of the # integers, rationals, reals, and complex numbers. param (PROP prop.ghi () "") param (PREDICATE ../../predicate/all.ghi (PROP) "") tvar (wff ph ps ch th ta) tvar (nat A B C D) var (nat x) term (nat (+ A B)) term (nat (* A B)) term (nat (0)) term (nat (1)) ## Associative Property ## right('Associate', 'R') left('Associate', 'L') stmt (addass () () (= (+ (+ A B) C) (+ A (+ B C)))) ## Additive Identity ## auto-right('Simplify', '0') stmt (addid () () (= (+ A (0)) A)) ## Commutative Property ## ## (= (+ A B) (+ B A)) ##
## right('Commute', '+') stmt (addcom () () (= (+ A B) (+ B A))) ## Associative Property ## right('Associate', 'R') left('Associate', 'L') stmt (mulass () () (= (* (* A B) C) (* A (* B C)))) ## Commutative Property ## ## (= (* A B) (* B A)) ##
## right('Commute', '*') stmt (mulcom () () (= (* A B) (* B A))) # Distribution of addition through multiplication ## Distributive Property ## ## (= (* A (+ B C)) (+ (* A B) (* A C))) ##
## right('Distribute', 'R') left('Distribute', '-R') stmt (distr () () (= (* A (+ B C)) (+ (* A B) (* A C)))) ## Multiplicative Identity ## right('Simplify', '1') ## ## (= (* A (1)) A) ##
## auto-right('Simplify') stmt (mulid () () (= (* A (1)) A)) ## 0 is not equal to 1 stmt (0ne1 () () (-. (= (0) (1)))) # 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)))) ## Cancellation of addition ## right('Cancel', '+') stmt (addcan () () (<-> (= (+ B A) (+ C A)) (= B C)))