## redirect equality.gh param (PROP prop.ghi () "") param (PREDICATE_MIN predicate_min.ghi (PROP) "") param (PREDICATE predicate.ghi (PROP PREDICATE_MIN) "") param (EQUALITY_MIN equality_min.ghi (PROP PREDICATE_MIN PREDICATE) "") tvar (wff ph ps ch) tvar (nat A B C D) var (nat x y z) # Exists-unique is handy for iota def, but could be expanded there term (wff (E! x ph)) stmt (df-eu ((ph y)) () (<-> (E! x ph) (E. y (A. x (<-> ph (= x y)))))) stmt (eubid ((ph x)) ((-> ph (<-> ps ch))) (-> ph (<-> (E! x ps) (E! x ch)))) ## Quantifier variable exchange stmt (eualpha ((ph y) (ps x)) ((-> (= x y) (<-> ph ps))) (<-> (E! x ph) (E! y ps))) stmt (tyeu ((A x)) () (E! x (= x A))) ## A number exists that proves the antecedent ## ## (-> (= x A) [ ph) ## [ ph ##
stmt (vtocle ((A x) (ph x)) ((-> (= x A) ph)) ph) term (wff ([/] A x ph) (x A)) stmt (df-subst ((A z) (ph z)) () (<-> ([/] A x ph) (E. z (/\ (= z A) (E. x (/\ (= x z) ph)))))) term (wff (rwff x ph)) stmt (df-rwff () () (<-> (rwff x ph) (A. x (<-> ph ([/] x x ph))))) ## Symmetric Property ## ## (= A B) ## (= B A) ##
stmt (eqcomi () ((= A B)) (= B A)) ## Symmetric Property ## ## (-> ph (= A B)) ## (-> ph (= B A)) ##
stmt (eqcomd () ((-> ph (= A B))) (-> ph (= B A))) ## Equivalence over Equality stmt (eqeq1 () () (-> (= A B) (<-> (= A C) (= B C)))) ## Equivalence over Equality stmt (eqeq2 () () (-> (= A B) (<-> (= C A) (= C B)))) ## Equivalence over Equality ## ## (= A ] ] [ B ] ) ## (<-> (= A ] C) ] [ (= B ] C)) ##
stmt (eqeq1i () ((= A B)) (<-> (= A C) (= B C))) ## Equivalence over Equality ## ## (= [ A ] [ [ B) ## (<-> (= C [ A) ] [ (= C [ B)) ##
stmt (eqeq2i () ((= A B)) (<-> (= C A) (= C B))) ## Equivalence over Equality ## ## (-> ph (= A ] ] [ B ] )) ## (-> ph (<-> (= A ] C) ] [ (= B ] C))) ##
stmt(eqeq1d () ((-> ph (= A B))) (-> ph (<-> (= A C) (= B C)))) ## Equivalence over Equality ## ## (-> ph (= [ A ] [ [ B)) ## (-> ph (<-> (= C [ A) ] [ (= C [ B))) ##
stmt(eqeq2d () ((-> ph (= A B))) (-> ph (<-> (= C A) (= C B)))) stmt (eqeq12 () () (-> (/\ (= A B) (= C D)) (<-> (= A C) (= B D)))) ## Transitive Property stmt (eqeq12d () ((-> ph (= A B)) (-> ph (= C D))) (-> ph (<-> (= A C) (= B D)))) ## Equivalence over Equality stmt (eqeq12i () ((= A B) (= C D)) (<-> (= A C) (= B D))) ## Transitive Property ## ## (= A [ B ] ] ) ## [ (= B ] [ C) ## (= A [ [ [ C) ##
stmt (eqtri () ((= A B) (= B C)) (= A C)) ## Transitive Property ## ## (= A [ [ [ B) ## (= A [ C ] ] ) ## [ (= C ] [B ) ##
stmt (eqtr2 () () (-> (/\ (= A B) (= A C)) (= B C))) ## Transitive Property ## ## (-> ph (= A [ B ] ] )) ## (-> ph [ (= B ] [ C)) ## (-> ph (= A [ [ [ C)) ##
stmt (eqtrd () ((-> ph (= A B)) (-> ph (= B C))) (-> ph (= A C))) ## Transitive Property ## ## (= A [ B ] ] ) ## (= A [ [ [ C) ## [ (= B ] [ C) ##
stmt (eqtr3 () ((= A B) (= A C)) (= B C)) ## Transitive Property ## ## (= A [ [ B) ## (= [ C [ B ) ## (= A [ C ] ) ##
stmt (eqtr4 () ((= A B) (= C B)) (= A C)) ## Transitive Property ## ## (= A [ [ [ B) ## (= A [ C ] ] ) ## [ (= C ] [ B ) ##
stmt (eqtr5 () ((= A B) (= A C)) (= C B)) ## Syllogism stmt (syl5eq () ((-> ph (= A B)) (= C A)) (-> ph (= C B))) ## Syllogism stmt (syl5eqr () ((-> ph (= A B)) (= A C)) (-> ph (= C B))) ## Syllogism ## ## (-> ph (= A [ B ] ] )) ## [ (= B ] [ C) ## (-> ph (= A [ [ [ C)) ##
stmt (syl6eq () ((-> ph (= A B)) (= B C)) (-> ph (= A C))) ## Syllogism stmt (syl6eqr () ((-> ph (= A B)) (= C B)) (-> ph (= A C))) ## Syllogism stmt (sylan9eq () ((-> ph (= A B)) (-> ps (= B C))) (-> (/\ ph ps) (= A C))) ## Make Implicit Substitution Explicit ## ## A representation of explicit substitution, inferred from an implicit substitution hypothesis. ## stmt (ceqsal ((A x) (ps x)) ((-> (= x A) (<-> ph ps))) (<-> (A. x (-> (= x A) ph)) ps)) ## Make Implicit Substitution Explicit ## ## A representation of explicit substitution, inferred from an implicit substitution hypothesis. ## stmt (ceqsex ((ps x) (A x)) ((-> (= x A) (<-> ph ps))) (<-> (E. x (/\ (= x A) ph)) ps)) stmt (vtocl ((A x) (ps x)) ((-> (= x A) (<-> ph ps)) ph) ps) ## Equality over substitution ## ## If A = B, then substituting A into an expression is the same as ## substituting B. ## stmt (dfsbcq () () (-> (= A B) (<-> ([/] A x ph) ([/] B x ph)))) ## Make an implicit substitution explicit stmt (sbcie ((A x) (ps x)) ((-> (= x A) (<-> ph ps))) (<-> ([/] A x ph) ps)) ## Convert Arbitrary Substitution into Universal Quantifier stmt (cla4g ((A x) (ps x)) ((-> (= x A) (<-> ph ps))) (-> (A. x ph) ps)) ## Quantifier variable exchange stmt (exalpha ((ph y) (ps x)) ((-> (= x y) (<-> ph ps))) (<-> (E. x ph) (E. y ps))) ## Quantifier variable exchange stmt (exalpha1 ((ph y) (ps x)) ((-> (= x y) (-> ph ps))) (-> (E. x ph) (E. y ps))) ## Relatively Well-Formed Formula Infernece stmt (rwffi ((ps x) (ph y)) ((-> (= x y) (<-> ph ps))) (rwff x ph)) ## Symmetric Property stmt (eqcoms () ((-> (= A B) ph)) (-> (= B A) ph)) ## Add Substitutions to both sides stmt (sbcbid ((ph x)) ((-> ph (<-> ps ch))) (-> ph (<-> ([/] A x ps) ([/] A x ch)))) ## Existence when number is used in substitution stmt (sbcex ((A x) (ph x)) () (-> ([/] A y ph) (E. x ([/] x y ph)))) ## Substitute any number into a universal statement stmt (a4sbc () () (-> (A. x ph) ([/] A x ph))) ## Negation Preserves Relatively Well-Formed-ness stmt (not-rwff () ((rwff x ph)) (rwff x (-. ph))) ## Transitive Property stmt (3eqtr4g () ((-> ph (= A B)) (= C A) (= D B)) (-> ph (= C D))) stmt (alpha ((ph y) (ps x)) ((-> (= x y) (<-> ph ps))) (<-> (A. x ph) (A. y ps))) stmt (substex ((ph x y) (ps y) (ch x) (A y)) ((-> (/\ ph (/\ (= y A) ps)) ch)) (-> (/\ ph (E. x ps)) (E. y ch))) stmt (eu4 ((ph y) (ps x)) ((-> (= x y) (<-> ph ps))) (<-> (E! x ph) (/\ (E. x ph) (A. x (A. y (-> (/\ ph ps) (= x y))))))) ## Unique Existence Implies Existence ## right('Infer', '∃') stmt (euex () () (-> (E! x ph) (E. x ph))) ## Substitution as Existence ## right('Equivalence', '∃') left('Equivalence', '[/]') stmt (sbc5 ((A x)) () (<-> ([/] A x ph) (E. x (/\ (= x A) ph)))) term (wff (E* x ph)) stmt (mo4 ((ph y) (ps x)) ((-> (= x y) (<-> ph ps))) (<-> (E* x ph) (A. x (A. y (-> (/\ ph ps) (= x y)))))) stmt (eu5 () ((rwff x ph)) (<-> (E! x ph) (/\ (E. x ph) (E* x ph))))