## ## Naturals axiom ## Integers ../arithmetic/integers/equality_min.gh ## Rationals ../arithmetic/rationals/NaN_construction/equality_min.gh ## Rationals2 ../arithmetic/rationals/equality_min.gh ## Complex ../arithmetic/complex/equality_min.gh ## param (PROP prop.ghi () "") param (PREDICATE_MIN predicate_min.ghi (PROP) "") param (PREDICATE predicate.ghi (PROP PREDICATE_MIN) "") tvar (nat A B C D) var (nat x y z) term (wff (= A B)) ## Equality Reflexive Property ## stmt (eqid () () (= A A)) ## Symmetric Property ## ## (<-> (= A B) (= B A)) ##
## right('Commute', '=') stmt (eqcom () () (<-> (= A B) (= B A))) ## Equality Transitive Property ## right('Simplify', '=') ## ## (-> (/\ (= A B) (= B C)) (= A C)) ##
## stmt (eqtr () () (-> (/\ (= A B) (= B C)) (= A C))) # Similar to ax-9, but expanded to nat's instead of var's. ## There is a number equal to any expression ## ## One of the axioms of predicate calculus with equality. ## One thing this tells us is that at least one number exists. ## ## stmt (tyex ((A x)) () (E. x (= x A)))